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)
ι : 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)
⊢ 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)
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.diagonal
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
          (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)))
        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)
ι : 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)
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.diagonal
        (Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
          (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)))
        x y :
      K)
have neg : Eq.{u_3 + 1} (α := K)
  ((((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 :
    K)
  ((Matrix.of : (a : (↑ι : Type u_4) → (↑ι : Type u_4) → K) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K)
      (fun (i_1 j : (↑ι : Type u_4)) ↦
        if i_1 = j then
          Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
            (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i_1
        else 0)
      x y :
    K)
Tactic: rw [toMatrix_apply, transvection.apply, Matrix.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 : Fintype (↑ι : Type u_4)
x y : (↑ι : Type u_4)
⊢ Eq.{u_3 + 1} (α := K)
    ((((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 :
      K)
    ((Matrix.of : (a : (↑ι : Type u_4) → (↑ι : Type u_4) → K) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K)
        (fun (i_1 j : (↑ι : Type u_4)) ↦
          if i_1 = j then
            Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
              (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) i_1
          else 0)
        x y :
      K)
have neg : HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
    (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) ((b : (a : (↑ι : Type u_4)) → V) y : V) : K)
      ((((b.repr : (a : V) → (↑ι : Type u_4) →₀ K) v : Finsupp.{u_4, u_3} (↑ι : Type u_4) K) :
            (a : (↑ι : Type u_4)) → K)
          x :
        K)) =
  if x = y then
    Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
      (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) x
  else 0
Tactic: simp only [map_add, Basis.repr_self, map_smul, Finsupp.coe_add, Finsupp.coe_smul,
      Pi.add_apply, Pi.smul_apply, smul_eq_mul, Matrix.of_apply]
-- 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)
x y : (↑ι : Type u_4)
⊢ HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) ((b : (a : (↑ι : Type u_4)) → V) y : V) : K)
        ((((b.repr : (a : V) → (↑ι : Type u_4) →₀ K) v : Finsupp.{u_4, u_3} (↑ι : Type u_4) K) :
              (a : (↑ι : Type u_4)) → K)
            x :
          K)) =
    if x = y then
      Function.update (β := fun (a : (↑ι : Type u_4)) ↦ K) 1 i
        (HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)) x
    else 0
have neg : HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
    (HMul.hMul (α := K) (β := K)
      ((HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i) : (a : V) → K)
          ((b : (a : (↑ι : Type u_4)) → V) y : V) :
        K)
      ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
  if x = y then
    if x = i then
      HAdd.hAdd (α := K) (β := K) (1 : K)
        ((HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i) : (a : V) → K)
            ((b : (a : (↑ι : Type u_4)) → V) i : V) :
          K)
    else 1
  else 0
Tactic: rw [hv, Function.update_apply, Basis.repr_self, Pi.one_apply, hf]
-- 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)
x y : (↑ι : Type u_4)
⊢ HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (α := K) (β := K)
        ((HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i) : (a : V) → K)
            ((b : (a : (↑ι : Type u_4)) → V) y : V) :
          K)
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    if x = y then
      if x = i then
        HAdd.hAdd (α := K) (β := K) (1 : K)
          ((HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i) : (a : V) → K)
              ((b : (a : (↑ι : Type u_4)) → V) i : V) :
            K)
      else 1
    else 0
have neg : HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
    (HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
      ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
  if x = y then if x = i then HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K) else 1 else 0
Tactic: simp only [smul_apply, Basis.coord_apply, Basis.repr_self, smul_eq_mul,
      Finsupp.single_eq_same, mul_one]
-- 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)
x y : (↑ι : Type u_4)
⊢ HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    if x = y then if x = i then HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K) else 1 else 0
have pos : ∀ (hxy : x = y) (hxi : x = i),
  HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
Tactic: split_ifs with hxy hxi
-- 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)
x y : (↑ι : Type u_4)
pos :
  ∀ (hxy : x = y) (hxi : x = i),
    HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
        (HMul.hMul (β := K)
          (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K)
            ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
          ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    if x = y then if x = i then HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K) else 1 else 0
have neg : ∀ (hxy : x = y) (hxi : ¬x = i),
  HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    1
Tactic: split_ifs with hxy hxi
-- 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)
x y : (↑ι : Type u_4)
pos :
  ∀ (hxy : x = y) (hxi : x = i),
    HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
        (HMul.hMul (β := K)
          (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K)
            ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
          ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
neg :
  ∀ (hxy : x = y) (hxi : ¬x = i),
    HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
        (HMul.hMul (β := K)
          (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K)
            ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
          ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
      1
⊢ HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    if x = y then if x = i then HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K) else 1 else 0
have neg₁ : ∀ (hxy : ¬x = y),
  HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    0
Tactic: split_ifs with hxy hxi
-- 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)
x y : (↑ι : Type u_4)
hxy : x = y
hxi : ¬x = i
⊢ HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    1
have neg : HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
    (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K) *
      0) =
  1
Tactic: rw [Finsupp.single_eq_of_ne hxi]
-- 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)
x y : (↑ι : Type u_4)
hxy : ¬x = y
⊢ HAdd.hAdd (α := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) x : K)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K))
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    0
have neg : HMul.hMul (α := K) ((f : (a : V) → K) v : K)
    (HMul.hMul (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K)
      ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
  0
Tactic: rw [Finsupp.single_eq_of_ne hxy, zero_add, mul_assoc]
-- 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)
x y : (↑ι : Type u_4)
hxy : ¬x = y
⊢ HMul.hMul (α := K) ((f : (a : V) → K) v : K)
      (HMul.hMul (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K)
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K)) =
    0
