awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), f i)
have rw : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (t : Finset ι), ⋃ i ∈ t, f i)
Tactic: classical
  rw [iUnion_eq_iUnion_finset f]
  apply linearIndepOn_iUnion_of_directed
  · apply directed_of_isDirected_le
    exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h
  intro t
  induction t using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    rw [Finset.set_biUnion_insert]
    refine (hl _).id_union ih ?_
    rw [span_iUnion₂]
    exact hd i s s.finite_toSet his
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
rw rw₁ rw₂ : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (t : Finset ι), ⋃ i ∈ t, f i)
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), f i)
have hs : Directed (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, f i_1
Tactic: classical
  rw [iUnion_eq_iUnion_finset f]
  apply linearIndepOn_iUnion_of_directed
  · apply directed_of_isDirected_le
    exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h
  intro t
  induction t using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    rw [Finset.set_biUnion_insert]
    refine (hl _).id_union ih ?_
    rw [span_iUnion₂]
    exact hd i s s.finite_toSet his
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ t, span R (f i))
rw rw₁ rw₂ : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (t : Finset ι), ⋃ i ∈ t, f i)
hs : Directed (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) fun (i : Finset ι) ↦ ⋃ i_1 ∈ i, f i_1
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), f i)
have h : ∀ (i : Finset ι), LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i_1 ∈ i, f i_1)
Tactic: classical
  rw [iUnion_eq_iUnion_finset f]
  apply linearIndepOn_iUnion_of_directed
  · apply directed_of_isDirected_le
    exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h
  intro t
  induction t using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    rw [Finset.set_biUnion_insert]
    refine (hl _).id_union ih ?_
    rw [span_iUnion₂]
    exact hd i s s.finite_toSet his
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
⊢ LinearIndependent R (M := M) fun (ji : (j : η) × ιs j) ↦
    f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j))
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
⊢ LinearIndependent R (M := M) fun (ji : (j : η) × ιs j) ↦
    f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j))
have hf : Injective (β := M) fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j))
Tactic: apply LinearIndependent.of_linearIndepOn_id_range
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
hf :
  Injective (β := M) fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j))
⊢ LinearIndependent R (M := M) fun (ji : (j : η) × ιs j) ↦
    f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j))
have a : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id
  (range fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
Tactic: apply LinearIndependent.of_linearIndepOn_id_range
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy :
  Eq.{u_4 + 1} (α := M)
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂))
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂
have pos : ∀ (h_cases : x₁ = y₁), Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂
Tactic: by_cases h_cases : x₁ = y₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy :
  Eq.{u_4 + 1} (α := M)
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂))
pos : ∀ (h_cases : x₁ = y₁), Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂
have neg : ∀ (h_cases : ¬x₁ = y₁), Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂
Tactic: by_cases h_cases : x₁ = y₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy :
  Eq.{u_4 + 1} (α := M)
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂))
h_cases : x₁ = y₁
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂
have pos : ∀ (y₂ : ιs x₁)
  (hxy :
    Eq.{u_4 + 1} (α := M)
      ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
        (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
      ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
        (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂))),
  Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂
Tactic: subst h_cases
Cleared hypotheses: y₁, y₂, hxy, h_cases
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy :
  Eq.{u_4 + 1} (α := M)
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂))
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂
have pos : Eq.recOn (motive := fun (x : η) (x_1 : (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂).fst (β := fun (a : η) ↦ ιs a) = x) ↦
    ιs x) sorry ((Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂).snd (β := fun (a : η) ↦ ιs a)) =
  (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂).snd (β := fun (a : η) ↦ ιs a)
Tactic: refine Sigma.eq rfl ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy :
  Eq.{u_4 + 1} (α := M)
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂))
⊢ Eq.recOn (motive := fun (x : η) (x_1 : (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂).fst (β := fun (a : η) ↦ ιs a) = x) ↦
      ιs x) ⋯ ((Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂).snd (β := fun (a : η) ↦ ιs a)) =
    (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂).snd (β := fun (a : η) ↦ ιs a)
have pos : Eq.recOn (motive := fun (x : η) (x_1 : (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂).fst (β := fun (a : η) ↦ ιs a) = x) ↦
    ιs x) sorry ((Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂).snd (β := fun (j : η) ↦ ιs j)) =
  (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂).snd (β := fun (a : η) ↦ ιs a)
