-- Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean
theorem linearIndependent_single {φ : ι → Type*} {f : ∀ ι, φ ι → M}
    (hf : ∀ i, LinearIndependent R (f i)) :
    LinearIndependent R fun ix : Σi, φ i => single ix.1 (f ix.1 ix.2)

Proof state:
case hd.refine_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ ⨆ i ∈ t, span R (Set.range fun x => single i (f i x)) ≤ ⨆ a ∈ t, LinearMap.range (lsingle a)

Tactic:
refine iSup₂_mono fun i hi => ?_

Result:
case hd.refine_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : t.Finite
hit : i✝ ∉ t
i : ι
hi : i ∈ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ LinearMap.range (lsingle i)

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R fun ix => single ix.fst (f ix.fst ix.snd)

Tactic:
apply @linearIndependent_iUnion_finite R _ _ _ _ ι φ fun i x => single i (f i x)

Result:
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (j : ι), LinearIndependent R fun x => single j (f j x)

case hd
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (i : ι) (t : Set ι),
    t.Finite →
      i ∉ t →
        Disjoint (span R (Set.range fun x => single i (f i x))) (⨆ i ∈ t, span R (Set.range fun x => single i (f i x)))

Proof state:
case hd.refine_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : t.Finite
hit : i✝ ∉ t
i : ι
hi : i ∈ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ LinearMap.range (lsingle i)

Tactic:
rw [span_le, range_coe]

Result:
case hd.refine_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : t.Finite
hit : i✝ ∉ t
i : ι
hi : i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ⇑(lsingle i)

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ Disjoint (span R (Set.range (f i))) ⊥

Tactic:
exact disjoint_bot_right

Result:
no goals

Proof state:
case hd.refine_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : t.Finite
hit : i✝ ∉ t
i : ι
hi : i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ⇑(lsingle i)

Tactic:
apply range_comp_subset_range _ (lsingle i)

Result:
no goals

Proof state:
case hd.refine_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(LinearMap.range (lsingle i))

Tactic:
rw [range_coe]

Result:
case hd.refine_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ⇑(lsingle i)

Proof state:
case hd.refine_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(⨆ a ∈ {i}, LinearMap.range (lsingle a))

Tactic:
simp only [iSup_singleton]

Result:
case hd.refine_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(LinearMap.range (lsingle i))

Proof state:
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ LinearIndependent R fun x => single i (f i x)

Tactic:
have h_disjoint : Disjoint (span R (range (f i))) (ker (lsingle i)) := by
  rw [ker_lsingle]
  exact disjoint_bot_right

Result:
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
h_disjoint : Disjoint (span R (Set.range (f i))) (ker (lsingle i))
⊢ LinearIndependent R fun x => single i (f i x)

Proof state:
case hd.refine_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ⇑(lsingle i)

Tactic:
apply range_comp_subset_range _ (lsingle i)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ Disjoint (span R (Set.range (f i))) (ker (lsingle i))

Tactic:
rw [ker_lsingle]

Result:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ Disjoint (span R (Set.range (f i))) ⊥

Proof state:
case hd
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ Disjoint (span R (Set.range fun x => single i (f i x))) (⨆ i ∈ t, span R (Set.range fun x => single i (f i x)))

Tactic:
refine (disjoint_lsingle_lsingle {i} t (disjoint_singleton_left.2 hit)).mono ?_ ?_

Result:
case hd.refine_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ ⨆ a ∈ {i}, LinearMap.range (lsingle a)

case hd.refine_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : t.Finite
hit : i ∉ t
⊢ ⨆ i ∈ t, span R (Set.range fun x => single i (f i x)) ≤ ⨆ a ∈ t, LinearMap.range (lsingle a)