Theorem: Set.subset_mem_chain_of_finite (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
⊢ ∅ ⊆ ⋃₀ c → ∃ t ∈ c, ∅ ⊆ t
Tactic:
rcases hc with ⟨t, ht⟩
State after:
case intro
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
⊢ ∅ ⊆ ⋃₀ c → ∃ t ∈ c, ∅ ⊆ t

State before:
case intro
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
⊢ ∅ ⊆ ⋃₀ c → ∃ t ∈ c, ∅ ⊆ t
Tactic:
intro
State after:
case intro
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
a✝ : ∅ ⊆ ⋃₀ c
⊢ ∃ t ∈ c, ∅ ⊆ t

State before:
case intro
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
a✝ : ∅ ⊆ ⋃₀ c
⊢ ∃ t ∈ c, ∅ ⊆ t
Tactic:
exact ⟨t, ht, by simp⟩
State after:
no goals

State before:
α : Type u_1
c : Set (Set α)
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
t : Set α
ht : t ∈ c
a✝ : ∅ ⊆ ⋃₀ c
⊢ ∅ ⊆ t
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hfin : s.Finite
⊢ ∀ {a : α} {s : Set α}, a ∉ s → s.Finite → (s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t) → insert a s ⊆ ⋃₀ c → ∃ t ∈ c, insert a s ⊆ t
Tactic:
intro a s _ _ ih h
State after:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, insert a s ⊆ t

State before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
have : ∃ t ∈ c, s ⊆ t := ih (subset_trans (Set.subset_insert a s) h)
State after:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
this : ∃ t ∈ c, s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t

State before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
this : ∃ t ∈ c, s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
rcases this with ⟨t, htc, ht⟩
State after:
case intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t

State before:
case intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
have : ∃ u ∈ c, a ∈ u := by simp [Set.insert_subset_iff] at h; exact h.1
State after:
case intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
this : ∃ u ∈ c, a ∈ u
⊢ ∃ t ∈ c, insert a s ⊆ t

State before:
case intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
this : ∃ u ∈ c, a ∈ u
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
rcases this with ⟨u, huc, hu⟩
State after:
case intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
⊢ ∃ t ∈ c, insert a s ⊆ t

State before:
case intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
have : ∃ z ∈ c, t ⊆ z ∧ u ⊆ z := IsChain.directedOn hchain t htc u huc
State after:
case intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
this : ∃ z ∈ c, t ⊆ z ∧ u ⊆ z
⊢ ∃ t ∈ c, insert a s ⊆ t

State before:
case intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
this : ∃ z ∈ c, t ⊆ z ∧ u ⊆ z
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
rcases this with ⟨z, hzc, htz, huz⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
z : Set α
hzc : z ∈ c
htz : t ⊆ z
huz : u ⊆ z
⊢ ∃ t ∈ c, insert a s ⊆ t

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
u : Set α
huc : u ∈ c
hu : a ∈ u
z : Set α
hzc : z ∈ c
htz : t ⊆ z
huz : u ⊆ z
⊢ ∃ t ∈ c, insert a s ⊆ t
Tactic:
exact ⟨z, hzc, Set.insert_subset (huz hu) (Set.Subset.trans ht htz)⟩
State after:
no goals

State before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
h : insert a s ⊆ ⋃₀ c
t : Set α
htc : t ∈ c
ht : s ⊆ t
⊢ ∃ u ∈ c, a ∈ u
Tactic:
simp [Set.insert_subset_iff] at h
State after:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
t : Set α
htc : t ∈ c
ht : s ⊆ t
h : (∃ t ∈ c, a ∈ t) ∧ s ⊆ ⋃₀ c
⊢ ∃ u ∈ c, a ∈ u

State before:
α : Type u_1
c : Set (Set α)
hc : c.Nonempty
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
s✝ : Set α
hfin : s✝.Finite
a : α
s : Set α
a✝¹ : a ∉ s
a✝ : s.Finite
ih : s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
t : Set α
htc : t ∈ c
ht : s ⊆ t
h : (∃ t ∈ c, a ∈ t) ∧ s ⊆ ⋃₀ c
⊢ ∃ u ∈ c, a ∈ u
Tactic:
exact h.1
State after:
no goals