awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
⊢ ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)

Tactic:
have h2 (i) (his : i ∈ s) : ∃ y, i y ≠ a y := by
    by_contra! hia
    obtain rfl : i = a := MonoidHom.ext hia
    contradiction
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
i : G →* L
his : i ∈ s
let : ∀ (y : G) (hy : Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)), g i = 0
⊢ g i = 0

Tactic:
let ⟨y, hy⟩ := h2 i his
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
i : G →* L
his : i ∈ s
y : G
hy : Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
⊢ HSMul.hSMul (β := L) (g i) ((i : (a : G) → L) y : L) = HSMul.hSMul (β := L) (g i) ((a : (a : G) → L) y : L)

Tactic:
have h : g i • i y = g i • a y := congr_fun (h1 i his) y
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
i : G →* L
his : i ∈ s
y : G
hy : Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h : HSMul.hSMul (β := L) (g i) ((i : (a : G) → L) y : L) = HSMul.hSMul (β := L) (g i) ((a : (a : G) → L) y : L)
⊢ g i = 0 ∨ HSub.hSub (α := L) (β := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L) = 0

Tactic:
rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h

Premises used: sub_eq_zero, smul_sub, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
i : G →* L
his : i ∈ s
y : G
hy : Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h : g i = 0 ∨ HSub.hSub (α := L) (β := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L) = 0
⊢ g i = 0

Tactic:
h.resolve_right (sub_ne_zero_of_ne hy)

Premises used: sub_ne_zero_of_ne, Or.resolve_right
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
i : G →* L
his : i ∈ s
y : G
hy : Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h : g i = 0 ∨ HSub.hSub (α := L) (β := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L) = 0
⊢ g i = 0

Tactic:
exact h.resolve_right (sub_ne_zero_of_ne hy)

Premises used: sub_ne_zero_of_ne, Or.resolve_right
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
⊢ ∀ (i : G →* L) (his : i ∈ s), g i = 0

Tactic:
have h3 (i) (his : i ∈ s) : g i = 0 := by
    let ⟨y, hy⟩ := h2 i his
    have h : g i • i y = g i • a y := congr_fun (h1 i his) y
    rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h
    exact h.resolve_right (sub_ne_zero_of_ne hy)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
rw : HMul.hMul (β := L) (g a) ((a : (a : G) → L) 1 : L) = HSMul.hSMul (β := (a : G) → L) (g a) (⇑a : (a : G) → L) 1
⊢ g a * 1 = HSMul.hSMul (β := (a : G) → L) (g a) (⇑a : (a : G) → L) 1

Tactic:
rw [← a.map_one]

Premises used: MonoidHom.map_one
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
⊢ HMul.hMul (β := L) (g a) ((a : (a : G) → L) 1 : L) = HSMul.hSMul (β := (a : G) → L) (g a) (⇑a : (a : G) → L) 1

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
rw : ∀ x ∈ s, HSMul.hSMul (β := (a : G) → L) (g x) (⇑x : (a : G) → L) = 0
⊢ HSMul.hSMul (β := (a : G) → L) (g a) (⇑a : (a : G) → L) 1 =
    (∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) 1

Tactic:
rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]

Premises used: Finset.sum_eq_zero, Finset.sum_insert, add_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
⊢ ∀ x ∈ s, HSMul.hSMul (β := (a : G) → L) (g x) (⇑x : (a : G) → L) = 0

Tactic:
simp +contextual [h3]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
rw : Eq.{u_7 + 1} (α := L) (0 1) 0
⊢ Eq.{u_7 + 1} (α := L) ((∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) 1) 0

Tactic:
rw [hg]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
⊢ Eq.{u_7 + 1} (α := L) (0 1) 0

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
⊢ g a = 0

Tactic:
have h4 : g a = 0 :=
    calc
      g a = g a * 1 := (mul_one _).symm
      _ = (g a • a : G → L) 1 := by rw [← a.map_one]; rfl
      _ = (∑ i ∈ insert a s, g i • i : G → L) 1 := by
        rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]
        simp +contextual [h3]
      _ = 0 := by rw [hg]; rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
