-- Mathlib/Order/Chain.lean
theorem chainClosure_succ_total (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂)
    (h : c₁ ⊆ c₂) : c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂

Proof state:
case union.a.inr.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Tactic:
exact h₁ h'.subset

Result:
no goals

Proof state:
case union.a.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Tactic:
obtain h' | h' := ih c₃ hc₃ hc₁ h

Result:
case union.a.inr.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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 union.a.inr.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Proof state:
case union.a
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Tactic:
obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃

Result:
case union.a.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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 union.a.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Proof state:
case succ.inr
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
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✝
h₁ : c₁ ⊆ s✝
h₂ : SuccChain r c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Tactic:
exact h₂.trans subset_succChain

Result:
no goals

Proof state:
case succ
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
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✝

Tactic:
refine ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => ?_

Result:
case succ
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
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✝
h₁ : c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Proof state:
case succ
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
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✝
h₁ : c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Tactic:
obtain rfl | h₂ := ih hc₁ h₁

Result:
case succ.inl
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
hc₁ : ChainClosure r s✝
h : s✝ ⊆ SuccChain r s✝
h₁ : s✝ ⊆ s✝
⊢ SuccChain r s✝ ⊆ SuccChain r s✝

case succ.inr
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
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✝
h₁ : c₁ ⊆ s✝
h₂ : SuccChain r c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Proof state:
case union.a
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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 ∈ s✝, ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False

Tactic:
intro c₃ hc₃ h₁ h₂

Result:
case union.a
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Proof state:
case succ.inl
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
hc₁ : ChainClosure r s✝
h : s✝ ⊆ SuccChain r s✝
h₁ : s✝ ⊆ s✝
⊢ SuccChain r s✝ ⊆ SuccChain r s✝

Tactic:
exact Subset.rfl

Result:
no goals

Proof state:
case union.a.inr.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Tactic:
exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)

Result:
no goals

Proof state:
case union.a
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Tactic:
simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]

Result:
case union.a
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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 ∈ s✝, ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False

Proof state:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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✝

Tactic:
apply by_contradiction

Result:
case union.a
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Proof state:
case union.a.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ 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

Tactic:
exact h₁ (subset_succChain.trans h)

Result:
no goals