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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
i : ι
hi : i ∉ f.support
refine_1 : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) = 0
have refine_1₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [Finsupp.notMem_support_iff.mp hi, zero_smul]
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
⊢ x ∈ f.support ∪ g.support
have refine_2 : ∀ (hni : x ∉ f.support ∪ g.support), Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
Tactic: contrapose hni
Cleared hypotheses: hni
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : x ∉ f.support ∪ g.support
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
have hni₁ : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) (0 : R) ∧ Eq.{u_2 + 1} (α := R) ((g : (a : ι) → R) x : R) (0 : R)
Tactic: simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni
Cleared hypotheses: hni
-- 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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) (0 : R) ∧ Eq.{u_2 + 1} (α := R) ((g : (a : ι) → R) x : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
have refine_2 : Eq.{u_2 + 1} (α := R) (0 : R) ((g : (a : ι) → R) x : R)
Tactic: rw [hni.1, hni.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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
hni : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) (0 : R) ∧ Eq.{u_2 + 1} (α := R) ((g : (a : ι) → R) x : R) (0 : R)
refine_2 : Eq.{u_2 + 1} (α := R) (0 : R) ((g : (a : ι) → R) x : R)
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
have refine_2₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [hni.1, hni.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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
have refine_1 : ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)),
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
    (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))
Tactic: classical
        refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_
        · rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;>
            rintro i - hi <;> rw [Finsupp.notMem_support_iff.mp hi, zero_smul]
        · contrapose hni
          simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni
          rw [hni.1, hni.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
hv :
  ∀ (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
f g : ι →₀ R
hl :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
x : ι
refine_1 :
  ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)),
    Eq.{u_4 + 1} (α := M)
      (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
      (∑ i ∈ f.support ∪ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i))
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)
have refine_2 : ∀ (hni : ¬Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) ((g : (a : ι) → R) x : R)), x ∈ f.support ∪ g.support
Tactic: classical
        refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_
        · rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;>
            rintro i - hi <;> rw [Finsupp.notMem_support_iff.mp hi, zero_smul]
        · contrapose hni
          simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni
          rw [hni.1, hni.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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
simp_rw simp_rw₁ :
  Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (if x ∈ s then f x else 0) • v x) (∑ x ∈ s, (if x ∈ s then g x else 0) • v x)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then f j else 0) i) (v i))
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then g j else 0) i) (v i))
have simp_rw₂ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then f x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x))
  (∑ x ∈ s, if x ∈ s then g x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x))
Tactic: simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]
-- 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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
simp_rw simp_rw₁ :
  Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (if x ∈ s then f x else 0) • v x) (∑ x ∈ s, (if x ∈ s then g x else 0) • v x)
