awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
rw :
  HMul.hMul (α := R) ((f : (a : V) → R) x : R)
      (1 + ((↑(-h.unit⁻¹) : R) + HMul.hMul (β := R) (↑(-h.unit⁻¹) : R) ((f : (a : V) → R) v : R))) =
    0
⊢ HMul.hMul (α := R) ((f : (a : V) → R) x : R)
      ((↑(-h.unit⁻¹) : R) + (1 + HMul.hMul (β := R) (↑(-h.unit⁻¹) : R) ((f : (a : V) → R) v : R))) =
    0

Tactic:
rw [← add_assoc, add_comm _ 1, add_assoc]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- 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 : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
nth_rewrite :
  HMul.hMul (α := R) ((f : (a : V) → R) x : R)
      (1 + (↑(-h.unit⁻¹) : R) * HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)) =
    0
⊢ HMul.hMul (α := R) ((f : (a : V) → R) x : R)
      (1 + ((↑(-h.unit⁻¹) : R) + HMul.hMul (β := R) (↑(-h.unit⁻¹) : R) ((f : (a : V) → R) v : R))) =
    0

Tactic:
nth_rewrite 1 [← mul_one (-h.unit⁻¹), Units.val_mul, Units.val_one, ← mul_add]

Premises used: Inv.inv, Units.val_one, IsUnit.unit, mul_add, mul_one, Units.val_mul, Neg.neg
-- 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 : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
⊢ HMul.hMul (α := R) ((f : (a : V) → R) x : R)
      (1 + (↑(-h.unit⁻¹) : R) * HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)) =
    0

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 : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
⊢ (↑(dilatransvection 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 : V
h : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
x : V
⊢ (dilatransvection h : (a : V) → V) x = x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : V) → R) x : R) v

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

Premises used: LinearMap.transvection.apply, LinearEquiv.dilatransvection
-- 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 : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
⊢ (↑(dilatransvection h) : V →ₗ[R] V) = LinearMap.transvection f 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 : IsUnit (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R))
⊢ ∃ (f_1 : Dual R V) (v_1 : V), (↑(dilatransvection h) : V →ₗ[R] V) = LinearMap.transvection f_1 v_1

Tactic:
refine ⟨f, v, by 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
⊢ Monotone.{0, u_2} (β := Set (V ≃ₗ[R] V)) fun (n : ℕ) ↦ HPow.hPow (α := Set (V ≃ₗ[R] V)) (dilatransvections R V) n

Tactic:
Set.pow_right_monotone one_mem_dilatransvections

Premises used: Set.pow_right_monotone, LinearEquiv.one_mem_dilatransvections
-- 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
e : V ≃ₗ[K] V
mp :
  Membership.mem (γ := Set (V ≃ₗ[K] V))
      {e : V ≃ₗ[K] V | ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v} e →
    Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
mpr :
  Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1 →
    Membership.mem (γ := Set (V ≃ₗ[K] V))
      {e : V ≃ₗ[K] V | ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v} e
⊢ Membership.mem (γ := Set (V ≃ₗ[K] V))
      {e : V ≃ₗ[K] V | ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v} e ↔
    Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1

Tactic:
constructor
-- 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
e : V ≃ₗ[K] V
f : Dual K V
v : V
he : (↑e : V →ₗ[K] V) = LinearMap.transvection f v
mp : Module.rank K ↥(K ∙ v) ≤ 1
apply : ((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ K ∙ v
⊢ Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1

Tactic:
apply le_trans (rank_mono (t := K ∙ v) ?_)

Premises used: Submodule.rank_mono, le_trans
-- 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
e : V ≃ₗ[K] V
f : Dual K V
v : V
he : (↑e : V →ₗ[K] V) = LinearMap.transvection f v
⊢ Cardinal.mk (↑{v} : Type u_2) ≤ 1

Tactic:
simp
-- 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
e : V ≃ₗ[K] V
f : Dual K V
v : V
he : (↑e : V →ₗ[K] V) = LinearMap.transvection f v
⊢ Module.rank K ↥(K ∙ v) ≤ 1

Tactic:
apply le_trans (rank_span_le _) (by simp)

Premises used: rank_span_le, le_trans
-- 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
e : V ≃ₗ[K] V
f : Dual K V
v : V
he : (↑e : V →ₗ[K] V) = LinearMap.transvection f v
x : V
⊢ Membership.mem (α := V) (γ := Submodule K V) (K ∙ v) (((↑e : V →ₗ[K] V) - LinearMap.id : (a : V) → V) x : V)

Tactic:
simp [mem_span_singleton, he, LinearMap.transvection.apply]

Premises used: Submodule.mem_span_singleton, LinearMap.transvection.apply
-- 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
e : V ≃ₗ[K] V
he : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
⊢ let u := (↑e : V →ₗ[K] V) - LinearMap.id;
  Module.rank K ↥u.range ≤ 1

Tactic:
set u := (e : V →ₗ[K] V) - LinearMap.id with hu

Premises used: LinearMap.id, LinearEquiv.toLinearMap
-- 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
e : V ≃ₗ[K] V
he : Module.rank K ↥((↑e : V →ₗ[K] V) - LinearMap.id).range ≤ 1
he₁ :
  let u := (↑e : V →ₗ[K] V) - LinearMap.id;
  Module.rank K ↥u.range ≤ 1
⊢ let u := (↑e : V →ₗ[K] V) - LinearMap.id;
  u = (↑e : V →ₗ[K] V) - LinearMap.id

Tactic:
set u := (e : V →ₗ[K] V) - LinearMap.id with hu

Premises used: LinearMap.id, LinearEquiv.toLinearMap
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u = (↑e : V →ₗ[K] V) - LinearMap.id
⊢ u + LinearMap.id = (↑e : V →ₗ[K] V)

Tactic:
rw [eq_sub_iff_add_eq] at hu

Premises used: eq_sub_iff_add_eq
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
pos : ∀ (hr : Module.rank K ↥u.range = 0), ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
neg : ∀ (hr : ¬Module.rank K ↥u.range = 0), ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v

Tactic:
by_cases hr : Module.rank K (range u) = 0

Premises used: Membership.mem, LinearMap.range, Subtype, Module.rank
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
h : (↑e : V →ₗ[K] V) = LinearMap.transvection 0 0
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v

Tactic:
use 0, 0
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
h : ∀ (x : V), Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V) ((LinearMap.transvection 0 0 : (a : V) → V) x : V)
⊢ (↑e : V →ₗ[K] V) = LinearMap.transvection 0 0

Tactic:
ext x
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
x : V
this : Eq (α := V) ((u : (a : V) → V) x : V) (0 : V)
⊢ Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V) ((LinearMap.transvection 0 0 : (a : V) → V) x : V)

