awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ s, f i)
⊢ Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ s, span R (f i))

Tactic:
hd i s s.finite_toSet his

Premises used: SetLike.coe, Finset.finite_toSet
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ s, f i)
⊢ Disjoint (α := Submodule R M) (span R (f i)) (⨆ i ∈ s, span R (f i))

Tactic:
exact hd i s s.finite_toSet his

Premises used: SetLike.coe, Finset.finite_toSet
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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))
t : Finset ι
h : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), f i)
h₁ :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s) (ih : LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ s, f i)),
    LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i_1 ∈ insert i s, f i_1)
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ t, f i)

Tactic:
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

Premises used: Insert.insert, Finset.set_biUnion_insert, Submodule.span_iUnion₂
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
h h₁ h₂ : ∀ (t : Finset ι), LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ i ∈ t, f i)
⊢ LinearIndepOn.{u_4, u_2, u_4} (ι := M) R id (⋃ (i : ι), 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

Premises used: linearIndepOn_iUnion_of_directed, Insert.insert, directed_of_isDirected_le, Set.iUnion_subset_iUnion_const, Set.iUnion_eq_iUnion_finset, Set.iUnion_mono, Finset.set_biUnion_insert, Submodule.span_iUnion₂
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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)))
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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))
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)))
⊢ LinearIndependent R (M := 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

Premises used: LinearIndependent.of_linearIndepOn_id_range
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₂
neg : ∀ (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₂

Tactic:
by_cases h_cases : x₁ = y₁
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₁
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₂
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂

Tactic:
subst h_cases
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₂

Tactic:
Sigma.eq rfl ?_

Premises used: Sigma.eq, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₂))
pos :
  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)
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂

Tactic:
refine Sigma.eq rfl ?_

Premises used: Sigma.eq, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₂))
pos pos₁ :
  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₁ y₂).snd (β := fun (j : η) ↦ ιs j)) =
    (Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ y₂).snd (β := fun (a : η) ↦ ιs a)
⊢ 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)

Tactic:
rw [LinearIndependent.injective (hindep _) hxy]

Premises used: LinearIndependent.injective
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₁
x₃ :
  Membership.mem (γ := Submodule R M) (⨆ (i : η), ⨆ (_ : Membership.mem (γ := Set η) {y₁} i), span R (range (f i)))
    (f x₁ x₂)
⊢ f x₁ x₂ = 0

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 _))

Premises used: Set.mem_range_self, Set.eq_of_mem_singleton, Iff.mp, Submodule.subset_span, Submodule.disjoint_def, Singleton.singleton, Set.finite_singleton
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₁
rw : Membership.mem (γ := Submodule R M) (span R (range (f y₁))) (f x₁ x₂)
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : η), ⨆ (_ : Membership.mem (γ := Set η) {y₁} i), span R (range (f i)))
    (f x₁ x₂)

Tactic:
rw [iSup_singleton]

Premises used: iSup_singleton
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₁
rw : Membership.mem (γ := Submodule R M) (span R (range (f y₁))) (f y₁ y₂)
⊢ Membership.mem (γ := Submodule R M) (span R (range (f y₁))) (f x₁ x₂)

Tactic:
rw [hxy]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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 y₁ y₂)

Tactic:
subset_span (mem_range_self y₂)

Premises used: Set.mem_range_self, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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 y₁ y₂)

Tactic:
exact subset_span (mem_range_self y₂)

Premises used: Set.mem_range_self, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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

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₂)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₁
h0 : f x₁ x₂ = 0
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂

Tactic:
False.elim ((hindep x₁).ne_zero _ h0)

Premises used: LinearIndependent.ne_zero, False.elim
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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₁
h0 : f x₁ x₂ = 0
⊢ Sigma.mk (β := fun (j : η) ↦ ιs j) x₁ x₂ = Sigma.mk (β := fun (j : η) ↦ ιs j) y₁ y₂

Tactic:
exact False.elim ((hindep x₁).ne_zero _ h0)

Premises used: LinearIndependent.ne_zero, False.elim
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
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)))
⊢ 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:
rw [range_sigma_eq_iUnion_range]

Premises used: Set.range_sigma_eq_iUnion_range
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
    (⋃ (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:
apply linearIndepOn_id_iUnion_finite (fun j => (hindep j).linearIndepOn_id) hd

Premises used: linearIndepOn_id_iUnion_finite, LinearIndependent.linearIndepOn_id
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
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)
⊢ ∃ (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⟩

Premises used: exists_maximal_linearIndepOn'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
right : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
⊢ ∃ (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:
use I, hIlinind
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
⊢ I ⊆ I ∪ {i}

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
⊢ LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}

Tactic:
specialize hImaximal (I ∪ {i}) (by simp)

Premises used: Union.union, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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}
⊢ let J := I ∪ {i};
  LinearIndepOn R v J → I = J

Tactic:
set J := I ∪ {i} with hJ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
⊢ let J := I ∪ {i};
  J = I ∪ {i}

Tactic:
set J := I ∪ {i} with hJ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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}
⊢ ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I

Tactic:
simp [hJ]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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}
⊢ ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I

Tactic:
have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
⊢ i ∈ J

Tactic:
simp [J]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
⊢ i ∈ J

Tactic:
have hiJ : i ∈ J := by simp [J]