awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ 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:
ext x y
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 :
  (((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
⊢ 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:
rw [toMatrix_apply, transvection.apply, Matrix.transvection]

Premises used: LinearMap.transvection.apply, Matrix.transvection, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 :
  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)
⊢ (((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:
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]

Premises used: Matrix.add_apply, map_add, Pi.add_apply, Finsupp.coe_add, And.right, And.left, smul_eq_mul, mul_one, Finsupp.smul_single, Module.Basis.coord_apply, Module.Basis.repr_self, map_smul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ 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:
apply congr_arg₂

Premises used: congr_arg₂
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
neg : ∀ (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)

Tactic:
by_cases h : x = y
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
pos : Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) y : K) (1 y y : K)
⊢ Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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) y : K) (1 y y : K)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
neg₁ neg₂ : Eq.{u_3 + 1} (α := K) 0 0
⊢ Eq.{u_3 + 1} (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K) (1 x y : K)

Tactic:
rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]

Premises used: Matrix.one_apply_ne, Finsupp.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
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)
⊢ 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:
rw [h.1, h.2]

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 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:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ 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'

Premises used: not_and_or, Iff.mp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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:
simp [Finsupp.single_eq_of_ne' h',
            Finsupp.single_eq_of_ne h',
            Matrix.single_apply_of_ne (h := h)]

Premises used: Matrix.single_apply_of_ne, Finsupp.single_eq_of_ne, Finsupp.single_eq_of_ne'
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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:
simp [Finsupp.single_eq_of_ne' h',
            Finsupp.single_eq_of_ne h',
            Matrix.single_apply_of_ne (h := h)]

Premises used: Matrix.single_apply_of_ne, Finsupp.single_eq_of_ne, Finsupp.single_eq_of_ne'
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ (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

Premises used: exists_basis_of_pairing_ne_zero
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ (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
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)

Tactic:
rw [← det_toMatrix b]

Premises used: LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 :
  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)
⊢ 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 [this]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ 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:
simp only [Matrix.det_diagonal]

Premises used: Matrix.det_diagonal
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
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)
⊢ ∏ 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:
rw [Finset.prod_eq_single i]

Premises used: Finset.prod_eq_single
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
j : (↑ι : Type u_4)
h₀ :
  Membership.mem (γ := Finset (↑ι : Type u_4)) Finset.univ j →
    j ≠ 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)) j :
          K)
        (1 : K)
⊢ Membership.mem (γ := Finset (↑ι : Type u_4)) Finset.univ j →
    j ≠ 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)) j :
          K)
        (1 : K)

Tactic:
_