awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
w : W
⊢ Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        w :
      W)
have h : Eq.{u_6 + 1} (α := W)
  ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) 0 : W)
  (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
        (a : W) → W)
      0 :
    W)
Tactic: induction w using ibc.inductionOn with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | smul a w hw => simp [hw]
  | tmul x => simp [LinearMap.transvection.apply, endHom_comp_apply, toDual_comp_apply]
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
w : W
h :
  Eq.{u_6 + 1} (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) 0 : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        0 :
      W)
⊢ Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        w :
      W)
have h₁ : ∀ (x y : W)
  (hx :
    Eq (α := W)
      ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) x : W)
      (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
            (a : W) → W)
          x :
        W))
  (hy :
    Eq (α := W)
      ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) y : W)
      (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
            (a : W) → W)
          y :
        W)),
  Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) (x + y) : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        (x + y) :
      W)
Tactic: induction w using ibc.inductionOn with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | smul a w hw => simp [hw]
  | tmul x => simp [LinearMap.transvection.apply, endHom_comp_apply, toDual_comp_apply]
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
w : W
h :
  Eq.{u_6 + 1} (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) 0 : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        0 :
      W)
h₁ :
  ∀ (x y : W)
    (hx :
      Eq (α := W)
        ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) x : W)
        (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
              (a : W) → W)
            x :
          W))
    (hy :
      Eq (α := W)
        ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) y : W)
        (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
              (a : W) → W)
            y :
          W)),
    Eq (α := W)
      ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) (x + y) :
        W)
      (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
            (a : W) → W)
          (x + y) :
        W)
⊢ Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        w :
      W)
have h₂ : ∀ (a : A) (w : W)
  (hw :
    Eq (α := W)
      ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
      (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
            (a : W) → W)
          w :
        W)),
  Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) (a • w) : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        (a • w) :
      W)
Tactic: induction w using ibc.inductionOn with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | smul a w hw => simp [hw]
  | tmul x => simp [LinearMap.transvection.apply, endHom_comp_apply, toDual_comp_apply]
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : CommRing A
inst_4 : Algebra R A
e : V ≃ₗ[R] V
he : Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e
⊢ Membership.mem (γ := Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V)) (dilatransvections A (A ⊗[R] V) : Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V))
    (LinearEquiv.baseChange R A V V e)
have obtain : ∀ (f : Dual R V) (v : V) (he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v),
  Membership.mem (γ := Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V)) (dilatransvections A (A ⊗[R] V) : Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V))
    (LinearEquiv.baseChange R A V V e)
Tactic: obtain ⟨f, v, he⟩ := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : CommRing A
inst_4 : Algebra R A
e : V ≃ₗ[R] V
f : Dual R V
v : V
he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v
⊢ Membership.mem (γ := Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V)) (dilatransvections A (A ⊗[R] V) : Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V))
    (LinearEquiv.baseChange R A V V e)
have h : Eq (α := A ⊗[R] V →ₗ[A] A ⊗[R] V) (↑(LinearEquiv.baseChange R A V V e) : A ⊗[R] V →ₗ[A] A ⊗[R] V)
  (LinearMap.transvection ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (1 ⊗ₜ[R] v))
