awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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)
have neg : Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
Tactic: apply congr_arg₂
-- 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)
neg : Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
⊢ 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)
have neg₁ : Eq.{u_3 + 1} (α := 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)
  (Matrix.single i j 1 x y : K)
Tactic: apply congr_arg₂
-- 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) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
have pos : ∀ (h : x = y), Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
Tactic: by_cases h : 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)
pos : ∀ (h : x = y), Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
⊢ Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
have neg : ∀ (h : ¬x = y), Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
Tactic: by_cases h : 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)
h : x = y
⊢ Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
have pos : Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) y : K) (1 y y : K)
Tactic: rw [h]
-- 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)
h : ¬x = y
⊢ Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
have neg : Eq.{u_3 + 1} (α := K) 0 (1 x y)
Tactic: rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]
-- 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)
h : ¬x = y
neg : Eq.{u_3 + 1} (α := K) 0 (1 x y)
⊢ Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)
have neg₁ : Eq.{u_3 + 1} (α := K) 0 0
Tactic: rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]
-- 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)
    (((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)
    (Matrix.single i j 1 x y : K)
have pos : ∀ (h : i = x ∧ j = y),
  Eq.{u_3 + 1} (α := 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)
    (Matrix.single i j 1 x y : K)
Tactic: by_cases h : i = x ∧ j = 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)
pos :
  ∀ (h : i = x ∧ j = y),
    Eq.{u_3 + 1} (α := 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)
      (Matrix.single i j 1 x y : K)
⊢ Eq.{u_3 + 1} (α := 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)
    (Matrix.single i j 1 x y : K)
have neg : ∀ (h : ¬(i = x ∧ j = y)),
  Eq.{u_3 + 1} (α := 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)
    (Matrix.single i j 1 x y : K)
Tactic: by_cases h : i = x ∧ j = 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)
h : i = x ∧ j = y
⊢ Eq.{u_3 + 1} (α := 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)
    (Matrix.single i j 1 x y : K)
have pos : Eq.{u_3 + 1} (α := K)
  (((Finsupp.single x ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) y) : Finsupp.{u_4, u_3} (↑ι : Type u_4) K) :
        (a : (↑ι : Type u_4)) → K)
      x :
    K)
  (Matrix.single x y 1 x y : K)
Tactic: rw [h.1, h.2]
-- 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)
h : ¬(i = x ∧ j = y)
⊢ Eq.{u_3 + 1} (α := 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)
    (Matrix.single i j 1 x y : K)
have neg : ∀ (h' : ¬i = x),
  Eq.{u_3 + 1} (α := 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)
    (Matrix.single i j 1 x y : K)
Tactic: rcases not_and_or.mp h with h' | h'
-- 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)
h : ¬(i = x ∧ j = y)
neg :
  ∀ (h' : ¬i = x),
    Eq.{u_3 + 1} (α := 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)
      (Matrix.single i j 1 x y : K)
⊢ Eq.{u_3 + 1} (α := 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)
    (Matrix.single i j 1 x y : K)
have neg₁ : ∀ (h' : ¬j = y),
  Eq.{u_3 + 1} (α := 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)
    (Matrix.single i j 1 x y : K)
Tactic: rcases not_and_or.mp h with h' | h'
-- 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 neg : ∀ (ι : Set V) (b : Basis (↑ι : Type u_4) K V) (i : (↑ι : Type u_4)) (hv : v = (b : (a : (↑ι : Type u_4)) → V) i)
  (hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)),
  (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, hv, hf⟩ := exists_basis_of_pairing_ne_zero hfv
-- 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)
ι : Set V
b : Basis (↑ι : Type u_4) K V
i : (↑ι : Type u_4)
hv : v = (b : (a : (↑ι : Type u_4)) → V) i
hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
⊢ (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)
ι : Set V
b : Basis (↑ι : Type u_4) K V
i : (↑ι : Type u_4)
hv : v = (b : (a : (↑ι : Type u_4)) → V) i
hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
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)
ι : Set V
b : Basis (↑ι : Type u_4) K V
i : (↑ι : Type u_4)
hv : v = (b : (a : (↑ι : Type u_4)) → V) i
hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
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.diagonal
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
          (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K))) :
      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.diagonal
      (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
        (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)))) =
  HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: rw [this]
-- 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)
ι : Set V
b : Basis (↑ι : Type u_4) K V
i : (↑ι : Type u_4)
hv : v = (b : (a : (↑ι : Type u_4)) → V) i
hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
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.diagonal
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
          (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K))) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
⊢ Matrix.det
      (Matrix.diagonal
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
          (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)))) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have simp : ∏ i_1 : (↑ι : Type u_4),
    Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
      (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i_1 =
  HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: simp only [Matrix.det_diagonal]
-- 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)
ι : Set V
b : Basis (↑ι : Type u_4) K V
i : (↑ι : Type u_4)
hv : v = (b : (a : (↑ι : Type u_4)) → V) i
hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
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.diagonal
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
          (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K))) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
⊢ ∏ i_1 : (↑ι : Type u_4),
      Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
        (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i_1 =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have rw : Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K))
    i =
  HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: rw [Finset.prod_eq_single i]
-- 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)
ι : Set V
b : Basis (↑ι : Type u_4) K V
i : (↑ι : Type u_4)
hv : v = (b : (a : (↑ι : Type u_4)) → V) i
hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
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.diagonal
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
          (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K))) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
rw :
  Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
      (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ ∏ i_1 : (↑ι : Type u_4),
      Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
        (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i_1 =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have h₀ : ∀ (b : (↑ι : Type u_4)),
  Membership.mem (γ := Finset (↑ι : Type u_4)) Finset.univ b →
    b ≠ i →
      Eq.{u_3 + 1} (α := K)
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
            (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) b :
          K)
        (1 : K)
Tactic: rw [Finset.prod_eq_single i]
-- 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)
ι : Set V
b : Basis (↑ι : Type u_4) K V
i : (↑ι : Type u_4)
hv : v = (b : (a : (↑ι : Type u_4)) → V) i
hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
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.diagonal
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
          (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K))) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
rw :
  Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
      (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
h₀ :
  ∀ (b : (↑ι : Type u_4)),
    Membership.mem (γ := Finset (↑ι : Type u_4)) Finset.univ b →
      b ≠ i →
        Eq.{u_3 + 1} (α := K)
          (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
              (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) b :
            K)
          (1 : K)
⊢ ∏ i_1 : (↑ι : Type u_4),
      Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
        (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i_1 =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
have h₁ : i ∉ Finset.univ →
  Eq.{u_3 + 1} (α := K)
    (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
        (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i :
      K)
    (1 : K)
Tactic: rw [Finset.prod_eq_single i]
-- 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)
ι : Set V
b : Basis (↑ι : Type u_4) K V
i : (↑ι : Type u_4)
hv : v = (b : (a : (↑ι : Type u_4)) → V) i
hf : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
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.diagonal
      (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
        (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K))) :
    Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
Tactic: suffices toMatrix b b (transvection f v) =
      Matrix.diagonal (Function.update 1 i (1 + f v)) by
      rw [this]
      simp only [Matrix.det_diagonal]
      rw [Finset.prod_eq_single i]
      · simp
      · intro j _ hj
        simp [Function.update_of_ne hj]
      · simp