[STATEMENT]
lemma inj_linear_imp_inv_linear:
  assumes "linear scale scale f" "inj f" shows "linear scale scale (inv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear (*s) (*s) (inv f)
[PROOF STEP]
using assms inj_iff left_inverse_linear
[PROOF STATE]
proof (prove)
using this:
linear (*s) (*s) f
inj f
inj ?f = (inv ?f \<circ> ?f = id)
\<lbrakk>linear (*s) (*s) ?f; ?g \<circ> ?f = id\<rbrakk> \<Longrightarrow> linear (*s) (*s) ?g

goal (1 subgoal):
 1. linear (*s) (*s) (inv f)
[PROOF STEP]
by blast