Tactic:
simp [← hu, this]
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
x : V
h : Eq (α := V) ((u : (a : V) → V) x : V) (0 : V)
⊢ Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V) ((LinearMap.transvection 0 0 : (a : V) → V) x : V)

Tactic:
suffices u x = 0 by simp [← hu, this]
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Module.rank K ↥u.range = 0
x : V
h : ∀ (hr : Subsingleton.{u_2 + 1} ↥u.range) (x : V), Eq (α := V) ((u : (a : V) → V) x : V) (0 : V)
⊢ Eq (α := V) ((u : (a : V) → V) x : V) (0 : V)

Tactic:
rw [rank_zero_iff] at hr

Premises used: rank_zero_iff
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : Subsingleton.{u_2 + 1} ↥u.range
x : V
⊢ Eq (α := V) ((u : (a : V) → V) x : V) (0 : V)

Tactic:
simpa [← Subtype.coe_inj] using Subsingleton.allEq (⟨u x , mem_range_self u x⟩ : range u) 0

Premises used: Subtype.coe_inj, LinearMap.mem_range_self, Subtype.mk, Subsingleton.allEq, OfNat.ofNat, DFunLike.coe
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : ¬Module.rank K ↥u.range = 0
⊢ 1 ≤ Module.rank K ↥u.range

Tactic:
rw [← ne_eq, ← Cardinal.one_le_iff_ne_zero] at hr

Premises used: Cardinal.one_le_iff_ne_zero, ne_eq
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
⊢ Module.rank K ↥u.range = 1

Tactic:
replace he : Module.rank K (range u) = 1 := le_antisymm he hr
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
he : Module.rank K ↥u.range = 1
⊢ Nonempty (Basis.{0, u_3, u_2} Unit K ↥u.range)

Tactic:
rw [rank_eq_one_iff_finrank_eq_one, finrank_eq_one_iff Unit] at he

Premises used: finrank_eq_one_iff, Unit, Module.rank_eq_one_iff_finrank_eq_one
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
he : Nonempty (Basis.{0, u_3, u_2} Unit K ↥u.range)
neg :
  ∀ (b : Basis.{0, u_3, u_2} Unit K ↥u.range), ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v

Tactic:
obtain ⟨b⟩ := he
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
h : (↑e : V →ₗ[K] V) = (b.coord default ∘ₗ u.rangeRestrict).transvection (↑((b : (a : Unit) → ↥u.range) default) : V)
⊢ ∃ (f : Dual K V) (v : V), (↑e : V →ₗ[K] V) = LinearMap.transvection f v

Tactic:
use (b.coord default) ∘ₗ u.rangeRestrict, b default

Premises used: Inhabited.default, Module.Basis.coord, LinearMap.rangeRestrict, DFunLike.coe
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
h :
  ∀ (x : V),
    Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V)
      (((b.coord default ∘ₗ u.rangeRestrict).transvection (↑((b : (a : Unit) → ↥u.range) default) : V) : (a : V) → V)
          x :
        V)
⊢ (↑e : V →ₗ[K] V) = (b.coord default ∘ₗ u.rangeRestrict).transvection (↑((b : (a : Unit) → ↥u.range) default) : V)

Tactic:
ext x
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
h :
  (LinearMap.id + u : (a : V) → V) x =
    x +
      HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V) ((b.coord default ∘ₗ u.rangeRestrict : (a : V) → K) x : K)
        (↑((b : (a : Unit) → ↥u.range) default) : V)
