-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_iUnion_finite {η : Type*} {ιs : η → Type*} {f : ∀ j : η, ιs j → M}
    (hindep : ∀ j, LinearIndependent R (f j))
    (hd : ∀ i, ∀ t : Set η,
      t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))) :
    LinearIndependent R fun ji : Σ j, ιs j => f ji.1 ji.2

Proof state:
case neg
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

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

Result:
case neg
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
h0 : f x₁ x₂ = 0
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

Proof state:
case hf
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ Injective fun ji => f ji.fst ji.snd

Tactic:
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy

Result:
case hf.mk.mk
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨y₁, y₂⟩
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))

Tactic:
simp only at hxy

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))

Proof state:
case a
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ LinearIndepOn R id (⋃ a, range fun b => f ⟨a, b⟩.fst ⟨a, b⟩.snd)

Tactic:
apply linearIndepOn_id_iUnion_finite (fun j => (hindep j).linearIndepOn_id) hd

Result:
no goals

Proof state:
case pos
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ ⟨x₁, x₂⟩ = ⟨x₁, y₂⟩

Tactic:
refine Sigma.eq rfl ?_

Result:
case pos
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ Eq.recOn ⋯ ⟨x₁, x₂⟩.snd = ⟨x₁, y₂⟩.snd

Proof state:
case pos
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ Eq.recOn ⋯ ⟨x₁, x₂⟩.snd = ⟨x₁, y₂⟩.snd

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

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))

Tactic:
rw [hxy]

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : f x₁ x₂ = f y₁ y₂
h_cases : ¬x₁ = y₁
⊢ f y₁ y₂ ∈ span R (range (f y₁))

Proof state:
case a
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ LinearIndepOn R id (range fun ji => f ji.fst ji.snd)

Tactic:
rw [range_sigma_eq_iUnion_range]

Result:
case a
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ LinearIndepOn R id (⋃ a, range fun b => f ⟨a, b⟩.fst ⟨a, b⟩.snd)