[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
src✝ : M →ₗ[R] M := ↑f
m : M
⊢ ↑(f.inv * ↑f) m = m
[PROOFSTEP]
erw [f.inv_val]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
src✝ : M →ₗ[R] M := ↑f
m : M
⊢ ↑1 m = m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
src✝ : M →ₗ[R] M := ↑f
m : M
⊢ ↑(↑f * f.inv) m = m
[PROOFSTEP]
erw [f.val_inv]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
src✝ : M →ₗ[R] M := ↑f
m : M
⊢ ↑1 m = m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ ofLinearEquiv (toLinearEquiv f) = f
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
x✝ : M
⊢ ↑↑(ofLinearEquiv (toLinearEquiv f)) x✝ = ↑↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
⊢ toLinearEquiv (ofLinearEquiv f) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
x✝ : M
⊢ ↑(toLinearEquiv (ofLinearEquiv f)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : GeneralLinearGroup R M
⊢ Equiv.toFun
      { toFun := toLinearEquiv, invFun := ofLinearEquiv,
        left_inv := (_ : ∀ (f : GeneralLinearGroup R M), ofLinearEquiv (toLinearEquiv f) = f),
        right_inv := (_ : ∀ (f : M ≃ₗ[R] M), toLinearEquiv (ofLinearEquiv f) = f) }
      (x * y) =
    Equiv.toFun
        { toFun := toLinearEquiv, invFun := ofLinearEquiv,
          left_inv := (_ : ∀ (f : GeneralLinearGroup R M), ofLinearEquiv (toLinearEquiv f) = f),
          right_inv := (_ : ∀ (f : M ≃ₗ[R] M), toLinearEquiv (ofLinearEquiv f) = f) }
        x *
      Equiv.toFun
        { toFun := toLinearEquiv, invFun := ofLinearEquiv,
          left_inv := (_ : ∀ (f : GeneralLinearGroup R M), ofLinearEquiv (toLinearEquiv f) = f),
          right_inv := (_ : ∀ (f : M ≃ₗ[R] M), toLinearEquiv (ofLinearEquiv f) = f) }
        y
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : GeneralLinearGroup R M
x✝ : M
⊢ ↑(Equiv.toFun
          { toFun := toLinearEquiv, invFun := ofLinearEquiv,
            left_inv := (_ : ∀ (f : GeneralLinearGroup R M), ofLinearEquiv (toLinearEquiv f) = f),
            right_inv := (_ : ∀ (f : M ≃ₗ[R] M), toLinearEquiv (ofLinearEquiv f) = f) }
          (x * y))
      x✝ =
    ↑(Equiv.toFun
            { toFun := toLinearEquiv, invFun := ofLinearEquiv,
              left_inv := (_ : ∀ (f : GeneralLinearGroup R M), ofLinearEquiv (toLinearEquiv f) = f),
              right_inv := (_ : ∀ (f : M ≃ₗ[R] M), toLinearEquiv (ofLinearEquiv f) = f) }
            x *
          Equiv.toFun
            { toFun := toLinearEquiv, invFun := ofLinearEquiv,
              left_inv := (_ : ∀ (f : GeneralLinearGroup R M), ofLinearEquiv (toLinearEquiv f) = f),
              right_inv := (_ : ∀ (f : M ≃ₗ[R] M), toLinearEquiv (ofLinearEquiv f) = f) }
            y)
      x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ ↑(↑(generalLinearEquiv R M) f) = ↑f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
x✝ : M
⊢ ↑↑(↑(generalLinearEquiv R M) f) x✝ = ↑↑f x✝
[PROOFSTEP]
rfl
