awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
h : Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)

Tactic:
simp only [Finsupp.zero_apply]

Premises used: Finsupp.zero_apply
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
h : ∀ (hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)), False
⊢ Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)

Tactic:
by_contra hn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ False

Tactic:
hn (H i _ ?_)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
h :
  Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i})))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i))
⊢ False

Tactic:
refine hn (H i _ ?_)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i})))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i))

Tactic:
(Finsupp.mem_span_image_iff_linearCombination R).2 ⟨Finsupp.single i (l i) - l, ?_, ?_⟩

Premises used: Iff.mpr, HSub.hSub, And.intro, Exists.intro, Finsupp.mem_span_image_iff_linearCombination, DFunLike.coe, Finsupp.single
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
h :
  Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i}))
    (HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l)
h₁ :
  (Finsupp.linearCombination R v : (a : ι →₀ R) → M)
      (HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i)
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i})))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i))

Tactic:
refine (Finsupp.mem_span_image_iff_linearCombination R).2 ⟨Finsupp.single i (l i) - l, ?_, ?_⟩

Premises used: Iff.mpr, HSub.hSub, And.intro, Exists.intro, Finsupp.mem_span_image_iff_linearCombination, DFunLike.coe, Finsupp.single
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
h :
  ∀ x ∉ univ \ {i},
    Eq.{u_2 + 1} (α := R)
      ((HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l : (a : ι) → R) x : R) (0 : R)
⊢ Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (univ \ {i}))
    (HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l)

Tactic:
rw [Finsupp.mem_supported']

Premises used: Finsupp.mem_supported'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
j : ι
hj : j ∉ univ \ {i}
⊢ j = i

Tactic:
have hij : j = i :=
          Classical.not_not.1 fun hij : j ≠ i =>
            hj ((mem_diff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
j : ι
hj : j ∉ univ \ {i}
hij : j = i
⊢ Eq.{u_2 + 1} (α := R)
    ((HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l : (a : ι) → R) j : R) (0 : R)

Tactic:
simp [hij]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
i : ι
hn : ¬Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ (Finsupp.linearCombination R v : (a : ι →₀ R) → M)
      (HSub.hSub (α := ι →₀ R) (Finsupp.single i ((l : (a : ι) → R) i) : ι →₀ R) l) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((l : (a : ι) → R) i : R) (v i)

Tactic:
simp [hl]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : Subsingleton ι
i : ι
hi : ∀ (r : R), r • v i = 0 → r = 0
this : Unique ι := uniqueOfSubsingleton i
⊢ LinearIndependent R v

Tactic:
simpa [linearIndependent_iff, Finsupp.linearCombination_unique, Finsupp.ext_iff,
    Unique.forall_iff] using fun _ ↦ hi _

Premises used: Unique.forall_iff, Finsupp.linearCombination_unique, linearIndependent_iff, Finsupp.ext_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
i : ι
hi : ∀ (r : R), r • v i = 0 → r = 0
⊢ LinearIndepOn R v {i}

Tactic:
LinearIndependent.of_subsingleton' ⟨i, rfl⟩ hi

Premises used: LinearIndependent.of_subsingleton', Subtype.mk, rfl, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Subsingleton ι
i : ι
hi : v i ≠ 0
⊢ ∀ (r : R), r • v i = 0 → r = 0

Tactic:
simp [hi]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
i : ι
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
hi : v i ≠ 0
⊢ LinearIndepOn R v {i}

Tactic:
simp [hi]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
apply :
  (∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0) ↔
    ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
⊢ LinearIndependent K v ↔ ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

Tactic:
apply linearIndependent_iff_eq_zero_of_smul_mem_span.trans

Premises used: linearIndependent_iff_eq_zero_of_smul_mem_span, Iff.trans
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
mp :
  (∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0) →
    ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
mpr :
  (∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))) →
    ∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0
⊢ (∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0) ↔
    ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
h : ∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0
i : ι
h_in_span : Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (v i)
⊢ Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (HSMul.hSMul.{u_3, u, u} (α := K) 1 (v i))

Tactic:
simp [h_in_span]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
h : ∀ (i : ι) (a : K), Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i) → a = 0
i : ι
h_in_span : Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (v i)
⊢ False

Tactic:
apply one_ne_zero (h i 1 (by simp [h_in_span]))

