awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
w : W
d : Dual K W
hd :
  Eq.{u_1 + 1} (α := K)
    ((d : (a : W) → K) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W) : K) (1 : K)
⊢ (T : (a : V) → W) ((((f.symm : (a : End K W) → End K V) (smulRight d w) : End K V) : (a : V) → V) u : V) = w

Tactic:
simp [T, this, hd]
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
w : W
d : Dual K W
hd :
  Eq.{u_1 + 1} (α := K)
    ((d : (a : W) → K) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W) : K) (1 : K)
⊢ ∃ (a : V), (T : (a : V) → W) a = w

Tactic:
exact ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)

Tactic:
have surj : Function.Surjective T := fun w ↦ by
    obtain ⟨d, hd⟩ := Projective.exists_dual_eq_one K hz
    exact ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
x y : V
hxy : Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W) ((T : (a : V) → W) y : W)
apply :
  ∀ (z : W),
    Eq (α := W)
      ((((f : (a : End K V) → End K W)
                ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) x) :
              End K W) :
            (a : W) → W)
          z :
        W)
      ((((f : (a : End K V) → End K W)
                ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) y) :
              End K W) :
            (a : W) → W)
          z :
        W)
⊢ Eq (α := V →ₗ[K] V)
    ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) x : V →ₗ[K] V)
    ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) y : V →ₗ[K] V)

Tactic:
apply f.injective <| LinearMap.ext fun z ↦ ?_

Premises used: LinearMap.ext, AlgEquiv.injective
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z_1 : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z_1 : W)
      ((0 : (a : W) → W) z_1 : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z_1 ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z_1 : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
x y : V
hxy : Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W) ((T : (a : V) → W) y : W)
z : W
obtain :
  ∀ (w : V),
    Eq.{u_3 + 1} (α := W)
      ((((f : (a : End K V) → End K W)
                ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) x) :
              End K W) :
            (a : W) → W)
          ((T : (a : V) → W) w : W) :
        W)
      ((((f : (a : End K V) → End K W)
                ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) y) :
              End K W) :
            (a : W) → W)
          ((T : (a : V) → W) w : W) :
        W)
⊢ Eq (α := W)
    ((((f : (a : End K V) → End K W)
              ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) x) :
            End K W) :
          (a : W) → W)
        z :
      W)
    ((((f : (a : End K V) → End K W)
              ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) y) :
            End K W) :
          (a : W) → W)
        z :
      W)

Tactic:
obtain ⟨w, rfl⟩ := surj z

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
x y : V
hxy : Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W) ((T : (a : V) → W) y : W)
w : V
simp_rw :
  Eq.{u_3 + 1} (α := W)
    ((T : (a : V) → W)
        ((((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) x :
                V →ₗ[K] V) :
              (a : V) → V)
            w :
          V) :
      W)
    ((T : (a : V) → W)
        ((((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) y :
                V →ₗ[K] V) :
              (a : V) → V)
            w :
          V) :
      W)
simp_rw₁ :
  Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) (HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((v : (a : V) → K) w : K) x) : W)
    ((T : (a : V) → W) (HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((v : (a : V) → K) w : K) y) : W)
simp_rw₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := K) (β := W) ((v : (a : V) → K) w : K) ((T : (a : V) → W) x : W) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := K) (β := W) ((v : (a : V) → K) w : K) ((T : (a : V) → W) y : W)
⊢ Eq.{u_3 + 1} (α := W)
    ((((f : (a : End K V) → End K W)
              ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) x) :
            End K W) :
          (a : W) → W)
        ((T : (a : V) → W) w : W) :
      W)
    ((((f : (a : End K V) → End K W)
              ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) y) :
            End K W) :
          (a : W) → W)
        ((T : (a : V) → W) w : W) :
      W)

Tactic:
simp_rw [← this, smulRightₗ_apply_apply, _root_.map_smul, hxy]

Premises used: LinearMap.smulRightₗ_apply_apply, map_smul
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
x y : V
hxy : Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W) ((T : (a : V) → W) y : W)
⊢ Eq (α := V →ₗ[K] V)
    ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) x : V →ₗ[K] V)
    ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) y : V →ₗ[K] V)

Tactic:
have h_smul : smulRightₗ v x = smulRightₗ v y := by
      apply f.injective <| LinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp_rw [← this, smulRightₗ_apply_apply, _root_.map_smul, hxy]
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
x y : V
hxy : Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W) ((T : (a : V) → W) y : W)
h_smul :
  Eq (α := V →ₗ[K] V)
    ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) x : V →ₗ[K] V)
    ((((smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v : V →ₗ[K] V →ₗ[K] V) : (a : V) → V →ₗ[K] V) y : V →ₗ[K] V)
⊢ x = y

Tactic:
simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)

Premises used: Ne.isUnit, IsUnit.smul_left_cancel
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)

Tactic:
have inj : Function.Injective T := fun x y hxy ↦ by
    have h_smul : smulRightₗ v x = smulRightₗ v y := by
      apply f.injective <| LinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp_rw [← this, smulRightₗ_apply_apply, _root_.map_smul, hxy]
    simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
