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

case union
α : Type u_1
β : Type ?u.13163
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → a ⊆ c₂
⊢ ⋃₀ s✝ ⊆ c₂
α : Type u_1
β : Type ?u.13163
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
⊢ c₁ ⊆ c₂
induction hc₁
case union
α : Type u_1
β : Type ?u.13163
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → a ⊆ c₂
⊢ ⋃₀ s✝ ⊆ c₂
case succ
α : Type u_1
β : Type ?u.13163
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set α
a✝ : ChainClosure r s✝
a_ih✝ : s✝ ⊆ c₂
⊢ SuccChain r s✝ ⊆ c₂

case union
α : Type u_1
β : Type ?u.13163
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → a ⊆ c₂
⊢ ⋃₀ s✝ ⊆ c₂
case succ s₁ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
no goals
case union
α : Type u_1
β : Type ?u.13163
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s✝ → ChainClosure r a
a_ih✝ : ∀ (a : Set α), a ∈ s✝ → a ⊆ c₂
⊢ ⋃₀ s✝ ⊆ c₂
case union s _ ih => exact sUnion_subset ih
no goals
α : Type u_1
β : Type ?u.13163
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s₁ : Set α
hc₁ : ChainClosure r s₁
h : s₁ ⊆ c₂
⊢ SuccChain r s₁ ⊆ c₂
exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
no goals
α : Type u_1
β : Type ?u.13163
r : α → α → Prop
c c₁ c₂ c₃ s✝ t : Set α
a b x y : α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s : Set (Set α)
a✝ : ∀ (a : Set α), a ∈ s → ChainClosure r a
ih : ∀ (a : Set α), a ∈ s → a ⊆ c₂
⊢ ⋃₀ s ⊆ c₂
exact sUnion_subset ih