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

State before:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
⊢ s ⊆ ⋃₀ C ↔ ∃ t ∈ C, s ⊆ t
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨t, ht, hst⟩ ↦ subset_sUnion_of_subset _ _ hst ht⟩
State after:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∃ t ∈ C, s ⊆ t

State before:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∃ t ∈ C, s ⊆ t
Tactic:
apply hs.induction_on' (C := fun x ↦ ∃ u ∈ C, x ⊆ u) ⟨_, hne.some_mem,empty_subset _⟩
State after:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∀ {a : α} {s_1 : Set α}, a ∈ s → s_1 ⊆ s → a ∉ s_1 → (∃ u ∈ C, s_1 ⊆ u) → ∃ u ∈ C, insert a s_1 ⊆ u

State before:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∀ {a : α} {s_1 : Set α}, a ∈ s → s_1 ⊆ s → a ∉ s_1 → (∃ u ∈ C, s_1 ⊆ u) → ∃ u ∈ C, insert a s_1 ⊆ u
Tactic:
rintro a t has - - ⟨u, huC, htu⟩
State after:
case intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
⊢ ∃ u ∈ C, insert a t ⊆ u

State before:
case intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
⊢ ∃ u ∈ C, insert a t ⊆ u
Tactic:
obtain ⟨v, hvC, hav⟩ := h has
State after:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
v : Set α
hvC : v ∈ C
hav : a ∈ v
⊢ ∃ u ∈ C, insert a t ⊆ u

State before:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
v : Set α
hvC : v ∈ C
hav : a ∈ v
⊢ ∃ u ∈ C, insert a t ⊆ u
Tactic:
obtain ⟨z, hzC, huz, hvz⟩ := hC _ huC _ hvC
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
v : Set α
hvC : v ∈ C
hav : a ∈ v
z : Set α
hzC : z ∈ C
huz : u ⊆ z
hvz : v ⊆ z
⊢ ∃ u ∈ C, insert a t ⊆ u

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
v : Set α
hvC : v ∈ C
hav : a ∈ v
z : Set α
hzC : z ∈ C
huz : u ⊆ z
hvz : v ⊆ z
⊢ ∃ u ∈ C, insert a t ⊆ u
Tactic:
exact ⟨z, hzC, insert_subset (hvz hav) (htu.trans huz)⟩
State after:
no goals