awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
f : Dual R V
v : V
r s : R
x : V
⊢ x +
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) (r • v) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R)
          (s • (v + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) v : R) (r • v)))) =
    x +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R)
        ((r + (s + HMul.hMul (β := R) s ((f : (a : V) → R) v : R) * r)) • v)

Tactic:
simp only [smul_add, ← mul_smul, ← add_smul, ← mul_add (f x), mul_assoc]

Premises used: mul_assoc, add_smul, mul_add, DFunLike.coe, SemigroupAction.mul_smul, smul_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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h1 : finrank R V ≤ 1
0 : ∀ (h : finrank R V = 0) (h1 : LE.le (α := ℕ) 0 1), transvection f v = id
1 : ∀ (h : finrank R V = 1) (h1 : LE.le (α := ℕ) 1 1), transvection f v = id
⊢ transvection f v = id

Tactic:
interval_cases h : finrank R V

Premises used: Module.finrank
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 0
h1 : LE.le (α := ℕ) 0 1
⊢ Subsingleton V

Tactic:
have : Subsingleton V := (finrank_eq_zero_iff_of_free R V).mp h
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 0
h1 : LE.le (α := ℕ) 0 1
this : Subsingleton V
⊢ transvection f v = id

Tactic:
simp [Subsingleton.eq_zero v]

Premises used: Subsingleton.eq_zero
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
1 : ∀ (x : V), Eq (α := V) ((transvection f v : (a : V) → V) x : V) ((id : (a : V) → V) x : V)
⊢ transvection f v = id

Tactic:
ext x
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
this : HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
⊢ Eq (α := V) ((transvection f v : (a : V) → V) x : V) ((id : (a : V) → V) x : V)

Tactic:
simp [apply, this]

Premises used: LinearMap.transvection.apply
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
1 : HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0
⊢ Eq (α := V) ((transvection f v : (a : V) → V) x : V) ((id : (a : V) → V) x : V)

Tactic:
suffices f x • v = 0 by
      simp [apply, this]
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
⊢ 0 < finrank R V

Tactic:
simp [h]
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
this :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R) =
    0

Tactic:
rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv

Premises used: mul_comm, smul_eq_mul, map_smul
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
this :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
hfv₁ :
  HMul.hMul (α := R) (β := R) ((f : (a : V) → R) ((b : (a : Fin (finrank R V)) → V) i : V) : R)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) v : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R) =
    0
⊢ ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)

Tactic:
rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv

Premises used: mul_comm, smul_eq_mul, map_smul
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
1 :
  ∀ (x : V),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : V) → R) x : R) v = 0

Tactic:
suffices ∀ x, x = b.repr x i • (b i) by
      rw [this v, map_smul, smul_eq_mul, mul_comm] at hfv
      rw [this x, this v, map_smul, smul_eq_mul, ← mul_smul, mul_assoc, hfv, mul_zero, zero_smul]
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x_1 : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
x : V
⊢ x =
    ∑ i : Fin (finrank R V),
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)

Tactic:
have : x = ∑ i, b.repr x i • b i := (b.sum_equivFun x).symm
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x_1 : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
x : V
this :
  x =
    ∑ i : Fin (finrank R V),
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
⊢ ∀ (b_1 : Fin (finrank R V)),
    Membership.mem (γ := Finset (Fin (finrank R V))) Finset.univ b_1 →
      b_1 ≠ i →
        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
            ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R)
                b_1 :
              R)
            ((b : (a : Fin (finrank R V)) → V) b_1 : V) =
          0

Tactic:
grind
-- 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
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : StrongRankCondition R
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : finrank R V = 1
h1 : LE.le (α := ℕ) 1 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x_1 : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
x : V
this :
  x =
    ∑ i : Fin (finrank R V),
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
1 h_1 h_2 h_3 :
  ∀
    (this :
      x =
        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
          ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i :
            R)
          ((b : (a : Fin (finrank R V)) → V) i : V)),
    x =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
        ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
        ((b : (a : Fin (finrank R V)) → V) i : V)
⊢ x =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V)
      ((((b.repr : (a : V) → Fin (finrank R V) →₀ R) x : Fin (finrank R V) →₀ R) : (a : Fin (finrank R V)) → R) i : R)
      ((b : (a : Fin (finrank R V)) → V) i : V)

Tactic:
rwa [Finset.sum_eq_single_of_mem i (Finset.mem_univ i) (by grind)] at this