simp_rw₂ :
  Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then f x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x))
    (∑ x ∈ s, if x ∈ s then g x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x))
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then f j else 0) i) (v i))
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then g j else 0) i) (v i))
have simp_rw₃ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then f x • v x else 0) (∑ x ∈ s, if x ∈ s then g x • v x else 0)
Tactic: simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]
-- 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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
⊢ f i = g i
have h : f i = if i ∈ s then f i else 0
Tactic: convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) 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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
h : f i = if i ∈ s then f i else 0
⊢ f i = g i
have h₁ : g i = if i ∈ s then g i else 0
Tactic: convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) 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
⊢ ¬LinearIndependent R v ↔
    ∃ (s : Finset ι) (f : ι → R) (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
have rw : (¬∀ (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 : Finset ι) (f : ι → R) (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
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 : Fintype ι
⊢ LinearIndependent R v ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
have simp_rw : Injective (α := ι → R) (β := M) (⇑(Fintype.linearCombination R v) : (a : ι → R) → M) ↔
  ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
Tactic: simp_rw [linearIndependent_iff_injective_fintypeLinearCombination,
    Injective, Fintype.linearCombination_apply, funext_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 : Fintype ι
simp_rw :
  Injective (α := ι → R) (β := M) (⇑(Fintype.linearCombination R v) : (a : ι → R) → M) ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
⊢ LinearIndependent R v ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
have simp_rw₁ : (∀ ⦃a₁ a₂ : ι → R⦄,
    Eq.{u_4 + 1} (α := M) ((Fintype.linearCombination R v : (a : ι → R) → M) a₁ : M)
        ((Fintype.linearCombination R v : (a : ι → R) → M) a₂ : M) →
      a₁ = a₂) ↔
  ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
Tactic: simp_rw [linearIndependent_iff_injective_fintypeLinearCombination,
    Injective, Fintype.linearCombination_apply, funext_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 : Fintype ι
simp_rw :
  Injective (α := ι → R) (β := M) (⇑(Fintype.linearCombination R v) : (a : ι → R) → M) ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
simp_rw₁ :
  (∀ ⦃a₁ a₂ : ι → R⦄,
      Eq.{u_4 + 1} (α := M) ((Fintype.linearCombination R v : (a : ι → R) → M) a₁ : M)
          ((Fintype.linearCombination R v : (a : ι → R) → M) a₂ : M) →
        a₁ = a₂) ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
⊢ LinearIndependent R v ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
have simp_rw₂ : (∀ ⦃a₁ a₂ : ι → R⦄, Eq.{u_4 + 1} (α := M) (∑ i : ι, a₁ i • v i) (∑ i : ι, a₂ i • v i) → a₁ = a₂) ↔
  ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
Tactic: simp_rw [linearIndependent_iff_injective_fintypeLinearCombination,
    Injective, Fintype.linearCombination_apply, funext_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
s : Finset ι
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ (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
have simp_rw : (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
  ∀ (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
Tactic: simp_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
s : Finset ι
⊢ (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
    ∀ (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
have mp : (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) →
  ∀ (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
Tactic: constructor
-- 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
s : Finset ι
mp :
  (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) →
    ∀ (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
⊢ (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
    ∀ (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
have mpr : (∀ (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) →
  ∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i
Tactic: constructor
-- 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
s : Finset ι
hv :
  ∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i
f g : ι → R
hfg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
⊢ f i = g i
have hfg₁ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s.attach, f (↑x : ι) • v (↑x : ι)) (∑ x ∈ s.attach, g (↑x : ι) • v (↑x : ι))
Tactic: simp_rw [← s.sum_attach] at hfg
Cleared hypotheses: hfg
-- 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
s : Finset ι
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ (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
have simp_rw : (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(↑s : Set ι) : Type u')) ↦ v (↑x : ι)) ↔
  ∀ (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
Tactic: classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iffₛ]
  constructor
  · rintro hv f g hfg i hi
    simp_rw [← s.sum_attach] at hfg
    exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩
  · rintro hv f g hfg i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (fun j ↦ if hj : j ∈ s then g ⟨j, hj⟩ else 0) (by simpa +contextual [← s.sum_attach]) 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
s : Finset ι
simp_rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(↑s : Set ι) : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (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
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ (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
have simp_rw₁ : (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
  ∀ (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
Tactic: classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iffₛ]
  constructor
  · rintro hv f g hfg i hi
    simp_rw [← s.sum_attach] at hfg
    exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩
  · rintro hv f g hfg i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (fun j ↦ if hj : j ∈ s then g ⟨j, hj⟩ else 0) (by simpa +contextual [← s.sum_attach]) 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
s : Finset ι
simp_rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(↑s : Set ι) : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (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
simp_rw₁ :
  (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
    ∀ (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
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ (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
have mp : (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) →
  ∀ (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
Tactic: classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iffₛ]
  constructor
  · rintro hv f g hfg i hi
    simp_rw [← s.sum_attach] at hfg
    exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩
  · rintro hv f g hfg i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (fun j ↦ if hj : j ∈ s then g ⟨j, hj⟩ else 0) (by simpa +contextual [← s.sum_attach]) 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
s : Finset ι
simp_rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(↑s : Set ι) : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (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
simp_rw₁ :
  (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
    ∀ (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
mp :
  (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) →
    ∀ (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
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ (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
have mpr : (∀ (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) →
  ∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i
Tactic: classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iffₛ]
  constructor
  · rintro hv f g hfg i hi
    simp_rw [← s.sum_attach] at hfg
    exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩
  · rintro hv f g hfg i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (fun j ↦ if hj : j ∈ s then g ⟨j, hj⟩ else 0) (by simpa +contextual [← s.sum_attach]) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → LinearIndepOn R v (↑t : Set ι)
⊢ LinearIndepOn R v s
have rw : ∀ (s_1 : Finset (↑s : Type u')),
  LinearIndependent.{u', u_2, u_4} (ι := ↥s_1) R (M := M)
    ((fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ∘ Subtype.val (p := fun (x : (↑s : Type u')) ↦ x ∈ s_1))
Tactic: rw [LinearIndepOn, linearIndependent_iff_finset_linearIndependent]