⊢ ∃ (T : V ≃ₗ[K] W), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a

Tactic:
⟨.ofBijective T ⟨inj, surj⟩, fun A ↦ (LinearMap.ext <| this A).symm⟩

Premises used: LinearMap.ext, And.intro, Exists.intro, Eq.symm, LinearEquiv.ofBijective
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
⊢ ∃ (T : V ≃ₗ[K] W), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a

Tactic:
exact ⟨.ofBijective T ⟨inj, surj⟩, fun A ↦ (LinearMap.ext <| this A).symm⟩
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
⊢ Function.Surjective (α := V ≃ₗ[K] W) (β := AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)) (conjAlgEquiv K)

Tactic:
fun f ↦ f.eq_linearEquivConjAlgEquiv.imp fun _ h ↦ h.symm

Premises used: Exists.imp, Function.Surjective, AlgEquiv.eq_linearEquivConjAlgEquiv
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
f : End K V ≃ₐ[K] End K V
have :
  ∀ (T : V ≃ₗ[K] V) (hT : f = conjAlgEquiv K T),
    ∃ (a : ConjAct (GeneralLinearGroup K V)), MulSemiringAction.toAlgEquiv K (End K V) a = f
⊢ ∃ (a : ConjAct (GeneralLinearGroup K V)), MulSemiringAction.toAlgEquiv K (End K V) a = f

Tactic:
have ⟨T, hT⟩ := f.eq_linearEquivConjAlgEquiv
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
f : End K V ≃ₐ[K] End K V
T : V ≃ₗ[K] V
hT : f = conjAlgEquiv K T
⊢ ∃ (a : ConjAct (GeneralLinearGroup K V)), MulSemiringAction.toAlgEquiv K (End K V) a = f

Tactic:
⟨.ofLinearEquiv T, hT.symm⟩

Premises used: LinearMap.GeneralLinearGroup.ofLinearEquiv, Exists.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
Goal:
K : Type u_1
V : Type u_2
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
f : End K V ≃ₐ[K] End K V
T : V ≃ₗ[K] V
hT : f = conjAlgEquiv K T
⊢ ∃ (a : ConjAct (GeneralLinearGroup K V)), MulSemiringAction.toAlgEquiv K (End K V) a = f

Tactic:
exact ⟨.ofLinearEquiv T, hT.symm⟩
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : GeneralLinearGroup R M
m : M
⊢ (f.inv * (↑f : M →ₗ[R] M) : (a : M) → M) m = m

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : GeneralLinearGroup R M
m : M
⊢ ((↑f : M →ₗ[R] M) * f.inv : (a : M) → M) m = m

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : GeneralLinearGroup R M
⊢ Eq (α := (a : M) → M) (⇑f.toLinearEquiv : (a : M) → M) (⇑(↑f : M →ₗ[R] M) : (a : M) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : GeneralLinearGroup R M
⊢ (f * g).toLinearEquiv = f.toLinearEquiv * g.toLinearEquiv

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : GeneralLinearGroup R M
⊢ f⁻¹.toLinearEquiv = f.toLinearEquiv⁻¹

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M ≃ₗ[R] M
⊢ Eq (α := (a : M) → M) (⇑(↑(ofLinearEquiv f) : M →ₗ[R] M) : (a : M) → M) (⇑f : (a : M) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M ≃ₗ[R] M
⊢ ofLinearEquiv (f * g) = ofLinearEquiv f * ofLinearEquiv g

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M ≃ₗ[R] M
⊢ ofLinearEquiv f⁻¹ = (ofLinearEquiv f)⁻¹

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M ≃ₗ[R] M
x : M
⊢ ofLinearEquiv f • x = (f : (a : M) → M) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : GeneralLinearGroup R M
h :
  ∀ (x_1 : M),
    Eq (α := M) (((x * y).toLinearEquiv : (a : M) → M) x_1 : M)
      ((x.toLinearEquiv * y.toLinearEquiv : (a : M) → M) x_1 : M)
⊢ (x * y).toLinearEquiv = x.toLinearEquiv * y.toLinearEquiv

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : GeneralLinearGroup R M
x_1 : M
⊢ Eq (α := M) (((x * y).toLinearEquiv : (a : M) → M) x_1 : M)
    ((x.toLinearEquiv * y.toLinearEquiv : (a : M) → M) x_1 : M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : GeneralLinearGroup R M
h :
  ∀ (x : M),
    Eq (α := M)
      (((↑((generalLinearEquiv R M : (a : GeneralLinearGroup R M) → M ≃ₗ[R] M) f) : M →ₗ[R] M) : (a : M) → M) x : M)
      (((↑f : M →ₗ[R] M) : (a : M) → M) x : M)
⊢ (↑((generalLinearEquiv R M : (a : GeneralLinearGroup R M) → M ≃ₗ[R] M) f) : M →ₗ[R] M) = (↑f : M →ₗ[R] M)

Tactic:
ext