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

case union
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃ s t : Set α
a b x y : α
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ⋃₀ s✝ = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
h : c₁ ⊆ c₂
⊢ c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
induction hc₂ generalizing c₁ hc₁
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
h₁ : c₁ ⊆ c₂
⊢ SuccChain r c₁ ⊆ SuccChain r c₂
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
⊢ SuccChain r c₂ = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r c₂
refine' ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => _
case inl
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
hc₁ : ChainClosure r c₂
h : c₂ ⊆ SuccChain r c₂
h₁ : c₂ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₂

case inr
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
h₁ : c₁ ⊆ c₂
h₂ : SuccChain r c₁ ⊆ c₂
⊢ SuccChain r c₁ ⊆ SuccChain r c₂
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
h₁ : c₁ ⊆ c₂
⊢ SuccChain r c₁ ⊆ SuccChain r c₂
obtain rfl | h₂ := ih hc₁ h₁
no goals
case inl
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
hc₁ : ChainClosure r c₂
h : c₂ ⊆ SuccChain r c₂
h₁ : c₂ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₂
exact Subset.rfl
no goals
case inr
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂✝ c₃ s t : Set α
a b x y : α
c₂ : Set α
a✝ : ChainClosure r c₂
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ c₂ → c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r c₂
h₁ : c₁ ⊆ c₂
h₂ : SuccChain r c₁ ⊆ c₂
⊢ SuccChain r c₁ ⊆ SuccChain r c₂
exact h₂.trans subset_succChain
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ⋃₀ s = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
apply Or.imp_left h.antisymm'
case a
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ¬(⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s) → False
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
apply by_contradiction
case a
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ∀ (x : Set α), x ∈ s → ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s → False
case a
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ¬(⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s) → False
simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
case a
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
⊢ False
case a
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
⊢ ∀ (x : Set α), x ∈ s → ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s → False
intro c₃ hc₃ h₁ h₂
case a.inl
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : SuccChain r c₃ ⊆ c₁
⊢ False

case a.inr
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
⊢ False
case a
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
⊢ False
obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
case a.inr.inl
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False

case a.inr.inr
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False
case a.inr
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
⊢ False
obtain h' | h' := ih c₃ hc₃ hc₁ h
no goals
case a.inl
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : SuccChain r c₃ ⊆ c₁
⊢ False
exact h₁ (subset_succChain.trans h)
no goals
case a.inr.inl
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False
exact h₁ h'.subset
no goals
case a.inr.inr
α : Type u_1
β : Type ?u.11677
r : α → α → Prop
c c₂ c₃✝ s✝ t : Set α
a b x y : α
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False
exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)