h4 : g a = 0
⊢ ∀ i ∈ insert a s, g i = 0

Tactic:
(Finset.forall_mem_insert ..).2 ⟨h4, h3⟩

Premises used: Iff.mpr, Finset.forall_mem_insert, And.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
h4 : g a = 0
⊢ ∀ i ∈ insert a s, g i = 0

Tactic:
exact (Finset.forall_mem_insert ..).2 ⟨h4, h3⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
v : ι → M
inst_5 : Unique ι
⊢ LinearIndependent R v ↔ v default ≠ 0

Tactic:
⟨?_, .of_subsingleton _⟩

Premises used: LinearIndependent.of_subsingleton, Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
v : ι → M
inst_5 : Unique ι
refine : LinearIndependent R v → v default ≠ 0
⊢ LinearIndependent R v ↔ v default ≠ 0

Tactic:
refine ⟨?_, .of_subsingleton _⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
v : ι → M
inst_5 : Unique ι
h : ∀ (l : ι →₀ R), v default = 0 → Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) default : R) (0 : R)
hv : v default = 0
⊢ False

Tactic:
simpa using h (.single default 1) hv

Premises used: Inhabited.default, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
v : ι → M
inst_5 : Unique ι
⊢ LinearIndependent R v → v default ≠ 0

Tactic:
simpa [linearIndependent_iff, Finsupp.linearCombination_unique, Finsupp.ext_iff,
    Unique.forall_iff, or_imp] using fun h hv ↦ by simpa using h (.single default 1) hv

Premises used: or_imp, Unique.forall_iff, Finsupp.linearCombination_unique, linearIndependent_iff, Finsupp.ext_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
v : ι → M
i : ι
⊢ LinearIndepOn R v {i} ↔ v i ≠ 0

Tactic:
⟨fun h ↦ h.ne_zero rfl, .singleton⟩

Premises used: LinearIndepOn.ne_zero, Iff.intro, LinearIndepOn.singleton, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
inl : ∀ (he : IsEmpty ι), LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
inr : ∀ (he : Nonempty ι), LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
obtain (he | he) := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
he : IsEmpty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
simp [linearIndependent_empty_type]

Premises used: linearIndependent_empty_type
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ Subsingleton ι

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
he : Nonempty ι
inr : ∀ (val : Unique ι), LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
obtain ⟨_⟩ := (unique_iff_subsingleton_and_nonempty (α := ι)).2 ⟨by assumption, he⟩

Premises used: Iff.mpr, unique_iff_subsingleton_and_nonempty, And.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
he : Nonempty ι
val : Unique ι
inr : f default ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
rw [linearIndependent_unique_iff]

Premises used: linearIndependent_unique_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
he : Nonempty ι
val : Unique ι
h : f default ≠ 0
i : ι
rwa rwa₁ rwa₂ rwa₃ : f default ≠ 0
⊢ f i ≠ 0

Tactic:
rwa [Unique.eq_default i]

Premises used: Unique.eq_default
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
inst_5 : Subsingleton ι
f : ι → M
he : Nonempty ι
val : Unique ι
⊢ f default ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

Tactic:
exact ⟨fun h i ↦ by rwa [Unique.eq_default i], fun h ↦ h _⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set ι
h : LinearIndepOn R v s
⊢ LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)

Tactic:
h

Premises used: LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ LinearIndependent R v ↔ Injective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
⊢ LinearIndependent R v ↔ Injective (α := ι → R) (β := M) (⇑(Fintype.linearCombination R v) : (a : ι → R) → M)

Tactic:
simp [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearIndependent]

Premises used: LinearIndependent, Finsupp.linearCombination_eq_fintype_linearCombination
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
⊢ Injective v

Tactic:
simpa [comp_def]
    using Injective.comp hv (Finsupp.single_left_injective one_ne_zero)

Premises used: Finsupp.single_left_injective, Function.comp_def, Function.Injective.comp, one_ne_zero