awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : g i ≤ f i
⊢ f i = g i
have pos : f i ≤ g i
Tactic: apply hi'.antisymm'
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ f i = g i
have neg : g i ≤ f i
Tactic: apply (not_le.1 hi').le.antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
letI letI₁ letI₂ :
  LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
⊢ LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have letI₃ : let this : Sub R := CanonicallyOrderedAdd.toSub;
∀ (this : OrderedSub R),
  LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
Tactic: classical
  letI : Sub R := CanonicallyOrderedAdd.toSub
  haveI : OrderedSub R := CanonicallyOrderedAdd.toOrderedSub
  rw [linearIndependent_iff'ₛ]
  refine ⟨fun h s t f hst heq => ?_, fun h s f g heq => ?_⟩
  · specialize h (s ∪ t) (fun i => if i ∈ s then f i else 0) (fun i => if i ∈ t then f i else 0) ?_
    · simpa
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩
    · simpa [hi, hst.notMem_of_mem_left_finset hi] using h i (Finset.mem_union_left _ hi)
    · simpa [hi, hst.notMem_of_mem_right_finset hi] using (h i (Finset.mem_union_right _ hi)).symm
  · specialize h { i ∈ s | g i ≤ f i } { i ∈ s | f i < g i }
      (fun i => if g i ≤ f i then f i - g i else g i - f i) ?_ ?_
    · simp_rw [Finset.disjoint_left, Finset.mem_filter]
      exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'
    · rw [← add_right_cancel_iff
        (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]
      conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
      conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
      convert! heq
        <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
        <;> congr! 2 with i hi
        <;> simp only [Finset.mem_filter] at hi
      · simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]
      · simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]
    simp only [Finset.mem_filter] at h
    intro i hi
    by_cases hi' : g i ≤ f i
    · apply hi'.antisymm'
      simpa [hi', tsub_eq_zero_iff_le] using h.1 i ⟨hi, hi'⟩
    · apply (not_le.1 hi').le.antisymm
      simpa [hi', tsub_eq_zero_iff_le] using h.2 i ⟨hi, not_le.1 hi'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
letI letI₁ letI₂ :
  LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
letI₃ :
  let this : Sub R := CanonicallyOrderedAdd.toSub;
  ∀ (this : OrderedSub R),
    LinearIndependent R v ↔
      ∀ (s t : Finset ι) (f : ι → R),
        Disjoint s t →
          Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
⊢ LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have letI₄ : let this : Sub R := CanonicallyOrderedAdd.toSub;
∀ (this : OrderedSub R),
  (∀ (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) ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
Tactic: classical
  letI : Sub R := CanonicallyOrderedAdd.toSub
  haveI : OrderedSub R := CanonicallyOrderedAdd.toOrderedSub
  rw [linearIndependent_iff'ₛ]
  refine ⟨fun h s t f hst heq => ?_, fun h s f g heq => ?_⟩
  · specialize h (s ∪ t) (fun i => if i ∈ s then f i else 0) (fun i => if i ∈ t then f i else 0) ?_
    · simpa
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩
    · simpa [hi, hst.notMem_of_mem_left_finset hi] using h i (Finset.mem_union_left _ hi)
    · simpa [hi, hst.notMem_of_mem_right_finset hi] using (h i (Finset.mem_union_right _ hi)).symm
  · specialize h { i ∈ s | g i ≤ f i } { i ∈ s | f i < g i }
      (fun i => if g i ≤ f i then f i - g i else g i - f i) ?_ ?_
    · simp_rw [Finset.disjoint_left, Finset.mem_filter]
      exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'
    · rw [← add_right_cancel_iff
        (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]
      conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
      conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
      convert! heq
        <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
        <;> congr! 2 with i hi
        <;> simp only [Finset.mem_filter] at hi
      · simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]
      · simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]
    simp only [Finset.mem_filter] at h
    intro i hi
    by_cases hi' : g i ≤ f i
    · apply hi'.antisymm'
      simpa [hi', tsub_eq_zero_iff_le] using h.1 i ⟨hi, hi'⟩
    · apply (not_le.1 hi').le.antisymm
      simpa [hi', tsub_eq_zero_iff_le] using h.2 i ⟨hi, not_le.1 hi'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
⊢ ¬LinearIndependent R v ↔
    ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
      Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, 0 < f i
have simp : (¬∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
  ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
Tactic: simp only [linearIndependent_iffₒₛ, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
⊢ (¬∀ (s t : Finset ι) (f : ι → R),
        Disjoint s t →
          Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
    ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
      Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
have push : (∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)) ↔
  ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
Tactic: push +distrib Not
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
⊢ (∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
      Disjoint s t ∧
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)) ↔
    ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
      Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
have refine : (∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)) →
  ∀ (s t : Finset ι) (f : ι → R) (hst : Disjoint s t)
    (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i)) (h : (∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0),
    ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
      Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
Tactic: refine ⟨fun ⟨s, t, f, hst, heq, h⟩ => ?_,
    fun ⟨s, t, f, hst, heq, hi⟩ => ⟨s, t, f, hst, heq, .inl hi⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
h_1 :
  ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i)
h : (∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0
⊢ ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
have inl : ∀ (i : ι) (hi : i ∈ s) (hfi : f i ≠ 0),
  ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
Tactic: rcases h with ⟨i, hi, hfi⟩ | ⟨i, hi, hgi⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
h_1 :
  ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i)
h : (∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0
inl :
  ∀ (i : ι) (hi : i ∈ s) (hfi : f i ≠ 0),
    ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
      Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
⊢ ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
have inr : ∀ (i : ι) (hi : i ∈ t) (hgi : f i ≠ 0),
  ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0
Tactic: rcases h with ⟨i, hi, hfi⟩ | ⟨i, hi, hgi⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
⊢ LinearIndependent R v ↔
    ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
have rw : (∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t →
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
  ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
Tactic: rw [linearIndependent_iffₒₛ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
⊢ (∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
    ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
have refine_1 : ∀
  (h :
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0)
  (t : Finset ι) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)) (i : ι), f i = 0
Tactic: refine ⟨fun h t f heq i => ?_, fun h t₁ t₂ f ht₁t₂ heq => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
refine_1 :
  ∀
    (h :
      ∀ (s t : Finset ι) (f : ι → R),
        Disjoint s t →
          Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0)
    (t : Finset ι) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)) (i : ι), f i = 0
⊢ (∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
    ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
have refine_2 : ∀
  (h :
    ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0)
  (t₁ t₂ : Finset ι) (f : ι → R) (ht₁t₂ : Disjoint t₁ t₂)
  (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)), (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
Tactic: refine ⟨fun h t f heq i => ?_, fun h t₁ t₂ f ht₁t₂ heq => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
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 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t →
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
⊢ f i = 0
have h₁ : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
Tactic: specialize h t tᶜ f disjoint_compl_right heq
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
⊢ f i = 0
have pos : ∀ (hi : i ∈ t), f i = 0
Tactic: by_cases hi : i ∈ t
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
pos : ∀ (hi : i ∈ t), f i = 0
⊢ f i = 0
have neg : ∀ (hi : i ∉ t), f i = 0
Tactic: by_cases hi : i ∈ t
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
have refine_2 : Eq.{u_4 + 1} (α := M)
  (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
  (∑ i ∈ t₁ᶜ, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
Tactic: specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
refine_2 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ i ∈ t₁ᶜ, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
have refine_2₁ : ∀ (h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0), (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
Tactic: specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ i ∈ t₁ᶜ, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
have refine_2 : Eq.{u_4 + 1} (α := M)
  (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
  (∑ x ∈ t₂, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) x) (v x))
Tactic: rw [← Finset.sum_subset ht₁t₂.le_compl_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
refine_2 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ x ∈ t₂, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) x) (v x))
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ i ∈ t₁ᶜ, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
have refine_2₁ : ∀ x ∈ t₁ᶜ,
  x ∉ t₂ → HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) x) (v x) = 0
Tactic: rw [← Finset.sum_subset ht₁t₂.le_compl_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ x ∈ t₂, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) x) (v x))
have h₁ : ∀ (i : ι) (hi : i ∈ t₁),
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i) = f i • v i
Tactic: convert! heq using 2 with i hi i hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
h₁ :
  ∀ (i : ι) (hi : i ∈ t₁),
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i) = f i • v i
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ x ∈ t₂, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) x) (v x))
have h₂ : ∀ (i : ι) (hi : i ∈ t₂),
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i) = f i • v i
Tactic: convert! heq using 2 with i hi i hi