Premises used: Finset.mem_univ, Finset.sum_eq_single_of_mem
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
f : Dual R V
v : V
e : V ≃ₗ[R] W
h :
  ∀ (x : W),
    Eq (α := W) (((↑e : V →ₗ[R] W) ∘ₗ transvection f v ∘ₗ (↑e.symm : W →ₗ[R] V) : (a : W) → W) x : W)
      (((f ∘ₗ (↑e.symm : W →ₗ[R] V)).transvection ((e : (a : V) → W) v) : (a : W) → W) x : W)
⊢ (↑e : V →ₗ[R] W) ∘ₗ transvection f v ∘ₗ (↑e.symm : W →ₗ[R] V) =
    (f ∘ₗ (↑e.symm : W →ₗ[R] V)).transvection ((e : (a : V) → W) v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
f : Dual R V
v : V
e : V ≃ₗ[R] W
x : W
⊢ Eq (α := W) (((↑e : V →ₗ[R] W) ∘ₗ transvection f v ∘ₗ (↑e.symm : W →ₗ[R] V) : (a : W) → W) x : W)
    (((f ∘ₗ (↑e.symm : W →ₗ[R] V)).transvection ((e : (a : V) → W) v) : (a : W) → W) x : W)

Tactic:
simp [transvection.apply]

Premises used: LinearMap.transvection.apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x y : V
⊢ (LinearMap.transvection f v : (a : V) → V) (x + y) =
    HAdd.hAdd (α := V) (β := V) ((LinearMap.transvection f v : (a : V) → V) x : V)
      ((LinearMap.transvection f v : (a : V) → V) y : V)

Tactic:
simp [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
r : R
x : V
⊢ (LinearMap.transvection f v : (a : V) → V) (r • x) =
    HSMul.hSMul (α := R) (β := V) ((RingHom.id R : (a : R) → R) r : R)
      ((LinearMap.transvection f v : (a : V) → V) x : V)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
⊢ (LinearMap.transvection f (-v) : (a : V) → V) ((LinearMap.transvection f v : (a : V) → V) x : V) = x

Tactic:
simp [comp_of_left_eq_apply h]

Premises used: LinearMap.transvection.comp_of_left_eq_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (-v) : R) (0 : R)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (-v) : R) (0 : R)

Tactic:
have h' : f (-v) = 0 := by simp [h]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
h' : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (-v) : R) (0 : R)
⊢ (LinearMap.transvection f v : (a : V) → V) ((LinearMap.transvection f (-v) : (a : V) → V) x : V) = x

Tactic:
simp [comp_of_left_eq_apply h']

Premises used: LinearMap.transvection.comp_of_left_eq_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
⊢ (transvection h : (a : V) → V) x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ (↑(transvection h) : V →ₗ[R] V) = LinearMap.transvection f v

Tactic:
rfl

Premises used: LinearMap.transvection, rfl
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v x : V
h : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ Eq (α := V) ((transvection h : (a : V) → V) x : V) ((LinearMap.transvection f v : (a : V) → V) x : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v w : V
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) w : R) (0 : R)
hvw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (v + w) : R) (0 : R)
h :
  ∀ (x : V),
    Eq (α := V) ((transvection hw ≪≫ₗ transvection hv : (a : V) → V) x : V) ((transvection hvw : (a : V) → V) x : V)
⊢ transvection hw ≪≫ₗ transvection hv = transvection hvw

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v w : V
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) w : R) (0 : R)
hvw : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (v + w) : R) (0 : R)
x : V
⊢ Eq (α := V) ((transvection hw ≪≫ₗ transvection hv : (a : V) → V) x : V) ((transvection hvw : (a : V) → V) x : V)

Tactic:
simp [comp_of_left_eq_apply hw]

Premises used: LinearMap.transvection.comp_of_left_eq_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f g : Dual R V
v : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hg : Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) v : R) (0 : R)
hfg : Eq.{u_1 + 1} (α := R) ((f + g : (a : V) → R) v : R) (0 : R)
h :
  ∀ (x : V),
    Eq (α := V) ((transvection hg ≪≫ₗ transvection hf : (a : V) → V) x : V) ((transvection hfg : (a : V) → V) x : V)
