awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
this : HSub.hSub (α := V) ((e : (a : V) → V) w : V) w ∈ ker f
⊢ HSub.hSub (α := K) (β := K) ((f : (a : V) → K) ((e : (a : V) → V) w : V) : K) ((f : (a : V) → K) w : K) = 0

Tactic:
simp only [LinearMap.mem_ker, map_sub] at this

Premises used: map_sub, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
this : HSub.hSub (α := K) (β := K) ((f : (a : V) → K) ((e : (a : V) → V) w : V) : K) ((f : (a : V) → K) w : K) = 0
⊢ Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)

Tactic:
simp only [v, LinearMap.map_smul, map_sub, this, smul_zero]

Premises used: map_sub, smul_zero, LinearMap.map_smul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
neg : HSub.hSub (α := V) ((e : (a : V) → V) w : V) w ∈ ker f
⊢ Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)

Tactic:
suffices e w - w ∈ LinearMap.ker f by
      simp only [LinearMap.mem_ker, map_sub] at this
      simp only [v, LinearMap.map_smul, map_sub, this, smul_zero]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
neg :
  Eq (α := V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
    (((↑e : V →ₗ[K] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
        (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w) :
      V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
    (0 : V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
⊢ HSub.hSub (α := V) ((e : (a : V) → V) w : V) w ∈ ker f

Tactic:
rw [← hf', ← Submodule.ker_mkQ e.fixedSubmodule, LinearMap.mem_ker]

Premises used: LinearMap.mem_ker, LinearEquiv.toLinearMap, LinearMap.fixedSubmodule, Submodule.ker_mkQ
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
V : Type u_2
inst : AddCommGroup V
K : Type u_3
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Module.Finite K V
e : V ≃ₗ[K] V
h : Membership.mem (γ := Set (V ≃ₗ[K] V)) (dilatransvections K V) e ∧ e.fixedReduce = 1
he : finrank.{u_3, u_2} K (V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e : V →ₗ[K] V).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e : V →ₗ[K] V).fixedSubmodule
f : Dual K V
hfw : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) w : K) (0 : K)
hf : map f (↑e : V →ₗ[K] V).fixedSubmodule = ⊥
hf' : (↑e : V →ₗ[K] V).fixedSubmodule = ker f
eq_top : (↑e : V →ₗ[K] V).fixedSubmodule ⊔ K ∙ w = ⊤
v : V :=
  HSMul.hSMul.{u_3, u_2, u_2} (α := K) (((f : (a : V) → K) w)⁻¹ : K) (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w)
⊢ Eq (α := V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
    (((↑e : V →ₗ[K] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
        (HSub.hSub (α := V) ((e : (a : V) → V) w : V) w) :
      V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)
    (0 : V ⧸ (↑e : V →ₗ[K] V).fixedSubmodule)

Tactic:
simp [Submodule.mkQ_apply, Submodule.Quotient.mk_sub, ← fixedReduce_mk, he']

Premises used: Submodule.Quotient.mk_sub, Submodule.mkQ_apply, LinearEquiv.fixedReduce_mk
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : Dual R V
v : V
a :
  ∀ (x : V),
    Eq (α := A ⊗[R] V)
      ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A (transvection f v)) :
                  A →ₗ[A] V →ₗ[R] A ⊗[R] V) :
                (a : A) → V →ₗ[R] A ⊗[R] V)
              1 :
            (a : V) → A ⊗[R] V)
          x :
        A ⊗[R] V)
      ((((TensorProduct.AlgebraTensorModule.curry
                    (transvection ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (1 ⊗ₜ[R] v)) :
                  A →ₗ[A] V →ₗ[R] A ⊗[R] V) :
                (a : A) → V →ₗ[R] A ⊗[R] V)
              1 :
            (a : V) → A ⊗[R] V)
          x :
        A ⊗[R] V)
⊢ Eq (α := A ⊗[R] V →ₗ[A] A ⊗[R] V) (LinearMap.baseChange A (transvection f v))
    (transvection ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (1 ⊗ₜ[R] v))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : Dual R V
v x : V
⊢ Eq (α := A ⊗[R] V)
    ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A (transvection f v)) :
                A →ₗ[A] V →ₗ[R] A ⊗[R] V) :
              (a : A) → V →ₗ[R] A ⊗[R] V)
            1 :
          (a : V) → A ⊗[R] V)
        x :
      A ⊗[R] V)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (transvection ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (1 ⊗ₜ[R] v)) :
                A →ₗ[A] V →ₗ[R] A ⊗[R] V) :
              (a : A) → V →ₗ[R] A ⊗[R] V)
            1 :
          (a : V) → A ⊗[R] V)
        x :
      A ⊗[R] V)

Tactic:
simp [transvection, TensorProduct.tmul_add]

Premises used: LinearMap.transvection, TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
h :
  ∀ (w : W),
    Eq (α := W)
      ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
      (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
            (a : W) → W)
          w :
        W)
⊢ Eq.{u_6 + 1} (α := W →ₗ[A] W) ((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W)
    (LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W)

Tactic:
ext w
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
⊢ Eq.{u_6 + 1} (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) 0 : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        0 :
      W)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
x y : W
hx :
  Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) x : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        x :
      W)
hy :
  Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) y : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        y :
      W)
⊢ Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) (x + y) : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        (x + y) :
      W)

Tactic:
simp [hx, hy]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
a : A
w : W
hw :
  Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) w : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        w :
      W)
⊢ Eq (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W) (a • w) : W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        (a • w) :
      W)

Tactic:
simp [hw]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
W : Type u_6
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module A W
inst_8 : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v x : V
⊢ Eq.{u_6 + 1} (α := W)
    ((((ibc.endHom : (a : V →ₗ[R] V) → W →ₗ[A] W) (LinearMap.transvection f v) : W →ₗ[A] W) : (a : W) → W)
        ((ε : (a : V) → W) x : W) :
      W)
    (((LinearMap.transvection ((ibc.toDual : (a : Dual R V) → Dual A W) f) ((ε : (a : V) → W) v) : W →ₗ[A] W) :
          (a : W) → W)
        ((ε : (a : V) → W) x : W) :
      W)

Tactic:
simp [LinearMap.transvection.apply, endHom_comp_apply, toDual_comp_apply]

Premises used: LinearMap.transvection.apply, IsBaseChange.toDual_comp_apply, IsBaseChange.endHom_comp_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : CommRing A
inst_4 : Algebra R A
f : Dual R V
v : V
h : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hA :
  Eq.{u_5 + 1} (α := A)
    ((((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f : Dual A (A ⊗[R] V)) : (a : A ⊗[R] V) → A)
        (1 ⊗ₜ[R] v) :
      A)
    (0 : A)
⊢ Eq (α := A ⊗[R] V ≃ₗ[A] A ⊗[R] V) (LinearEquiv.baseChange R A V V (transvection h))
    (transvection (R := A) (V := A ⊗[R] V) (f := (Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (v :=
      1 ⊗ₜ[R] v) hA)

Tactic:
simp [← toLinearMap_inj, coe_baseChange,
    LinearEquiv.transvection.coe_toLinearMap, LinearMap.transvection.baseChange]

Premises used: LinearEquiv.coe_baseChange, LinearEquiv.toLinearMap_inj, LinearEquiv.transvection.coe_toLinearMap, LinearMap.transvection.baseChange
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : CommRing A
inst_4 : Algebra R A
e : V ≃ₗ[R] V
he : Membership.mem (γ := Set (V ≃ₗ[R] V)) (dilatransvections R V) e
obtain :
  ∀ (f : Dual R V) (v : V) (he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v),
    Membership.mem (γ := Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V)) (dilatransvections A (A ⊗[R] V) : Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V))
      (LinearEquiv.baseChange R A V V e)
⊢ Membership.mem (γ := Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V)) (dilatransvections A (A ⊗[R] V) : Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V))
    (LinearEquiv.baseChange R A V V e)

