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)
ι : 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
hj : 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:
simp [Function.update_of_ne hj]

Premises used: Function.update_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)
ι : 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 ∉ 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:
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 : Fintype (↑ι : Type u_4)
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)
⊢ 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:
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
-- 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 :
  ∀ (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)
⊢ 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:
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)
ι : 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)
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)
⊢ 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:
rw [toMatrix_apply, transvection.apply, Matrix.diagonal]

Premises used: LinearMap.transvection.apply, Matrix.diagonal, 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)
ι : 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)
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
⊢ 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:
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]

Premises used: map_add, Matrix.of_apply, Pi.add_apply, Finsupp.coe_add, Finsupp.coe_smul, smul_eq_mul, Module.Basis.repr_self, map_smul, Pi.smul_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)
ι : 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)
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
⊢ 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:
rw [hv, Function.update_apply, Basis.repr_self, Pi.one_apply, hf]

Premises used: Pi.one_apply, Function.update_apply, Module.Basis.repr_self
-- 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)
x y : (↑ι : Type u_4)
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
⊢ 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:
simp only [smul_apply, Basis.coord_apply, Basis.repr_self, smul_eq_mul,
      Finsupp.single_eq_same, mul_one]

Premises used: Finsupp.single_eq_same, LinearMap.smul_apply, smul_eq_mul, mul_one, Module.Basis.coord_apply, Module.Basis.repr_self
-- 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)
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
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
⊢ 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:
split_ifs with hxy hxi
-- 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)
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)) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)

Tactic:
simp [← hxy, hxi]
-- 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)
x y : (↑ι : Type u_4)
hxy : x = y
hxi : ¬x = i
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
⊢ 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:
rw [Finsupp.single_eq_of_ne hxi]

Premises used: 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)
ι : 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) (β := K) ((f : (a : V) → K) v : K) ((Finsupp.single y 1 : (a : (↑ι : Type u_4)) → K) i : K) *
        0) =
    1

Tactic:
simp [hxy]
-- 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)
x y : (↑ι : Type u_4)
hxy : ¬x = y
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
⊢ 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:
rw [Finsupp.single_eq_of_ne hxy, zero_add, mul_assoc]

Premises used: mul_assoc, Finsupp.single_eq_of_ne, zero_add
-- 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)
x y : (↑ι : Type u_4)
hxy : ¬x = y
⊢ HMul.hMul (α := K) (β := K) ((f : (a : V) → K) v : K) (0 : K) = 0

Tactic:
mul_zero _

Premises used: MulZeroClass.mul_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)
this : Fintype (↑ι : Type u_4)
x y : (↑ι : Type u_4)
hxy : ¬x = y
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
⊢ 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:
convert! mul_zero _

Premises used: MulZeroClass.mul_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)
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
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
⊢ 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
-- 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)
x y : (↑ι : Type u_4)
hxy : ¬x = y
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:
simp [← hxi, Finsupp.single_eq_of_ne hxy]

Premises used: 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)
ι : 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
⊢ 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:
simp [Finsupp.single_eq_of_ne hxi]

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : IsDomain R
f : Dual R V
v : V
K : Type u_3 := FractionRing R
this : Field K := inferInstance
a :
  Eq (α := K) ((algebraMap R K : (a : R) → K) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v)) : K)
    ((algebraMap R K : (a : R) → K) (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)) : K)
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)

Tactic:
apply FaithfulSMul.algebraMap_injective R K

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : IsDomain R
f : Dual R V
v : V
K : Type u_3 := FractionRing R
this : Field K := inferInstance
⊢ (LinearMap.det : (a : K ⊗[R] V →ₗ[K] K ⊗[R] V) → K)
      (transvection ((Dual.baseChange K : (a : Dual R V) → Dual K (K ⊗[R] V)) f) (1 ⊗ₜ[R] v)) =
    HAdd.hAdd (α := K) (β := K) (1 : K)
      ((((Dual.baseChange K : (a : Dual R V) → Dual K (K ⊗[R] V)) f : Dual K (K ⊗[R] V)) : (a : K ⊗[R] V) → K)
          (1 ⊗ₜ[R] v) :
        K)

Tactic:
have := det_ofField (f.baseChange K) (1 ⊗ₜ[R] v)