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

case hd
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (i : ι) (t : Set ι),
    Set.Finite t →
      ¬i ∈ t →
        Disjoint (span R (Set.range fun x => single i (f i x)))
          (⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x)))
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R fun ix => single ix.fst (f ix.fst ix.snd)
apply @linearIndependent_iUnion_finite R _ _ _ _ ι φ fun i x => single i (f i x)
case hindep
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ LinearIndependent R fun x => single i (f i x)
case hindep
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (j : ι), LinearIndependent R fun x => single j (f j x)
intro i
case hindep
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
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)
case hindep
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ LinearIndependent R fun x => single i (f i x)
have h_disjoint : Disjoint (span R (range (f i))) (ker (lsingle i)) := by
  rw [ker_lsingle]
  exact disjoint_bot_right
no goals
case hindep
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
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)
apply (hf i).map h_disjoint
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ Disjoint (span R (Set.range (f i))) ⊥
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ Disjoint (span R (Set.range (f i))) (ker (lsingle i))
rw [ker_lsingle]
no goals
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ Disjoint (span R (Set.range (f i))) ⊥
exact disjoint_bot_right
case hd
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ Disjoint (span R (Set.range fun x => single i (f i x)))
    (⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x)))
case hd
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (i : ι) (t : Set ι),
    Set.Finite t →
      ¬i ∈ t →
        Disjoint (span R (Set.range fun x => single i (f i x)))
          (⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x)))
intro i t _ hit
case hd.refine'_1
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ ⨆ (a : ι) (_ : a ∈ {i}), LinearMap.range (lsingle a)

case hd.refine'_2
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x))) ≤
    ⨆ (a : ι) (_ : a ∈ t), LinearMap.range (lsingle a)
case hd
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ Disjoint (span R (Set.range fun x => single i (f i x)))
    (⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x)))
refine' (disjoint_lsingle_lsingle {i} t (disjoint_singleton_left.2 hit)).mono _ _
case hd.refine'_1
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(⨆ (a : ι) (_ : a ∈ {i}), LinearMap.range (lsingle a))
case hd.refine'_1
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ ⨆ (a : ι) (_ : a ∈ {i}), LinearMap.range (lsingle a)
rw [span_le]
case hd.refine'_1
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(LinearMap.range (lsingle i))
case hd.refine'_1
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(⨆ (a : ι) (_ : a ∈ {i}), LinearMap.range (lsingle a))
simp only [iSup_singleton]
case hd.refine'_1
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ↑(lsingle i)
case hd.refine'_1
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(LinearMap.range (lsingle i))
rw [range_coe]
no goals
case hd.refine'_1
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ↑(lsingle i)
apply range_comp_subset_range _ (lsingle i)
case hd.refine'_2
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i✝ ∈ t
i : ι
hi : i ∈ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ LinearMap.range (lsingle i)
case hd.refine'_2
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x))) ≤
    ⨆ (a : ι) (_ : a ∈ t), LinearMap.range (lsingle a)
refine' iSup₂_mono fun i hi => _
case hd.refine'_2
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i✝ ∈ t
i : ι
hi : i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ↑(lsingle i)
case hd.refine'_2
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i✝ ∈ t
i : ι
hi : i ∈ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ LinearMap.range (lsingle i)
rw [span_le, range_coe]
no goals
case hd.refine'_2
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_1
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i✝ ∈ t
i : ι
hi : i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ↑(lsingle i)
apply range_comp_subset_range _ (lsingle i)