awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndepOn R v s
⊢ InjOn v s

Tactic:
injOn_iff_injective.2 <| LinearIndependent.injective hv

Premises used: Iff.mpr, Set.injOn_iff_injective, LinearIndependent.injective
-- 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
hv : LinearIndependent R v
i : ι
⊢ Injective.{u_2 + 1, u_4 + 1} (α := R) (β := M)
    (comp (β := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) (Finsupp.single i))

Tactic:
hv.comp (Finsupp.single_injective i)

Premises used: Finsupp.single_injective, Function.Injective.comp
-- 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
hv : LinearIndependent R v
i : ι
h : ∀ (x : R), x • v i = comp (β := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) (Finsupp.single i) x
⊢ Injective.{u_2 + 1, u_4 + 1} (β := M) fun (r : R) ↦ r • v i

Tactic:
convert! hv.comp (Finsupp.single_injective i)

Premises used: Finsupp.single_injective, Function.Injective.comp
-- 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
hv : LinearIndependent R v
i : ι
x : R
⊢ x • v i = comp (β := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) (Finsupp.single i) x

Tactic:
simp
-- 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
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) 0 : M)

Tactic:
simpa using 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
inst_3 : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ Eq (α := ι →₀ R) (Finsupp.single i 1) 0

Tactic:
have := @hv (Finsupp.single i 1 : ι →₀ R) 0 (by simpa using 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
inst_3 : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
this : Eq (α := ι →₀ R) (Finsupp.single i 1) 0
⊢ False

Tactic:
simp at this
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
i : ι
hv : LinearIndepOn R v s
hi : i ∈ s
⊢ v i ≠ 0

Tactic:
LinearIndependent.ne_zero ⟨i, hi⟩ hv

Premises used: LinearIndependent.ne_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hs : LinearIndepOn R v s
⊢ 0 ∉ v '' s

Tactic:
fun ⟨_, hi, h0⟩ ↦ hs.ne_zero hi h0

Premises used: False, LinearIndepOn.ne_zero, Not, _private.0.LinearIndepOn.zero_notMem_image.match_1
-- 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 : IsEmpty ι
⊢ LinearIndependent R v

Tactic:
injective_of_subsingleton _

Premises used: Function.injective_of_subsingleton, LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
⊢ LinearIndependent.{u', u_2, u_4} (ι := ι) R (M := M) 0 ↔ IsEmpty ι

Tactic:
⟨fun h ↦ not_nonempty_iff.1 fun ⟨i⟩ ↦ (h.ne_zero i rfl).elim,
    fun _ ↦ linearIndependent_empty_type⟩

Premises used: False, _private.0.linearIndependent_zero_iff.match_1, LinearIndependent.ne_zero, linearIndependent_empty_type, False.elim, not_nonempty_iff, Iff.intro, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
⊢ LinearIndepOn.{u', u_2, u_4} R (M := M) 0 s ↔ s = ∅

Tactic:
linearIndependent_zero_iff.trans isEmpty_coe_sort

Premises used: linearIndependent_zero_iff, Set.isEmpty_coe_sort, Iff.trans, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : Subsingleton M
f : ι → M
rw : LinearIndependent.{u', u_2, u_4} (ι := ι) R (M := M) 0 ↔ IsEmpty ι
rw₁ rw₂ : IsEmpty ι ↔ IsEmpty ι
⊢ LinearIndependent R f ↔ IsEmpty ι

Tactic:
rw [Subsingleton.elim f 0, linearIndependent_zero_iff]

Premises used: linearIndependent_zero_iff, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ LinearIndependent R (M := M) fun (x : (↑∅ : Type u_4)) ↦ (↑x : M)

Tactic:
linearIndependent_empty_type

Premises used: linearIndependent_empty_type
-- 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
⊢ LinearIndepOn R v ∅

Tactic:
linearIndependent_empty_type ..

Premises used: linearIndependent_empty_type, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔ LinearIndepOn R v s

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ LinearIndependent.{u_4, u_2, u_4} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) ↔
    LinearIndepOn R id s

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ LinearIndependent (ι := (↑s : Type u')) R (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔ LinearIndepOn R v s

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
⊢ LinearIndependent R (v ∘ f)

Tactic:
simpa [comp_def] using Injective.comp h (Finsupp.mapDomain_injective hf)

Premises used: Function.comp_def, Function.Injective.comp, Finsupp.mapDomain_injective
-- 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
t s : Set ι
hs : LinearIndepOn R v s
h : t ⊆ s
⊢ LinearIndepOn R v t

Tactic:
hs.comp _ <| Set.inclusion_injective h

Premises used: Set.inclusion_injective, LinearIndependent.comp, 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 ↔
    ∀ (l₁ l₂ : ι →₀ R),
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
          ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
        l₁ = l₂

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearIndependent, Function.Injective
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (∑ i ∈ s, Finsupp.single i (f i)) : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (∑ i ∈ s, Finsupp.single i (g i)) : M)

Tactic:
simpa only [map_sum, Finsupp.linearCombination_single] using eq

Premises used: map_sum, Finsupp.linearCombination_single
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
⊢ Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i))

Tactic:
have h :=
        hv (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i)) <| by
          simpa only [map_sum, Finsupp.linearCombination_single] using eq
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
rw : f i = (Finsupp.single i (f i) : (a : ι) → R) i
rw₁ rw₂ : f i = f i
⊢ f i = (Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single i (f i))

Tactic:
rw [Finsupp.lapply_apply, Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.lapply_apply
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
rw : f i = (Finsupp.single i (f i) : (a : ι) → R) i
rw₁ rw₂ : f i = f i
⊢ f i = (Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single i (f i))

Tactic:
{ rw [Finsupp.lapply_apply, Finsupp.single_eq_same] }

Premises used: Finsupp.single_eq_same, Finsupp.lapply_apply
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f_1 g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f_1 i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f_1 i)) (∑ i ∈ s, Finsupp.single i (g i))
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
rw : Eq.{u_2 + 1} (α := R) ((Finsupp.single j (f j) : (a : ι) → R) i : R) (0 : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) ((Finsupp.lapply i : (a : ι →₀ R) → R) (Finsupp.single j (f j)) : R) (0 : R)