have h : HMul.hMul (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K)
    ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K) =
  0
Tactic: convert! mul_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)
ι : 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)
x y : (↑ι : Type u_4)
hxy : ¬x = y
⊢ HMul.hMul (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K)
      ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K) =
    0
have pos : ∀ (hxi : x = i),
  HMul.hMul (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K)
      ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K) =
    0
Tactic: by_cases hxi : x = 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)
x y : (↑ι : Type u_4)
hxy : ¬x = y
pos :
  ∀ (hxi : x = i),
    HMul.hMul (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K)
        ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K) =
      0
⊢ HMul.hMul (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K)
      ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K) =
    0
have neg : ∀ (hxi : ¬x = i),
  HMul.hMul (α := K) (β := K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K)
      ((Finsupp.single i 1 : (a : (↑ι : Type u_4)) → K) x : K) =
    0
Tactic: by_cases hxi : x = 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
⊢ (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: classical
  by_cases hfv : f v = 0
  · by_cases hv : v = 0
    · simp [hv]
    by_cases hf : f = 0
    · simp [hf]
    obtain ⟨ι, b, i, j, hi, hj⟩ := exists_basis_of_pairing_eq_zero hfv hf hv
    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
    rw [← det_toMatrix b]
    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]
    ext x y
    rw [toMatrix_apply, transvection.apply, Matrix.transvection]
    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]
    apply congr_arg₂
    · by_cases h : x = y
      · rw [h]; simp
      · rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]
    · by_cases h : i = x ∧ j = y
      · rw [h.1, h.2]; simp
      · rcases not_and_or.mp h with h' | h' <;>
          simp [Finsupp.single_eq_of_ne' h',
            Finsupp.single_eq_of_ne h',
            Matrix.single_apply_of_ne (h := h)]
  · obtain ⟨ι, b, i, hv, hf⟩ := exists_basis_of_pairing_ne_zero hfv
    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
    rw [← det_toMatrix b]
    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
    ext x y
    rw [toMatrix_apply, transvection.apply, Matrix.diagonal]
    simp only [map_add, Basis.repr_self, map_smul, Finsupp.coe_add, Finsupp.coe_smul,
      Pi.add_apply, Pi.smul_apply, smul_eq_mul, Matrix.of_apply]
    rw [hv, Function.update_apply, Basis.repr_self, Pi.one_apply, hf]
    simp only [smul_apply, Basis.coord_apply, Basis.repr_self, smul_eq_mul,
      Finsupp.single_eq_same, mul_one]
    split_ifs with hxy hxi
    · simp [← hxy, hxi]
    · rw [Finsupp.single_eq_of_ne hxi]; simp [hxy]
    · rw [Finsupp.single_eq_of_ne hxy, zero_add, mul_assoc]
      convert! mul_zero _
      by_cases hxi : x = i
      · simp [← hxi, Finsupp.single_eq_of_ne hxy]
      · simp [Finsupp.single_eq_of_ne hxi]
-- 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: classical
  by_cases hfv : f v = 0
  · by_cases hv : v = 0
    · simp [hv]
    by_cases hf : f = 0
    · simp [hf]
    obtain ⟨ι, b, i, j, hi, hj⟩ := exists_basis_of_pairing_eq_zero hfv hf hv
    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
    rw [← det_toMatrix b]
    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]
    ext x y
    rw [toMatrix_apply, transvection.apply, Matrix.transvection]
    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]
    apply congr_arg₂
    · by_cases h : x = y
      · rw [h]; simp
      · rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]
    · by_cases h : i = x ∧ j = y
      · rw [h.1, h.2]; simp
      · rcases not_and_or.mp h with h' | h' <;>
          simp [Finsupp.single_eq_of_ne' h',
            Finsupp.single_eq_of_ne h',
            Matrix.single_apply_of_ne (h := h)]
  · obtain ⟨ι, b, i, hv, hf⟩ := exists_basis_of_pairing_ne_zero hfv
    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
    rw [← det_toMatrix b]
    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
    ext x y
    rw [toMatrix_apply, transvection.apply, Matrix.diagonal]
    simp only [map_add, Basis.repr_self, map_smul, Finsupp.coe_add, Finsupp.coe_smul,
      Pi.add_apply, Pi.smul_apply, smul_eq_mul, Matrix.of_apply]
    rw [hv, Function.update_apply, Basis.repr_self, Pi.one_apply, hf]
    simp only [smul_apply, Basis.coord_apply, Basis.repr_self, smul_eq_mul,
      Finsupp.single_eq_same, mul_one]
    split_ifs with hxy hxi
    · simp [← hxy, hxi]
    · rw [Finsupp.single_eq_of_ne hxi]; simp [hxy]
    · rw [Finsupp.single_eq_of_ne hxy, zero_add, mul_assoc]
      convert! mul_zero _
      by_cases hxi : x = i
      · simp [← hxi, Finsupp.single_eq_of_ne hxy]
      · simp [Finsupp.single_eq_of_ne hxi]