α : Type u_2
β : Type u_1
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)
α : Type u_2
β : Type u_1
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)
simp only [hab, exists_prop, and_self_iff, Subtype.exists]
no goals
α : Type u_2
β : Type u_1
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)
exact ⟨b, hb, refl _⟩