α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
b : α
hb : b ∈ s
hab : r₁ a b
this : a = b
⊢ r₁ b a
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
b : α
hb : b ∈ s
hab : r₁ a b
⊢ r₁ b a
have := eq_of_mem_maximals ha hb (h _ _ hab)
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
hb : a ∈ s
hab : r₁ a a
⊢ r₁ a a
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
b : α
hb : b ∈ s
hab : r₁ a b
this : a = b
⊢ r₁ b a
subst this
no goals
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a✝ b : α
inst✝ : IsAntisymm α r₂
h : ∀ (a b : α), r₁ a b → r₂ a b
a : α
ha : a ∈ maximals r₂ s
hb : a ∈ s
hab : r₁ a a
⊢ r₁ a a
exact hab