Tactic:
obtain ⟨f, v, he⟩ := he
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : CommRing A
inst_4 : Algebra R A
e : V ≃ₗ[R] V
f : Dual R V
v : V
he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v
h :
  Eq (α := A ⊗[R] V →ₗ[A] A ⊗[R] V) (↑(LinearEquiv.baseChange R A V V e) : A ⊗[R] V →ₗ[A] A ⊗[R] V)
    (LinearMap.transvection ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (1 ⊗ₜ[R] v))
⊢ Membership.mem (γ := Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V)) (dilatransvections A (A ⊗[R] V) : Set (A ⊗[R] V ≃ₗ[A] A ⊗[R] V))
    (LinearEquiv.baseChange R A V V e)

Tactic:
use (f.baseChange A), (1 ⊗ₜ[R] v)

Premises used: Module.Dual.baseChange, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : CommRing A
inst_4 : Algebra R A
e : V ≃ₗ[R] V
f : Dual R V
v : V
he : (↑e : V →ₗ[R] V) = LinearMap.transvection f v
⊢ Eq (α := A ⊗[R] V →ₗ[A] A ⊗[R] V) (↑(LinearEquiv.baseChange R A V V e) : A ⊗[R] V →ₗ[A] A ⊗[R] V)
    (LinearMap.transvection ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) (1 ⊗ₜ[R] v))

Tactic:
simp [he, LinearMap.transvection.baseChange]

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

Tactic:
by_cases hfv : f v = 0

Premises used: DFunLike.coe
-- 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)
pos :
  ∀ (hv : v = 0),
    (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
neg :
  ∀ (hv : ¬v = 0),
    (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)

Tactic:
by_cases hv : v = 0
-- 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
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)

Tactic:
simp [hv]
-- 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
pos :
  ∀ (hf : f = 0),
    (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
neg :
  ∀ (hf : ¬f = 0),
    (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)

Tactic:
by_cases hf : f = 0
-- 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
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)

Tactic:
simp [hf]
-- 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
neg :
  ∀ (ι : Set V) (b : Basis (↑ι : Type u_4) K V) (i j : (↑ι : Type u_4)) (hi : i ≠ j)
    (hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j),
    (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
      HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) (transvection f v) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)

Tactic:
obtain ⟨ι, b, i, j, hi, hj⟩ := exists_basis_of_pairing_eq_zero hfv hf hv

Premises used: exists_basis_of_pairing_eq_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)
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
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)
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 :
  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)
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι : Type u_4) K V
i j : (↑ι : Type u_4)
hi : i ≠ j
hj : v = (b : (a : (↑ι : Type u_4)) → V) i ∧ f = b.coord j
this_1 : Fintype (↑ι : Type u_4)
this :
  Eq (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    (Matrix.transvection i j 1 : Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
rw : Matrix.det (Matrix.transvection i j 1) = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
rw₁ : 1 = HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)
rw₂ : 1 = HAdd.hAdd (α := K) 1 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := K) 1 1
⊢ 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, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]

Premises used: Matrix.det_transvection_of_ne, add_zero, OfNat.ofNat
-- 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 :
  Eq (α := Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v) :
      Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
    (Matrix.transvection i j 1 : Matrix.{u_4, u_4, u_3} (↑ι : Type u_4) (↑ι : Type u_4) K)
⊢ Matrix.det.{u_3, u_4} (n := (↑ι : Type u_4))
      ((toMatrix b b : (a : V →ₗ[K] V) → Matrix (↑ι : Type u_4) (↑ι : Type u_4) K) (transvection f v)) =
    HAdd.hAdd (α := K) (β := K) (1 : K) ((f : (a : V) → K) v : K)

Tactic:
suffices toMatrix b b (LinearMap.transvection f v) = Matrix.transvection i j 1 by
      rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]