awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
this : Std.Refl r
⊢ f = g
have inr : ∀ (I : X) (_I_mem : I ∈ c) (hI : (↑f.support : Set ι) ∪ (↑g.support : Set ι) ⊆ (↑I : Set ι)), f = g
Tactic: classical
    obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
⊢ ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
have key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, (↑I : Set ι))
Tactic: have key : ∀ c : Set X, IsChain r c → indep (⋃ (I : X) (_ : I ∈ c), I) := by
    intro c hc
    dsimp [indep]
    rw [linearIndepOn_iffₛ]
    intro f hfsupp g hgsupp hsum
    rcases eq_empty_or_nonempty c with (rfl | hn)
    · rw [show f = 0 by simpa using hfsupp, show g = 0 by simpa using hgsupp]
    haveI : Std.Refl r := ⟨fun _ => Set.Subset.refl _⟩
    classical
    obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, (↑I : Set ι))
⊢ ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
have obtain : ∀ (I : Set ι) (hli : indep I)
  (hmax :
    ∀ (a : X),
      r (Subtype.mk (p := fun (I : Set ι) ↦ indep I) I hli) a →
        r a (Subtype.mk (p := fun (I : Set ι) ↦ indep I) I hli)),
  ∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
Tactic: obtain ⟨⟨I, hli : indep I⟩, hmax : ∀ a, r ⟨I, hli⟩ a → r a ⟨I, hli⟩⟩ :=
    exists_maximal_of_chains_bounded (r := r)
      (fun c hc => ⟨⟨⋃ I ∈ c, (I : Set ι), key c hc⟩, fun I => Set.subset_biUnion_of_mem⟩)
      Set.Subset.trans
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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 : Eq (α := Submodule R M) (span R (range v)) ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
have rw : Codisjoint (α := Submodule R M) (map (Finsupp.linearCombination R v) (Finsupp.supported R R s))
  (map (Finsupp.linearCombination R v) (Finsupp.supported R R t))
