case pos
α : Type u_1
β : Type ?u.98
γ : Type ?u.101
δ : Type ?u.104
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : x = y
⊢ r x y

case neg
α : Type u_1
β : Type ?u.98
γ : Type ?u.101
δ : Type ?u.104
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : ¬x = y
⊢ r x y
α : Type u_1
β : Type ?u.98
γ : Type ?u.101
δ : Type ?u.104
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
⊢ r x y
by_cases hxy : x = y
no goals
case pos
α : Type u_1
β : Type ?u.98
γ : Type ?u.101
δ : Type ?u.104
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : x = y
⊢ r x y
exact hxy ▸ h x
no goals
case neg
α : Type u_1
β : Type ?u.98
γ : Type ?u.101
δ : Type ?u.104
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : ¬x = y
⊢ r x y
exact hr hxy