ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ LinearIndependent R fun x => ↑x
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ LinearIndependent R fun x => ↑x
rw [iUnion_eq_iUnion_finset f]
case hs
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => ⋃ (i_1 : ι) (_ : i_1 ∈ i), f i_1

case h
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ ∀ (i : Finset ι), LinearIndependent R fun x => ↑x
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ LinearIndependent R fun x => ↑x
apply linearIndependent_iUnion_of_directed
case h
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
t : Finset ι
⊢ LinearIndependent R fun x => ↑x
case h
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ ∀ (i : Finset ι), LinearIndependent R fun x => ↑x
intro t
case h.empty
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ LinearIndependent R fun x => ↑x

case h.insert
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
i : ι
s : Finset ι
his : ¬i ∈ s
ih : LinearIndependent R fun x => ↑x
⊢ LinearIndependent R fun x => ↑x
case h
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
t : Finset ι
⊢ LinearIndependent R fun x => ↑x
induction' t using Finset.induction_on with i s his ih
case hs.H
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ ∀ ⦃i j : Finset ι⦄, i ≤ j → (⋃ (i_1 : ι) (_ : i_1 ∈ i), f i_1) ⊆ ⋃ (i : ι) (_ : i ∈ j), f i
case hs
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => ⋃ (i_1 : ι) (_ : i_1 ∈ i), f i_1
apply directed_of_sup
no goals
case hs.H
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ ∀ ⦃i j : Finset ι⦄, i ≤ j → (⋃ (i_1 : ι) (_ : i_1 ∈ i), f i_1) ⊆ ⋃ (i : ι) (_ : i ∈ j), f i
exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h
case h.empty
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ (⋃ (i : ι) (_ : i ∈ ∅), f i) ⊆ ∅
case h.empty
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ LinearIndependent R fun x => ↑x
refine' (linearIndependent_empty R M).mono _
no goals
case h.empty
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
⊢ (⋃ (i : ι) (_ : i ∈ ∅), f i) ⊆ ∅
simp
case h.insert
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
i : ι
s : Finset ι
his : ¬i ∈ s
ih : LinearIndependent R fun x => ↑x
⊢ LinearIndependent R fun x => ↑x
case h.insert
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
i : ι
s : Finset ι
his : ¬i ∈ s
ih : LinearIndependent R fun x => ↑x
⊢ LinearIndependent R fun x => ↑x
rw [Finset.set_biUnion_insert]
case h.insert
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
i : ι
s : Finset ι
his : ¬i ∈ s
ih : LinearIndependent R fun x => ↑x
⊢ Disjoint (span R (f i)) (span R (⋃ (x : ι) (_ : x ∈ s), f x))
case h.insert
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
i : ι
s : Finset ι
his : ¬i ∈ s
ih : LinearIndependent R fun x => ↑x
⊢ LinearIndependent R fun x => ↑x
refine' (hl _).union ih _
case h.insert
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
i : ι
s : Finset ι
his : ¬i ∈ s
ih : LinearIndependent R fun x => ↑x
⊢ Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ s), span R (f i))
case h.insert
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
i : ι
s : Finset ι
his : ¬i ∈ s
ih : LinearIndependent R fun x => ↑x
⊢ Disjoint (span R (f i)) (span R (⋃ (x : ι) (_ : x ∈ s), f x))
rw [span_iUnion₂]
no goals
case h.insert
ι✝ : Type u'
ι' : Type ?u.381677
R : Type u_3
K : Type ?u.381683
M : Type u_2
M' : Type ?u.381689
M'' : Type ?u.381692
V : Type u
V' : Type ?u.381697
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
f : ι → Set M
hl : ∀ (i : ι), LinearIndependent R fun x => ↑x
hd : ∀ (i : ι) (t : Set ι), Set.Finite t → ¬i ∈ t → Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ t), span R (f i))
i : ι
s : Finset ι
his : ¬i ∈ s
ih : LinearIndependent R fun x => ↑x
⊢ Disjoint (span R (f i)) (⨆ (i : ι) (_ : i ∈ s), span R (f i))
exact hd i s s.finite_toSet his