Tactic: rw [Finsupp.span_image_eq_map_linearCombination, Finsupp.span_image_eq_map_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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 : Eq (α := Submodule R M) (span R (range v)) ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (α := Submodule R M) (map (Finsupp.linearCombination R v) (Finsupp.supported R R s))
    (map (Finsupp.linearCombination R v) (Finsupp.supported R R t))
have refine : Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)
Tactic: refine Submodule.codisjoint_map ?_ (Finsupp.codisjoint_supported_supported hst)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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 : Eq (α := Submodule R M) (span R (range v)) ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)
have rwa : Eq (α := Submodule R M) (LinearMap.range (Finsupp.linearCombination R v)) ⊤
Tactic: rwa [← LinearMap.range_eq_top, Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have rw : (∀ (t : Finset ι) (g : ι → R),
    (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
  ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
Tactic: rw [linearIndepOn_iff'']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have refine_1 : ∀
  (h :
    ∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
  (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
Tactic: refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
refine_1 :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R),
        (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
    (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
⊢ (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have refine_2 : ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
  (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0), ∀ i ∈ t, g i = 0
Tactic: refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h :
  ∀ (t : Finset ι) (g : ι → R),
    (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0
c d : R
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0
have h₁ : (↑{i, j} : Set ι) ⊆ {i, j} →
  (∀ i_1 ∉ {i, j},
      HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
          (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 =
        0) →
    Eq.{u_4 + 1} (α := M)
        (∑ i_1 ∈ {i, j},
          HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
              (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 •
            f i_1)
        0 →
      ∀ (i_1 : ι),
        Membership.mem (γ := Finset ι) {i, j} i_1 →
          HAdd.hAdd (α := (j : ι) → R) (β := (j : ι) → R) (Pi.single (M := fun (a : ι) ↦ R) i c)
              (Pi.single (M := fun (a : ι) ↦ R) j d) i_1 =
            0
Tactic: specialize h {i, j} (Pi.single i c + Pi.single j d)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0
⊢ ∀ i ∈ t, g i = 0
have ht' : t ⊆ {i, j}
Tactic: have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0
have refine_2 : ∀ (h0 : g i • f i + g j • f j = 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
Tactic: rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
Cleared hypotheses: h0, ht'
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0
ht' : t ⊆ {i, j}
refine_2 : ∀ (h0 : g i • f i + g j • f j = 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
⊢ ∀ i ∈ t, g i = 0
have refine_2₁ : ∀ (x : ι), Membership.mem (γ := Finset ι) {i, j} x → x ∉ t → g x • f x = 0
Tactic: rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0
have hi0 : g i = 0
Tactic: obtain ⟨hi0, hj0⟩ := h _ _ h0
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : (↑t : Set ι) ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
hi0 : g i = 0
⊢ ∀ i ∈ t, g i = 0
have hj0 : g j = 0
Tactic: obtain ⟨hi0, hj0⟩ := h _ _ h0
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have rw : (∀ (t : Finset ι) (g : ι → R),
    (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
  ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
Tactic: classical
  rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
rw rw₁ rw₂ :
  (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have refine_1 : ∀
  (h :
    ∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
  (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
Tactic: classical
  rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
rw rw₁ rw₂ :
  (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
refine_1 :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R),
        (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
    (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have refine_2 : ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
  (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0), ∀ i ∈ t, g i = 0
Tactic: classical
  rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
rw rw₁ rw₂ :
  (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
refine_1 :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R),
        (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
    (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
refine_2 refine_2₁ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0), ∀ i ∈ t, g i = 0
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have refine_2₂ : ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
  (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
Tactic: classical
  rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
rw rw₁ rw₂ :
  (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
refine_1 :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R),
        (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
    (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
refine_2 refine_2₁ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0), ∀ i ∈ t, g i = 0
refine_2₂ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have refine_2₃ : ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
  (hg0 : ∀ i ∉ t, g i = 0) (h0 : g i • f i + g j • f j = 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
Tactic: classical
  rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
i j : ι
f : ι → M
hij : i ≠ j
rw rw₁ rw₂ :
  (∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
refine_1 :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R),
        (↑t : Set ι) ⊆ {i, j} → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0 → ∀ i ∈ t, g i = 0)
    (c d : R) (hcd : c • f i + d • f j = 0), c = 0 ∧ d = 0
refine_2 refine_2₁ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0), ∀ i ∈ t, g i = 0
refine_2₂ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
refine_2₃ :
  ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
    (hg0 : ∀ i ∉ t, g i = 0) (h0 : g i • f i + g j • f j = 0) (ht' : t ⊆ {i, j}), ∀ i ∈ t, g i = 0
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
have refine_2₄ : ∀ (h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0) (t : Finset ι) (g : ι → R) (ht : (↑t : Set ι) ⊆ {i, j})
  (hg0 : ∀ i ∉ t, g i = 0) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • f i) 0) (ht' : t ⊆ {i, j}) (x : ι),
  Membership.mem (γ := Finset ι) {i, j} x → x ∉ t → g x • f x = 0
Tactic: classical
  rw [linearIndepOn_iff'']
  refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
  · specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
  have ht' : t ⊆ {i, j} := by simpa [← Finset.coe_subset]
  rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
  · obtain ⟨hi0, hj0⟩ := h _ _ h0
    exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
  simp +contextual [hg0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
⊢ LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
have rw : (∀ (c d : R), c • ![x, y] 0 + d • ![x, y] 1 = 0 → c = 0 ∧ d = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
Tactic: rw [← linearIndepOn_univ_iff, ← Finset.coe_univ, show @Finset.univ (Fin 2) _ = {0,1} from rfl,
    Finset.coe_insert, Finset.coe_singleton, LinearIndepOn.pair_iff _ (by trivial)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]
have mp : LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
Tactic: tauto
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
mp : LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]
have mpr : LinearIndependent R ![y, x] → LinearIndependent R ![x, y]
Tactic: tauto
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
mp : LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
mpr : LinearIndependent R ![y, x] → LinearIndependent R ![x, y]
mp₁ mp₂ : LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]
have mp₃ : LinearIndependent R ![x, y] →
  ∀ ⦃a₁ a₂ : Fin (Nat.succ 0).succ →₀ R⦄,
    Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R ![y, x] : (a : Fin (Nat.succ 0).succ →₀ R) → M) a₁ : M)
        ((Finsupp.linearCombination R ![y, x] : (a : Fin (Nat.succ 0).succ →₀ R) → M) a₂ : M) →
      a₁ = a₂
Tactic: tauto