awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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)
⊢ ∃ (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
have neg : ∀ (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), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a
Tactic: obtain ⟨z, hz⟩ : ∃ z : W, ¬ f (smulRight v u) z = (0 : End K W) z := by
    rw [← not_forall, ← LinearMap.ext_iff, EmbeddingLike.map_eq_zero_iff, LinearMap.ext_iff]
    exact not_forall.mpr ⟨u, huv.isUnit.smul_eq_zero.not.mpr hu⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (hypothesis)
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
⊢ ∃ (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
have 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)
Tactic: have hT x : T x = f (smulRight v x) z := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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)
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)
have simp : Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v ((A : (a : V) → V) x)) : End K W) : (a : W) → W) z : W)
  ((((f : (a : End K V) → End K W) (A * smulRight v x) : End K W) : (a : W) → W) z : W)
Tactic: simp only [hT, ← End.mul_apply, ← map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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)
A : End K V
x : V
⊢ Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v ((A : (a : V) → V) x)) : End K W) : (a : W) → W) z : W)
    ((((f : (a : End K V) → End K W) (A * smulRight v x) : End K W) : (a : W) → W) z : W)
have e_a : smulRight v ((A : (a : V) → V) x) = A * smulRight v x
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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)
A : End K V
x : V
⊢ smulRight v ((A : (a : V) → V) x) = A * smulRight v x
have e_a : ∀ (x_1 : V),
  Eq (α := V) (((smulRight v ((A : (a : V) → V) x) : V →ₗ[K] V) : (a : V) → V) x_1 : V)
    ((A * smulRight v x : (a : V) → V) x_1 : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (hypothesis)
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)
⊢ ∃ (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
have 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)
Tactic: have this A x : T (A x) = f A (T x) := by
    simp only [hT, ← End.mul_apply, ← map_mul]
    congr; ext; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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
⊢ ∃ (a : V), (T : (a : V) → W) a = w
have obtain : ∀ (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: obtain ⟨d, hd⟩ := Projective.exists_dual_eq_one K hz
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (hypothesis)
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)
⊢ ∃ (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
have surj : 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]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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)
have 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)
Tactic: apply f.injective <| LinearMap.ext fun z ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨w, rfl⟩ := surj z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [← this, smulRightₗ_apply_apply, _root_.map_smul, hxy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [← this, smulRightₗ_apply_apply, _root_.map_smul, hxy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [← this, smulRightₗ_apply_apply, _root_.map_smul, hxy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (hypothesis)
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)
⊢ x = y
have 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)
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]