Tactic: use (f.baseChange A), (1 ⊗ₜ[R] v)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have pos : ∀ (hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)),
  (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: by_cases hfv : f v = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
pos :
  ∀ (hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)),
    (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have neg : ∀ (hfv : ¬Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)),
  (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: by_cases hfv : f v = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have pos : ∀ (hv : v = 0),
  (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
pos :
  ∀ (hv : v = 0),
    (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have neg : ∀ (hv : ¬v = 0),
  (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have pos : ∀ (hf : f = 0),
  (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
pos :
  ∀ (hf : f = 0),
    (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have neg : ∀ (hf : ¬f = 0),
  (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have neg : ∀ (ι : Set V) (b : Basis (↑ι : Type u_4) K V) (i j : (↑ι : Type u_4)) (hi : i ≠ j)
  (hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j),
  (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: obtain ⟨ι, b, i, j, hi, hj⟩ := exists_basis_of_pairing_eq_zero hfv hf hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have neg : ∀ (this : Fintype (↑ι : Type u_4)),
  (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this : Fintype (↑ι : Type u_4)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have neg : Matrix.det.{u_3, u_4} (n := (↑ι : Type u_4))
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v)) =
  HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: rw [← det_toMatrix b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this_1 : Fintype (↑ι : Type u_4)
this :
  Eq (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    (Matrix.transvection i j 1 : Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
⊢ Matrix.det.{u_3, u_4} (n := (↑ι : Type u_4))
      ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v)) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have rw : Matrix.det (Matrix.transvection i j 1) = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this_1 : Fintype (↑ι : Type u_4)
this :
  Eq (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    (Matrix.transvection i j 1 : Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
rw : Matrix.det (Matrix.transvection i j 1) = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ Matrix.det.{u_3, u_4} (n := (↑ι : Type u_4))
      ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v)) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have rw₁ : 1 = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this_1 : Fintype (↑ι : Type u_4)
this :
  Eq (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    (Matrix.transvection i j 1 : Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
rw : Matrix.det (Matrix.transvection i j 1) = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
rw₁ : 1 = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ Matrix.det.{u_3, u_4} (n := (↑ι : Type u_4))
      ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v)) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have rw₂ : 1 = HAdd.hAdd (α := K) 1 0
Tactic: rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this_1 : Fintype (↑ι : Type u_4)
this :
  Eq (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    (Matrix.transvection i j 1 : Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
rw : Matrix.det (Matrix.transvection i j 1) = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
rw₁ : 1 = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
rw₂ : 1 = HAdd.hAdd (α := K) 1 0
⊢ Matrix.det.{u_3, u_4} (n := (↑ι : Type u_4))
      ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v)) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have rw₃ : Eq.{u_3 + 1} (α := K) 1 1
Tactic: rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this : Fintype (↑ι : Type u_4)
⊢ Matrix.det.{u_3, u_4} (n := (↑ι : Type u_4))
      ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v)) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have neg : Eq (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
  ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) :
    Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
  (Matrix.transvection i j 1 : Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
Tactic: suffices toMatrix b b (LinearMap.transvection f v) = Matrix.transvection i j 1 by
      rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this : Fintype (↑ι : Type u_4)
⊢ Eq (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    (Matrix.transvection i j 1 : Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
have neg : ∀ (x y : (↑ι : Type u_4)),
  Eq.{u_3 + 1} (α := K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) x y : K)
    (Matrix.transvection i j 1 x y : K)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this : Fintype (↑ι : Type u_4)
x y : (↑ι : Type u_4)
⊢ Eq.{u_3 + 1} (α := K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) x y : K)
    (Matrix.transvection i j 1 x y : K)
have neg : (((b.repr : (a : V) → (↑ι : Type u_4) →₀ K)
          (HAdd.hAdd (α := V) ((b : (a : (↑ι : Type u_4)) → V) y : V)
            (HSMul.hSMul.{u_3, u_4, u_4} (α := K) ((f : (a : V) → K) ((b : (a : (↑ι : Type u_4)) → V) y : V) : K) v)) :
        Finsupp.{u_4, u_3} (↑ι : Type u_4) K) :
      (a : (↑ι : Type u_4)) → K)
    x =
  HAdd.hAdd (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K) (β :=
    Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K) 1 (Matrix.single i j 1) x y
Tactic: rw [toMatrix_apply, transvection.apply, Matrix.transvection]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : Dual K V
v : V
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this : Fintype (↑ι : Type u_4)
x y : (↑ι : Type u_4)
⊢ (((b.repr : (a : V) → (↑ι : Type u_4) →₀ K)
            (HAdd.hAdd (α := V) ((b : (a : (↑ι : Type u_4)) → V) y : V)
              (HSMul.hSMul.{u_3, u_4, u_4} (α := K) ((f : (a : V) → K) ((b : (a : (↑ι : Type u_4)) → V) y : V) : K)
                v)) :
          Finsupp.{u_4, u_3} (↑ι : Type u_4) K) :
        (a : (↑ι : Type u_4)) → K)
      x =
    HAdd.hAdd (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K) (β :=
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K) 1 (Matrix.single i j 1) x y
have neg : HAdd.hAdd (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
    (((Finsupp.single i ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) j) : Finsupp.{u_4, u_3} (↑ι : Type u_4) K) :
          (a : (↑ι : Type u_4)) → K)
        x :
      K) =
  HAdd.hAdd (α := K) (1 x y) (Matrix.single i j 1 x y)
Tactic: simp only [hj.2, Basis.coord_apply, Basis.repr_self, hj.1, map_add, map_smul,
      Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.coe_add, Pi.add_apply, Matrix.add_apply]