⊢ transvection hg ≪≫ₗ transvection hf = transvection hfg

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f g : Dual R V
v : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hg : Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) v : R) (0 : R)
hfg : Eq.{u_1 + 1} (α := R) ((f + g : (a : V) → R) v : R) (0 : R)
x : V
⊢ Eq (α := V) ((transvection hg ≪≫ₗ transvection hf : (a : V) → V) x : V) ((transvection hfg : (a : V) → V) x : V)

Tactic:
simp [comp_of_right_eq_apply hf]

Premises used: LinearMap.transvection.comp_of_right_eq_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
v : V
hv : Eq.{u_1 + 1} (α := R) ((0 : (a : V) → R) v : R) (0 : R)
h : ∀ (x : V), Eq (α := V) ((transvection hv : (a : V) → V) x : V) ((refl R V : (a : V) → V) x : V)
⊢ transvection hv = refl R V

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
v : V
hv : Eq.{u_1 + 1} (α := R) ((0 : (a : V) → R) v : R) (0 : R)
x : V
⊢ Eq (α := V) ((transvection hv : (a : V) → V) x : V) ((refl R V : (a : V) → V) x : V)

Tactic:
simp [transvection]

Premises used: LinearEquiv.transvection
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) 0 : R) (0 : R)
h : ∀ (x : V), Eq (α := V) ((transvection hf : (a : V) → V) x : V) ((refl R V : (a : V) → V) x : V)
⊢ transvection hf = refl R V

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) 0 : R) (0 : R)
x : V
⊢ Eq (α := V) ((transvection hf : (a : V) → V) x : V) ((refl R V : (a : V) → V) x : V)

Tactic:
simp [transvection]

Premises used: LinearEquiv.transvection
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hv' : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (-v) : R) (0 : R)
h : ∀ (x : V), Eq (α := V) (((transvection hv).symm : (a : V) → V) x : V) ((transvection hv' : (a : V) → V) x : V)
⊢ (transvection hv).symm = transvection hv'

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hv' : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (-v) : R) (0 : R)
x : V
⊢ Eq (α := V) (((transvection hv).symm : (a : V) → V) x : V) ((transvection hv' : (a : V) → V) x : V)

Tactic:
simp [symm_apply_eq, comp_of_left_eq_apply hv']

Premises used: LinearMap.transvection.comp_of_left_eq_apply, LinearEquiv.symm_apply_eq
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hv' : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) (-v) : R) (0 : R)
⊢ (transvection hv)⁻¹ = transvection hv'

Tactic:
symm_eq hv

Premises used: LinearEquiv.transvection.symm_eq
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hf' : Eq.{u_1 + 1} (α := R) ((-f : (a : V) → R) v : R) (0 : R)
h : ∀ (x : V), Eq (α := V) (((transvection hf).symm : (a : V) → V) x : V) ((transvection hf' : (a : V) → V) x : V)
⊢ (transvection hf).symm = transvection hf'

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hf' : Eq.{u_1 + 1} (α := R) ((-f : (a : V) → R) v : R) (0 : R)
x : V
⊢ Eq (α := V) (((transvection hf).symm : (a : V) → V) x : V) ((transvection hf' : (a : V) → V) x : V)

Tactic:
simp [symm_apply_eq, comp_of_right_eq_apply hf]

Premises used: LinearEquiv.symm_apply_eq, LinearMap.transvection.comp_of_right_eq_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hf : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
hf' : Eq.{u_1 + 1} (α := R) ((-f : (a : V) → R) v : R) (0 : R)
⊢ (transvection hf)⁻¹ = transvection hf'

Tactic:
symm_eq' hf

Premises used: LinearEquiv.transvection.symm_eq'
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
⊢ x ∈ (↑(transvection hfv) : V →ₗ[R] V).fixedSubmodule ↔
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v = 0

Tactic:
simp [LinearMap.transvection.apply, add_eq_left]

Premises used: LinearMap.transvection.apply, add_eq_left
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
hx : x ∈ ker f
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)

Tactic:
rw [mem_ker] at hx

Premises used: LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
x : V
hx : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)
⊢ x ∈ (↑(transvection hfv) : V →ₗ[R] V).fixedSubmodule

Tactic:
simp [LinearMap.transvection.apply, hx]

Premises used: LinearMap.transvection.apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
⊢ Membership.mem (γ := Set (V ≃ₗ[R] V)) (transvections R V) e ↔
    ∃ (f : Dual R V) (v : V) (hfv : Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)), e = transvection hfv

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, LinearEquiv.transvections