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
inst_7 : DecidableEq ι
inst_8 : Fintype ι
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 : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
have refine_2 : ∀ (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
inst_7 : DecidableEq ι
inst_8 : Fintype ι
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 : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
refine_2 : ∀ (i : ι) (hi : i ∈ t₁), f i = 0
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
have refine_2₁ : ∀ (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
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 ∈ t, 0 < f i
have simp : (∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0) ↔
  ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
Tactic: simp only [linearIndependent_iffₒₛ, not_forall, 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
inst_7 : DecidableEq ι
inst_8 : Fintype ι
⊢ (∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
      ¬x_1 x = 0) ↔
    ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
have refine : (∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0) →
  ∀ (t : Finset ι) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)) (i : ι)
    (hfi : ¬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 ∈ t, f i ≠ 0
Tactic: refine ⟨fun ⟨t, f, heq, i, hfi⟩ => ?_, fun ⟨t, f, heq, i, hi, hfi⟩ =>
    ⟨t, f, heq, i, hfi⟩⟩
-- 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 :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬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 ∈ t, f i ≠ 0
have pos : ∀ (hi' : i ∈ t),
  ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ 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 :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬f i = 0
pos :
  ∀ (hi' : i ∈ t),
    ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ 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 ∈ t, f i ≠ 0
have neg : ∀ (hi' : i ∉ t),
  ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ 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 :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
have neg : Eq.{u_4 + 1} (α := M) (∑ i ∈ tᶜ, f i • v i) (∑ i ∈ tᶜᶜ, f i • v i)
Tactic: refine ⟨tᶜ, f, ?_, i, Finset.mem_compl.2 hi', hfi⟩
-- 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 ι
s : Finset ι
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
have rw : (∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0) ↔
  ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
Tactic: rw [LinearIndepOn, Fintype.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 ι
s : Finset ι
⊢ (∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0) ↔
    ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
have refine_1 : ∀
  (h :
    ∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0)
  (t : Finset ι) (ht : t ⊆ s) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i))
  (i : ι) (hi : i ∈ s),
  Eq.{u_4 + 1} (α := M)
    (∑ i : (↑(↑s : Set ι) : Type u') with (↑i : ι) ∈ t,
      (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
    (∑ i ∈ {i : (↑(↑s : Set ι) : Type u') | (↑i : ι) ∈ t}ᶜ,
      (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
Tactic: refine ⟨fun h t ht f heq i hi => h { i | i.1 ∈ t } (f ∘ Subtype.val) ?_ ⟨i, hi⟩,
    fun h t f heq 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
inst_7 : DecidableEq ι
s : Finset ι
refine_1 :
  ∀
    (h :
      ∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
          ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0)
    (t : Finset ι) (ht : t ⊆ s) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i))
    (i : ι) (hi : i ∈ s),
    Eq.{u_4 + 1} (α := M)
      (∑ i : (↑(↑s : Set ι) : Type u') with (↑i : ι) ∈ t,
        (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
      (∑ i ∈ {i : (↑(↑s : Set ι) : Type u') | (↑i : ι) ∈ t}ᶜ,
        (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
⊢ (∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0) ↔
    ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
have refine_2 : ∀ (h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0)
  (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R)
  (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)))
  (i : (↑(↑s : Set ι) : Type u')), f i = 0
Tactic: refine ⟨fun h t ht f heq i hi => h { i | i.1 ∈ t } (f ∘ Subtype.val) ?_ ⟨i, hi⟩,
    fun h t f heq 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
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i : (↑(↑s : Set ι) : Type u') with (↑i : ι) ∈ t,
      (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
    (∑ i ∈ {i : (↑(↑s : Set ι) : Type u') | (↑i : ι) ∈ t}ᶜ,
      (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
have refine_1 : Eq.{u_4 + 1} (α := M) (∑ a : ↥s, if (↑a : ι) ∈ t then f (↑a : ι) • v (↑a : ι) else 0)
  (∑ a : ↥s, if (↑a : ι) ∉ t then f (↑a : ι) • v (↑a : ι) else 0)
Tactic: simp only [Finset.compl_filter, Finset.sum_filter, Function.comp_apply, Finset.coe_sort_coe]
-- 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 ι
s : Finset ι
h :
  ∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
⊢ Eq.{u_4 + 1} (α := M) (∑ a : ↥s, if (↑a : ι) ∈ t then f (↑a : ι) • v (↑a : ι) else 0)
    (∑ a : ↥s, if (↑a : ι) ∉ t then f (↑a : ι) • v (↑a : ι) else 0)
have refine_1 : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, if i ∈ t then f i • v i else 0) (∑ i ∈ s, if i ∉ t then f i • v i else 0)
Tactic: rw [Finset.sum_coe_sort s fun i => if i ∈ t then f i • v i else 0,
      Finset.sum_coe_sort s fun i => if i ∉ t then f i • v 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 ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
⊢ f i = 0
have refine_2 : Eq.{u_4 + 1} (α := M)
  (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R)
      ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i) (v i))
  (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R)
      ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i) (v i))
Tactic: specialize h (t.map (Embedding.subtype _)) (Finset.map_subtype_subset _)
      (fun i => if h : i ∈ s then f ⟨i, h⟩ else 0) ?_ i i.2
-- 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 ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
refine_2 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
⊢ f i = 0
have refine_2₁ : ∀
  (h :
    Eq.{u_2 + 1} (α := R)
      (if h : (↑i : ι) ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) (↑i : ι) h) else 0) 0),
  f i = 0
Tactic: specialize h (t.map (Embedding.subtype _)) (Finset.map_subtype_subset _)
      (fun i => if h : i ∈ s then f ⟨i, h⟩ else 0) ?_ i i.2
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 ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
| Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
have enter : s
Tactic: enter [2, 1, 1]
-- 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 ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
| s
have rw : Finset.map (Embedding.subtype (Membership.mem s)) Finset.univ
Tactic: rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]
-- 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 ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
| Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
have enter : Finset.map (α := { x : ι // x ∈ (↑s : Set ι) }) (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) Finset.univ
Tactic: enter [2, 1, 1]
        rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]
        change Finset.map (Embedding.subtype (· ∈ (s : Set ι))) _
-- 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 ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
have refine_2 : Eq.{u_4 + 1} (α := M)
  (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R)
      ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i) (v i))
  (∑
    i ∈
      Finset.map (α := { x : ι // x ∈ (↑s : Set ι) }) (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) Finset.univ \
        Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R)
      ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i) (v i))
Tactic: conv =>
        enter [2, 1, 1]
        rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]
        change Finset.map (Embedding.subtype (· ∈ (s : Set ι))) _
-- 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 ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑
      i ∈
        Finset.map (α := { x : ι // x ∈ (↑s : Set ι) }) (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) Finset.univ \
          Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
have refine_2 : Eq.{u_4 + 1} (α := M)
  (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
    HSMul.hSMul.{u_2, u_4, u_4} (α := R)
      ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i) (v i))
  (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) (Finset.univ \ t),
    HSMul.hSMul.{u_2, u_4, u_4} (α := R)
      ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i) (v i))
Tactic: rw [← Finset.map_sdiff]
-- 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 ι
s : Finset ι
⊢ ¬LinearIndepOn R v (↑s : Set ι) ↔
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, 0 < f i
have simp : (∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0) ↔
  ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
Tactic: simp only [linearIndepOn_finset_iffₒₛ, not_forall, pos_iff_ne_zero]