⊢ Eq (α := V) (((↑e : V →ₗ[K] V) : (a : V) → V) x : V)
    (((b.coord default ∘ₗ u.rangeRestrict).transvection (↑((b : (a : Unit) → ↥u.range) default) : V) : (a : V) → V) x :
      V)

Tactic:
rw [← hu, LinearMap.transvection.apply, add_comm]

Premises used: LinearMap.transvection.apply, add_comm
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this :
  (u : (a : V) → V) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      (↑((b : (a : Unit) → ↥u.range) default) : V)
⊢ (LinearMap.id + u : (a : V) → V) x =
    x +
      HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V) ((b.coord default ∘ₗ u.rangeRestrict : (a : V) → K) x : K)
        (↑((b : (a : Unit) → ↥u.range) default) : V)

Tactic:
simp [this]
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
h :
  (u : (a : V) → V) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      (↑((b : (a : Unit) → ↥u.range) default) : V)
⊢ (LinearMap.id + u : (a : V) → V) x =
    x +
      HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V) ((b.coord default ∘ₗ u.rangeRestrict : (a : V) → K) x : K)
        (↑((b : (a : Unit) → ↥u.range) default) : V)

Tactic:
suffices u x = b.repr (u.rangeRestrict x) default • b default by
      simp [this]
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
rw :
  (u.rangeRestrict : (a : V) → ↥u.range) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      ((b : (a : Unit) → ↥u.range) default : ↥u.range)
⊢ (u : (a : V) → V) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      (↑((b : (a : Unit) → ↥u.range) default) : V)

Tactic:
rw [← this, ← Submodule.coe_smul, Subtype.coe_inj]

Premises used: Subtype.coe_inj, Submodule.coe_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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
nth_rewrite :
  (Finsupp.linearCombination K (⇑b : (a : Unit) → ↥u.range) : (a : Unit →₀ K) → ↥u.range)
      ((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x)) =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      ((b : (a : Unit) → ↥u.range) default : ↥u.range)
⊢ (u.rangeRestrict : (a : V) → ↥u.range) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      ((b : (a : Unit) → ↥u.range) default : ↥u.range)

Tactic:
nth_rewrite 1 [← b.linearCombination_repr (u.rangeRestrict x)]

Premises used: LinearMap.rangeRestrict, Module.Basis.linearCombination_repr, DFunLike.coe
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
h₀ :
  ∀ (b_1 : Unit),
    Ne.{u_3 + 1} (α := K)
        ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) :
              (a : Unit) → K)
            b_1 :
          K)
        (0 : K) →
      b_1 ≠ default →
        HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
            ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) :
                  (a : Unit) → K)
                b_1 :
              K)
            ((b : (a : Unit) → ↥u.range) b_1 : ↥u.range) =
          0
h₁ :
  Eq.{u_3 + 1} (α := K)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      (0 : K) →
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range) 0 ((b : (a : Unit) → ↥u.range) default : ↥u.range) = 0
⊢ (Finsupp.linearCombination K (⇑b : (a : Unit) → ↥u.range) : (a : Unit →₀ K) → ↥u.range)
      ((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x)) =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      ((b : (a : Unit) → ↥u.range) default : ↥u.range)

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum_eq_single default]

Premises used: Inhabited.default, Finsupp.linearCombination_apply, Finsupp.sum_eq_single
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
⊢ ∀ (b_1 : Unit),
    Ne.{u_3 + 1} (α := K)
        ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) :
              (a : Unit) → K)
            b_1 :
          K)
        (0 : K) →
      b_1 ≠ default →
        HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range)
            ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) :
                  (a : Unit) → K)
                b_1 :
              K)
            ((b : (a : Unit) → ↥u.range) b_1 : ↥u.range) =
          0

Tactic:
simp
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
this : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
⊢ Eq.{u_3 + 1} (α := K)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      (0 : K) →
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := ↥u.range) 0 ((b : (a : Unit) → ↥u.range) default : ↥u.range) = 0

Tactic:
simp
-- 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
e : V ≃ₗ[K] V
u : V →ₗ[K] V := (↑e : V →ₗ[K] V) - LinearMap.id
hu : u + LinearMap.id = (↑e : V →ₗ[K] V)
hr : 1 ≤ Module.rank K ↥u.range
b : Basis.{0, u_3, u_2} Unit K ↥u.range
x : V
h : Eq (α := V) ((↑((u.rangeRestrict : (a : V) → ↥u.range) x) : V) : V) ((u : (a : V) → V) x : V)
⊢ (u : (a : V) → V) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := K) (β := V)
      ((((b.repr : (a : ↥u.range) → Unit →₀ K) ((u.rangeRestrict : (a : V) → ↥u.range) x) : Unit →₀ K) : (a : Unit) → K)
          default :
        K)
      (↑((b : (a : Unit) → ↥u.range) default) : V)

Tactic:
suffices u.rangeRestrict x = u x by
      rw [← this, ← Submodule.coe_smul, Subtype.coe_inj]
      nth_rewrite 1 [← b.linearCombination_repr (u.rangeRestrict x)]
      rw [Finsupp.linearCombination_apply, Finsupp.sum_eq_single default] <;> simp