Tactic: rw [LinearIndependent.injective (hindep _) hxy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy :
  Eq.{u_4 + 1} (α := M)
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂))
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ = 0
have x₃ : Membership.mem (γ := Submodule R M) (⨆ (i : η), ⨆ (_ : Membership.mem (γ := Set η) {y₁} i), span R (range (f i)))
  (f x₁ x₂)
Tactic: apply
          disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
            (f x₁ x₂) (subset_span (mem_range_self _))
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy :
  Eq.{u_4 + 1} (α := M)
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂))
h_cases : ¬x₁ = y₁
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : η), ⨆ (_ : Membership.mem (γ := Set η) {y₁} i), span R (range (f i)))
    (f x₁ x₂)
have rw : Membership.mem (γ := Submodule R M) (span R (range (f y₁))) (f x₁ x₂)
Tactic: rw [iSup_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ Membership.mem (γ := Submodule R M) (span R (range (f y₁))) (f x₁ x₂)
have rw : Membership.mem (γ := Submodule R M) (span R (range (f y₁))) (f y₁ y₂)
Tactic: rw [hxy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy :
  Eq.{u_4 + 1} (α := M)
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂))
    ((fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
      (Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂))
h_cases : ¬x₁ = y₁
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂
have h0 : f x₁ x₂ = 0
Tactic: have h0 : f x₁ x₂ = 0 := by
        apply
          disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
            (f x₁ x₂) (subset_span (mem_range_self _))
        rw [iSup_singleton]
        simp only at hxy
        rw [hxy]
        exact subset_span (mem_range_self y₂)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd :
  ∀ (i : η) (t : Set η),
    t.Finite → i ∉ t → Disjoint (α := Submodule R M) (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
h : Nontrivial R
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id
    (range fun (ji : (j : η) × ιs j) ↦ f (ji.fst (β := fun (j : η) ↦ ιs j)) (ji.snd (β := fun (j : η) ↦ ιs j)))
have a : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id
  (⋃ (a : η),
    range fun (b : ιs a) ↦
      f ((Sigma.mk (β := fun (j : η) ↦ ιs j) a b).fst (β := fun (j : η) ↦ ιs j))
        ((Sigma.mk (β := fun (j : η) ↦ ιs j) a b).snd (β := fun (j : η) ↦ ιs j)))
Tactic: rw [range_sigma_eq_iUnion_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
have rcases : ∀ (I : Set ι) (hIlinind : LinearIndepOn R v I) (hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t),
  ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
Tactic: rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
⊢ ∃ (s : Set ι),
    LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' s)) (a • v i)
have right : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
Tactic: use I, hIlinind
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
i : ι
hi : i ∉ I
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
have hImaximal₁ : LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}
Tactic: specialize hImaximal (I ∪ {i}) (by simp)
Cleared hypotheses: hImaximal
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
hImaximal : LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}
hImaximal₁ :
  let J := I ∪ {i};
  LinearIndepOn R v J → I = J
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
have hJ : let J := I ∪ {i};
J = I ∪ {i}
Tactic: set J := I ∪ {i} with hJ
Cleared hypotheses: hImaximal
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
have memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
Tactic: have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
have hiJ : i ∈ J
Tactic: have hiJ : i ∈ J := by simp [J]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ¬LinearIndepOn R v J
have refine : ¬I = J
Tactic: refine mt hImaximal ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
⊢ False
have hi₁ : i ∉ J
Tactic: rw [h2] at hi
Cleared hypotheses: hi, hImaximal, hJ, memJ, hiJ, h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
have h : ¬LinearIndepOn R v J
Tactic: have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
have right : ∀ (f : ι →₀ R) (supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f)
  (sum_f :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0)
  (f_ne : f ≠ 0), ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
Tactic: obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
⊢ Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
have contrapose : ∀ (hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)), ¬LinearIndepOn R v I
Tactic: contrapose hIlinind
Cleared hypotheses: hIlinind
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
⊢ ¬LinearIndepOn R v I
have refine : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R I) f
Tactic: refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