case succ
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
s✝ : Set α
a✝ : ChainClosure r s✝
a_ih✝ : IsChain r s✝
⊢ IsChain r (SuccChain r s✝)

case union
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c 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✝ → IsChain r a
⊢ IsChain r (⋃₀ s✝)
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc : ChainClosure r c
⊢ IsChain r c
induction hc
case union
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c 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✝ → IsChain r a
⊢ IsChain r (⋃₀ s✝)
case succ
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
s✝ : Set α
a✝ : ChainClosure r s✝
a_ih✝ : IsChain r s✝
⊢ IsChain r (SuccChain r s✝)

case union
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c 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✝ → IsChain r a
⊢ IsChain r (⋃₀ s✝)
case succ c _ h => exact h.succ
no goals
case union
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c 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✝ → IsChain r a
⊢ IsChain r (⋃₀ s✝)
case union s hs h =>
  exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
    ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
      h t₁ ht₁ hc₁ (ht hc₂) hneq
no goals
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a b x y : α
c : Set α
a✝ : ChainClosure r c
h : IsChain r c
⊢ IsChain r (SuccChain r c)
exact h.succ
no goals
α : Type u_1
β : Type ?u.13781
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
s : Set (Set α)
hs : ∀ (a : Set α), a ∈ s → ChainClosure r a
h : ∀ (a : Set α), a ∈ s → IsChain r a
⊢ IsChain r (⋃₀ s)
exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
  ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
    h t₁ ht₁ hc₁ (ht hc₂) hneq