[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
⊢ IsChain r univ ↔ IsTrichotomous α r
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a b => _⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
h : IsChain r univ
a b : α
⊢ r a b ∨ a = b ∨ r b a
[PROOFSTEP]
rw [or_left_comm, or_iff_not_imp_left]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
h : IsChain r univ
a b : α
⊢ ¬a = b → r a b ∨ r b a
[PROOFSTEP]
exact h trivial trivial
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x x_1 => x ≤ x_1) (range f)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x x_1 => x ≤ x_1) (f '' univ)
[PROOFSTEP]
exact (isChain_of_trichotomous _).image (· ≤ ·) _ _ hf
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝ : IsRefl α r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ z,
    r ((fun x => f ↑x) { val := a, property := ha }) ((fun x => f ↑x) z) ∧
      r ((fun x => f ↑x) { val := b, property := hb }) ((fun x => f ↑x) z)
[PROOFSTEP]
simp only [hab, exists_prop, and_self_iff, Subtype.exists]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝ : IsRefl α r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ a, a ∈ c ∧ r (f b) (f a)
[PROOFSTEP]
exact ⟨b, hb, refl _⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
⊢ ∃ z x, r a z ∧ r b z ∧ r c z
[PROOFSTEP]
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) a mem1 b mem2 with ⟨z, mem4, H1, H2⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
⊢ ∃ z x, r a z ∧ r b z ∧ r c z
[PROOFSTEP]
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) z mem4 c mem3 with ⟨z', mem5, H3, H4⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c✝ c₁ c₂ c₃ s t : Set α
a✝ b✝ x y : α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
z' : α
mem5 : z' ∈ s
H3 : r z z'
H4 : r c z'
⊢ ∃ z x, r a z ∧ r b z ∧ r c z
[PROOFSTEP]
exact ⟨z', mem5, _root_.trans H1 H3, _root_.trans H2 H3, H4⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
have : IsChain r s ∧ SuperChain r s (choose h) := @choose_spec _ (fun t => IsChain r s ∧ SuperChain r s t) _
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∃ t, IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s (choose h)
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs : IsChain r s
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)
[PROOFSTEP]
rw [exists_and_left] at h 
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)
[PROOFSTEP]
simpa [SuccChain, dif_neg, h] using hs
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
simp only [IsMaxChain, not_and, not_forall, exists_prop, exists_and_left] at hs₂ 
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
obtain ⟨t, ht, hst⟩ := hs₂ hs₁
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t✝ : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)
[PROOFSTEP]
exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ s ⊆ SuccChain r s
[PROOFSTEP]
rw [exists_and_left] at h 
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ s ⊆ SuccChain r s
[PROOFSTEP]
simp [SuccChain, dif_neg, h, Subset.rfl]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
⊢ ChainClosure r ∅
[PROOFSTEP]
have : ChainClosure r (⋃₀ ∅) := ChainClosure.union fun a h => False.rec h
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
induction hc₁
[GOAL]
case succ
α : Type u_1
β : Type u_2
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_2
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₂
[PROOFSTEP]
case succ c₃ hc₃ ih =>
  cases' ih with ih ih
  · exact Or.inl (ih.trans subset_succChain)
  · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
case succ c₃ hc₃ ih =>
  cases' ih with ih ih
  · exact Or.inl (ih.trans subset_succChain)
  · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
cases' ih with ih ih
[GOAL]
case inl
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
exact Or.inl (ih.trans subset_succChain)
[GOAL]
case inr
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
[GOAL]
case union
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
refine' or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => _
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
induction hc₂ generalizing c₁ hc₁
[GOAL]
case succ
α : Type u_1
β : Type u_2
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_2
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✝
[PROOFSTEP]
case succ c₂ _
  ih =>
  refine' ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => _
  obtain rfl | h₂ := ih hc₁ h₁
  · exact Subset.rfl
  · exact h₂.trans subset_succChain
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
case succ c₂ _
  ih =>
  refine' ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => _
  obtain rfl | h₂ := ih hc₁ h₁
  · exact Subset.rfl
  · exact h₂.trans subset_succChain
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
refine' ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => _
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
obtain rfl | h₂ := ih hc₁ h₁
[GOAL]
case inl
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case inr
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
exact h₂.trans subset_succChain
[GOAL]
case union
α : Type u_1
β : Type u_2
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✝
[PROOFSTEP]
case union s _ ih =>
  apply Or.imp_left h.antisymm'
  apply by_contradiction
  simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
  intro c₃ hc₃ h₁ h₂
  obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
  · exact h₁ (subset_succChain.trans h)
  obtain h' | h' := ih c₃ hc₃ hc₁ h
  · exact h₁ h'.subset
  · exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
case union s _ ih =>
  apply Or.imp_left h.antisymm'
  apply by_contradiction
  simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
  intro c₃ hc₃ h₁ h₂
  obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
  · exact h₁ (subset_succChain.trans h)
  obtain h' | h' := ih c₃ hc₃ hc₁ h
  · exact h₁ h'.subset
  · exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply Or.imp_left h.antisymm'
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply by_contradiction
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
intro c₃ hc₃ h₁ h₂
[GOAL]
case a
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
[GOAL]
case a.inl
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact h₁ (subset_succChain.trans h)
[GOAL]
case a.inr
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain h' | h' := ih c₃ hc₃ hc₁ h
[GOAL]
case a.inr.inl
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact h₁ h'.subset
[GOAL]
case a.inr.inr
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
induction hc₁
[GOAL]
case succ
α : Type u_1
β : Type u_2
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_2
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₂
[PROOFSTEP]
case succ s₁ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
case succ s₁ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
[GOAL]
case union
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
case union s _ ih => exact sUnion_subset ih
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
case union s _ ih => exact sUnion_subset ih
[GOAL]
α : Type u_1
β : Type u_2
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₂
[PROOFSTEP]
exact sUnion_subset ih
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hc : ChainClosure r c
⊢ IsChain r c
[PROOFSTEP]
induction hc
[GOAL]
case succ
α : Type u_1
β : Type u_2
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_2
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✝)
[PROOFSTEP]
case succ c _ h => exact h.succ
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
case succ c _ h => exact h.succ
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact h.succ
[GOAL]
case union
α : Type u_1
β : Type u_2
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✝)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LE α
s✝ t✝ : Flag α
a : α
s t : Flag α
h : s.carrier = t.carrier
⊢ s = t
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : LE α
s t✝ : Flag α
a : α
t : Flag α
carrier✝ : Set α
Chain'✝ : IsChain (fun x x_1 => x ≤ x_1) carrier✝
max_chain'✝ : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x ≤ x_1) s → carrier✝ ⊆ s → carrier✝ = s
h : { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ } = t
[PROOFSTEP]
cases t
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝ : LE α
s t : Flag α
a : α
carrier✝¹ : Set α
Chain'✝¹ : IsChain (fun x x_1 => x ≤ x_1) carrier✝¹
max_chain'✝¹ : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x ≤ x_1) s → carrier✝¹ ⊆ s → carrier✝¹ = s
carrier✝ : Set α
Chain'✝ : IsChain (fun x x_1 => x ≤ x_1) carrier✝
max_chain'✝ : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x ≤ x_1) s → carrier✝ ⊆ s → carrier✝ = s
h :
  { carrier := carrier✝¹, Chain' := Chain'✝¹, max_chain' := max_chain'✝¹ }.carrier =
    { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }.carrier
⊢ { carrier := carrier✝¹, Chain' := Chain'✝¹, max_chain' := max_chain'✝¹ } =
    { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }
[PROOFSTEP]
congr