Premises used: one_ne_zero, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
i : ι
a : K
ha : Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i)
mpr : ∀ (ha' : ¬a = 0), False
⊢ a = 0

Tactic:
by_contra ha'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
i : ι
a : K
ha : Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i)
ha' : ¬a = 0
⊢ False

Tactic:
False.elim (h _ ((smul_mem_iff _ ha').1 ha))

Premises used: False.elim, Submodule.smul_mem_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
i : ι
a : K
ha : Membership.mem (γ := Submodule K V) (span K (v '' (univ \ {i}))) (a • v i)
ha' : ¬a = 0
⊢ False

Tactic:
exact False.elim (h _ ((smul_mem_iff _ ha').1 ha))

Premises used: False.elim, Submodule.smul_mem_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s : Set ι
rw :
  (∀ (i : (↑s : Type u')),
      v (↑i : ι) ∉ span K (image (α := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (univ \ {i}))) ↔
    ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
⊢ LinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
rw [LinearIndepOn, linearIndependent_iff_notMem_span, ← Function.comp_def]

Premises used: Function.comp_def, linearIndependent_iff_notMem_span, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s : Set ι
simp_rw :
  (∀ (i : (↑s : Type u')),
      v (↑i : ι) ∉ span K (v '' image (α := (↑s : Type u')) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (univ \ {i}))) ↔
    ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
⊢ (∀ (i : (↑s : Type u')),
      v (↑i : ι) ∉ span K (image (α := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (univ \ {i}))) ↔
    ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
simp_rw [Set.image_comp]

Premises used: Set.image_comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s : Set ι
⊢ (∀ (i : (↑s : Type u')),
      v (↑i : ι) ∉ span K (v '' image (α := (↑s : Type u')) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) (univ \ {i}))) ↔
    ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
simp [Set.image_diff Subtype.val_injective]

Premises used: Subtype.val_injective, Set.image_diff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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 ι
inst_4 : DecidableEq ι
⊢ LinearIndependent R v ↔
    Injective (α := (i : ι) → R) (β := M)
      (⇑((LinearMap.lsum R (fun (x : ι) ↦ R) ℕ : (a : (i : ι) → R →ₗ[R] M) → ((i : ι) → R) →ₗ[R] M) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (v i)) :
        (a : (i : ι) → R) → M)

Tactic:
simp [Fintype.linearIndependent_iffₛ, Injective, funext_iff]

Premises used: Fintype.linearIndependent_iffₛ, funext_iff, Function.Injective
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
simp :
  (FinVec.Forall.{u_2} (α := R) (m := 2) fun (x_1 : Fin 2 → R) ↦
      FinVec.Forall.{u_2} (α := R) (m := 2) fun (x_2 : Fin 2 → R) ↦
        x_1 0 • x + x_1 1 • y = x_2 0 • x + x_2 1 • y → x_1 0 = x_2 0 ∧ x_1 1 = x_2 1) ↔
    ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'
⊢ LinearIndependent R ![x, y] ↔ ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Tactic:
simp [Fintype.linearIndependent_iffₛ, Fin.forall_fin_two, ← FinVec.forall_iff]

Premises used: Fin.forall_fin_two, Fintype.linearIndependent_iffₛ, FinVec.forall_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
⊢ (FinVec.Forall.{u_2} (α := R) (m := 2) fun (x_1 : Fin 2 → R) ↦
      FinVec.Forall.{u_2} (α := R) (m := 2) fun (x_2 : Fin 2 → R) ↦
        x_1 0 • x + x_1 1 • y = x_2 0 • x + x_2 1 • y → x_1 0 = x_2 0 ∧ x_1 1 = x_2 1) ↔
    ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t s' t' : R
h' : s • x + t • y = s' • x + t' • y
⊢ s = s' ∧ t = t'

Tactic:
pair_iffₛ.mp h _ _ _ _ h'

Premises used: LinearIndependent.pair_iffₛ, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
suffices : s = 0 ∧ 0 = t
⊢ s = 0 ∧ t = 0

Tactic:
suffices H : s = 0 ∧ 0 = t from ⟨H.1, H.2.symm⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s • x + HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 y = HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 x + t • y

Tactic:
simpa using h'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s = 0 ∧ 0 = t

Tactic:
exact h.eq_of_pair (by simpa using h')

Premises used: LinearIndependent.eq_of_pair
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
refine_2 :
  ∀ (h : HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t) = 0), s = 0 ∧ t = 0
refine_1 :
  Eq.{u_4 + 1} (α := M)
    ((Finsupp.linearCombination R ![x, y] : (a : Fin (Nat.succ 0).succ →₀ R) → M)
        (HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t)) :
      M)
    ((Finsupp.linearCombination R ![x, y] : (a : Fin (Nat.succ 0).succ →₀ R) → M) 0 : M)
⊢ s = 0 ∧ t = 0

Tactic:
replace h := @h (.single 0 s + .single 1 t) 0 ?_
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t) = 0
⊢ s = 0

Tactic:
simpa using congr($h 0)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t) = 0
⊢ t = 0

Tactic:
simpa using congr($h 1)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t) = 0
⊢ s = 0 ∧ t = 0

Tactic:
exact ⟨by simpa using congr($h 0), by simpa using congr($h 1)⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
⊢ Eq.{u_4 + 1} (α := M)
    ((Finsupp.linearCombination R ![x, y] : (a : Fin (Nat.succ 0).succ →₀ R) → M)
        (HAdd.hAdd (α := Fin (Nat.succ 0).succ →₀ R) (Finsupp.single 0 s) (Finsupp.single 1 t)) :
      M)
    ((Finsupp.linearCombination R ![x, y] : (a : Fin (Nat.succ 0).succ →₀ R) → M) 0 : M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
pos : ∀ (hη : Nonempty η), LinearIndepOn R v (⋃ (i : η), s i)
neg : ∀ (hη : ¬Nonempty η), LinearIndepOn R v (⋃ (i : η), s i)
⊢ LinearIndepOn R v (⋃ (i : η), s i)

Tactic:
by_cases hη : Nonempty η

Premises used: Nonempty
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
⊢ LinearIndepOn R v (⋃ (i : η), s i)

Tactic:
linearIndepOn_of_finite (⋃ i, s i) fun t ht ft => ?_

Premises used: linearIndepOn_of_finite, Set.iUnion
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
pos : ∀ (t : Set ι) (ht : t ⊆ ⋃ (i : η), s i) (ft : t.Finite), LinearIndepOn R v t
⊢ LinearIndepOn R v (⋃ (i : η), s i)

Tactic:
refine linearIndepOn_of_finite (⋃ i, s i) fun t ht ft => ?_

Premises used: linearIndepOn_of_finite, Set.iUnion
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
pos : ∀ (I : Set η) (fi : I.Finite) (hI : t ⊆ ⋃ i ∈ I, s i), LinearIndepOn R v t
⊢ LinearIndepOn R v t

Tactic:
rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩

Premises used: Set.finite_subset_iUnion
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
pos : ∀ (i : η) (hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i), LinearIndepOn R v t
⊢ LinearIndepOn R v t

Tactic:
rcases hs.finset_le fi.toFinset with ⟨i, hi⟩

Premises used: Set.Finite.toFinset, Directed.finset_le
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i
⊢ LinearIndepOn R v t

Tactic:
(h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Premises used: Iff.mpr, Set.iUnion₂_subset, Set.Subset.trans, Set.Finite.mem_toFinset, LinearIndepOn.mono
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i
⊢ LinearIndepOn R v t

Tactic:
exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Premises used: Iff.mpr, Set.iUnion₂_subset, Set.Subset.trans, Set.Finite.mem_toFinset, LinearIndepOn.mono
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
⊢ LinearIndepOn R v (⋃ (i : η), s i)

Tactic:
(linearIndepOn_empty R v).mono (t := iUnion (s ·)) ?_

Premises used: LinearIndepOn.mono, linearIndepOn_empty
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
η : Type u_6
s : η → Set ι
hs : Directed (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
neg : Subset.{u'} (α := Set ι) (⋃ (x : η), s x) ∅
⊢ LinearIndepOn R v (⋃ (i : η), s i)

Tactic:
refine (linearIndepOn_empty R v).mono (t := iUnion (s ·)) ?_

Premises used: LinearIndepOn.mono, linearIndepOn_empty