-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndepOn_iUnion_of_directed {η : Type*} {s : η → Set ι} (hs : Directed (· ⊆ ·) s)
    (h : ∀ i, LinearIndepOn R v (s i)) : LinearIndepOn R v (⋃ i, s i)

Proof state:
case pos.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ LinearIndepOn R v t

Tactic:
rcases hs.finset_le fi.toFinset with ⟨i, hi⟩

Result:
case pos.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i
⊢ LinearIndepOn R v t

Proof state:
case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ i, s i
ft : t.Finite
⊢ LinearIndepOn R v t

Tactic:
rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩

Result:
case pos.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ LinearIndepOn R v t

Proof state:
case pos.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i
⊢ LinearIndepOn R v t

Tactic:
exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Result:
no goals

Proof state:
case neg.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
a✝ : ι
w✝ : Set ι
right✝ : a✝ ∈ w✝
i : η
h✝ : (fun x => s x) i = w✝
⊢ a✝ ∈ ∅

Tactic:
exact hη ⟨i⟩

Result:
no goals

Proof state:
case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
⊢ ⋃ x, s x ⊆ ∅

Tactic:
rintro _ ⟨_, ⟨i, _⟩, _⟩

Result:
case neg.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
a✝ : ι
w✝ : Set ι
right✝ : a✝ ∈ w✝
i : η
h✝ : (fun x => s x) i = w✝
⊢ a✝ ∈ ∅

Proof state:
case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
⊢ LinearIndepOn R v (⋃ i, s i)

Tactic:
refine linearIndepOn_of_finite (⋃ i, s i) fun t ht ft => ?_

Result:
case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
t : Set ι
ht : t ⊆ ⋃ i, s i
ft : t.Finite
⊢ LinearIndepOn R v t

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
⊢ LinearIndepOn R v (⋃ i, s i)

Tactic:
by_cases hη : Nonempty η

Result:
case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
⊢ LinearIndepOn R v (⋃ i, s i)

case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
⊢ LinearIndepOn R v (⋃ i, s i)