Tactic:
rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji]

Premises used: Finsupp.single_eq_of_ne', Finsupp.lapply_apply
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i))
⊢ ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i

Tactic:
have (f : ι → R) : f i = (∑ j ∈ s, Finsupp.single j (f j)) i :=
        calc
          f i = (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single i (f i)) := by
            { rw [Finsupp.lapply_apply, Finsupp.single_eq_same] }
          _ = ∑ j ∈ s, (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single j (f j)) :=
            Eq.symm <|
              Finset.sum_eq_single i
                (fun j _hjs hji => by rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji])
                fun hnis => hnis.elim his
          _ = (∑ j ∈ s, Finsupp.single j (f j)) i := (map_sum ..).symm
-- 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
hv :
  ∀ (l₁ l₂ : ι →₀ R),
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M) →
      l₁ = l₂
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
his : i ∈ s
h : Eq (α := ι →₀ R) (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i))
this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i
rw : (∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i = g i
rw₁ :
  Eq.{u_2 + 1} (α := R) ((∑ j ∈ s, Finsupp.single j (f j) : (a : ι) → R) i : R)
    ((∑ j ∈ s, Finsupp.single j (g j) : (a : ι) → R) i : R)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := R) ((∑ i ∈ s, Finsupp.single i (g i) : (a : ι) → R) i : R)
    ((∑ j ∈ s, Finsupp.single j (g j) : (a : ι) → R) i : R)
⊢ f i = g i

Tactic:
rw [this f, this g, 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)

Tactic:
_root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_

Premises used: Finsupp.support, by_contradiction, Union.union, DFunLike.coe
-- 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
refine_1 :
  ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)),
    Eq.{u_4 + 1} (α := M)
      (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
      (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))
refine_2 :
  ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)), x ∈ f.support ∪ g.support
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)

Tactic:
refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_

Premises used: Finsupp.support, by_contradiction, Union.union, DFunLike.coe
-- 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
refine_1 :
  ∀ x ∈ f.support ∪ g.support, x ∉ g.support → HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) x : R) (v x) = 0
refine_1₁ :
  ∀ x ∈ f.support ∪ g.support, x ∉ f.support → HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x) = 0
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))

Tactic:
rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right]

Premises used: Finset.subset_union_left, Finset.sum_subset, Finset.subset_union_right
-- 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
i : ι
hi : i ∉ g.support
refine_1 : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
refine_1₁ refine_1₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i) = 0

Tactic:
rw [Finsupp.notMem_support_iff.mp hi, zero_smul]

Premises used: Finsupp.notMem_support_iff, zero_smul, Iff.mp
-- 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
i : ι
hi : i ∉ f.support
refine_1 : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
refine_1₁ refine_1₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) = 0

Tactic:
rw [Finsupp.notMem_support_iff.mp hi, zero_smul]

Premises used: Finsupp.notMem_support_iff, zero_smul, Iff.mp
-- 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
refine_2 :
  ∀ (hni : x ∉ f.support ∪ g.support), Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
⊢ x ∈ f.support ∪ g.support

Tactic:
contrapose hni
-- 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : x ∉ f.support ∪ g.support
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) (0 : R) ∧ Eq.{u_2 + 1} (α := R) ((g : (a : ι) → R) x : R) (0 : R)

Tactic:
simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni

Premises used: Finsupp.notMem_support_iff, Finset.notMem_union
-- 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) (0 : R) ∧ Eq.{u_2 + 1} (α := R) ((g : (a : ι) → R) x : R) (0 : R)
refine_2 : Eq.{u_2 + 1} (α := R) (0 : R) ((g : (a : ι) → R) x : R)
refine_2₁ refine_2₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)

Tactic:
rw [hni.1, hni.2]

Premises used: And.right, And.left
-- 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
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
refine_1 :
  ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)),
    Eq.{u_4 + 1} (α := M)
      (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
      (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))
refine_2 refine_2₁ :
  ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)), x ∈ f.support ∪ g.support
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)

Tactic:
classical
        refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_
        · rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;>
            rintro i - hi <;> rw [Finsupp.notMem_support_iff.mp hi, zero_smul]
        · contrapose hni
          simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni
          rw [hni.1, hni.2]

Premises used: Finsupp.notMem_support_iff, Finset.subset_union_left, zero_smul, Finset.notMem_union, Finset.sum_subset, Finset.subset_union_right