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 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 ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have refine_1 : ∀ (i : ι) (hi : i ∈ s), f i = 0
Tactic: refine ⟨fun i hi => ?_, fun 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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 ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
refine_1 : ∀ (i : ι) (hi : i ∈ s), f i = 0
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
have refine_1₁ : ∀ (i : ι) (hi : i ∈ t), f i = 0
Tactic: refine ⟨fun i hi => ?_, fun 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ ∀ i ∈ s, f i = g i
have refine_2 : Disjoint ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i})
Tactic: 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) ?_ ?_
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
refine_2 : Disjoint ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i})
⊢ ∀ i ∈ s, f i = g i
have refine_2₁ : Eq.{u_4 + 1} (α := M)
  (∑ i ∈ s with g i ≤ f i,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i))
  (∑ i ∈ s with f i < g i,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i))
Tactic: 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) ?_ ?_
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
refine_2 : Disjoint ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i})
refine_2₁ :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s with g i ≤ f i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i))
    (∑ i ∈ s with f i < g i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i))
⊢ ∀ i ∈ s, f i = g i
have refine_2₂ : ∀
  (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 ∈ s, f i = g i
Tactic: 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) ?_ ?_
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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ Disjoint ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i})
have refine_2 : ∀ ⦃a : ι⦄, a ∈ s ∧ g a ≤ f a → ¬(a ∈ s ∧ f a < g a)
Tactic: simp_rw [Finset.disjoint_left, Finset.mem_filter]
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s with g i ≤ f i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i))
    (∑ i ∈ s with f i < g i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i))
have refine_2 : ∑ i ∈ s with g i ≤ f i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i) =
  ∑ i ∈ s with f i < g i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i)
Tactic: 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)]
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
| ∑ i ∈ s with g i ≤ f i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i)
have rw : HAdd.hAdd (α := M)
  (∑ x ∈ s with g x ≤ f x,
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
      g x • v x))
  (∑ i ∈ s with f i < g i, f i • v i)
Tactic: rw [← add_assoc, ← Finset.sum_add_distrib]
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ ∑ i ∈ s with g i ≤ f i,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
      HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i) =
    ∑ i ∈ s with f i < g i,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
      HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i)
have refine_2 : HAdd.hAdd (α := M)
    (∑ x ∈ s with g x ≤ f x,
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
        g x • v x))
    (∑ i ∈ s with f i < g i, f i • v i) =
  ∑ i ∈ s with f i < g i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i)
Tactic: conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
| ∑ i ∈ s with f i < g i,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i)
have rw : HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
  (∑ x ∈ s with f x < g x,
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
      f x • v x))
Tactic: rw [add_left_comm, ← Finset.sum_add_distrib]
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    ∑ i ∈ s with f i < g i,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
      HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i)
have refine_2 : HAdd.hAdd (α := M)
    (∑ x ∈ s with g x ≤ f x,
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
        g x • v x))
    (∑ i ∈ s with f i < g i, f i • v i) =
  HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
    (∑ x ∈ s with f x < g x,
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
        f x • v x))
Tactic: conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          f x • v x))
have h₁ : HAdd.hAdd (α := M)
    (∑ x ∈ s with g x ≤ f x,
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
        g x • v x))
    (∑ i ∈ s with f i < g i, f i • v i) =
  ∑ i ∈ s, f i • v i
Tactic: convert! 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h₁ :
  HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    ∑ i ∈ s, f i • v i
⊢ HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          f x • v x))
have h₂ : HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
    (∑ x ∈ s with f x < g x,
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
        f x • v x)) =
  ∑ i ∈ s, g i • v i
Tactic: convert! 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    ∑ i ∈ s, f i • v i
have h₁ : HAdd.hAdd (α := M) (∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x))
    (∑ i ∈ s with f i < g i, f i • v i) =
  HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, f i • v i) (∑ i ∈ s with f i < g i, f i • v i)
Tactic: simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          f x • v x)) =
    ∑ i ∈ s, g i • v i
have h₁ : HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
    (∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x)) =
  HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, g i • v i)
Tactic: simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
-- 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
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ HAdd.hAdd (α := M) (∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, f i • v i) (∑ i ∈ s with f i < g i, f i • v i)
have h₁ : ∀ (i : ι) (hi : i ∈ {i ∈ s | g i ≤ f i}), (if g i ≤ f i then f i - g i else g i - f i) • v i + g i • v i = f i • v i
Tactic: congr! 2 with 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x)) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, g i • v i)
have h₁ : ∀ (i : ι) (hi : i ∈ {x ∈ s | f x < g x}), (if g i ≤ f i then f i - g i else g i - f i) • v i + f i • v i = g i • v i
Tactic: congr! 2 with i hi
-- 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ {i ∈ s | g i ≤ f i}
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + g i • v i = f i • v i
have hi₁ : i ∈ s ∧ g i ≤ f i
Tactic: simp only [Finset.mem_filter] at hi
Cleared hypotheses: hi
-- 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ {x ∈ s | f x < g x}
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + f i • v i = g i • v i
have hi₁ : i ∈ s ∧ f i < g i
Tactic: simp only [Finset.mem_filter] at hi
Cleared hypotheses: hi
-- 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
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 ∈ s, f i = g i
have 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
Tactic: simp only [Finset.mem_filter] at h
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
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
⊢ f i = g i
have pos : ∀ (hi' : g i ≤ f i), f i = g i
Tactic: by_cases hi' : g i ≤ f i
-- 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
pos : ∀ (hi' : g i ≤ f i), f i = g i
⊢ f i = g i
have neg : ∀ (hi' : ¬g i ≤ f i), f i = g i
Tactic: by_cases hi' : g i ≤ f i