case succ
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set α
a✝ : ChainClosure r s✝
a_ih✝ : SuccChain r c₂ ⊆ s✝ ∨ s✝ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r s✝ ∨ SuccChain r s✝ ⊆ c₂

case union
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s✝ ∨ ⋃₀ s✝ ⊆ c₂
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₁ : ChainClosure r c₁
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂
induction hc₁
no goals
case union
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s✝ ∨ ⋃₀ s✝ ⊆ c₂
case union s _ ih =>
  refine' or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => _
  exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha
case inl
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

case inr
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
cases' ih with ih ih
no goals
case inl
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
exact Or.inl (ih.trans subset_succChain)
no goals
case inr
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃✝ s t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a✝¹ b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
hn : ¬SuccChain r c₂ ⊆ ⋃₀ s
a : Set α
ha : a ∈ s
⊢ a ⊆ c₂
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s ∨ ⋃₀ s ⊆ c₂
refine' or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => _
no goals
α : Type u_1
β : Type ?u.11219
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a✝¹ b x y : α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
hn : ¬SuccChain r c₂ ⊆ ⋃₀ s
a : Set α
ha : a ∈ s
⊢ a ⊆ c₂
exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha