Theorem: Set.Finite.subset_biUnion_mono_iff (Matroid/ForMathlib/Data/Set/Finite.lean)

State before:
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
doimage : DirectedOn (fun x x_1 => x ⊆ x_1) (v '' a)
⊢ s ⊆ ⋃ i ∈ a, v i ↔ ∃ i ∈ a, s ⊆ v i
Tactic:
simpa using hs.subset_sUnion_directedOn_iff doimage (hne.image v)
State after:
no goals

State before:
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
⊢ DirectedOn (fun x x_1 => x ⊆ x_1) (v '' a)
Tactic:
rintro _ ⟨i, hi, rfl⟩ _ ⟨j, hj, rfl⟩
State after:
case intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z

State before:
case intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z
Tactic:
obtain ⟨k, hka, hik, hjk⟩ := ha i hi j hj
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
k : ι
hka : k ∈ a
hik : i ≤ k
hjk : j ≤ k
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
k : ι
hka : k ∈ a
hik : i ≤ k
hjk : j ≤ k
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z
Tactic:
exact ⟨v k, ⟨k, hka, rfl⟩, hv hik, hv hjk⟩
State after:
no goals