Theorem: Logic.Relation.TightApartness.eq_iff_not_apart (GMLInit/Logic/Equivalence.lean)

State before:
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ x = y ↔ ¬r x y
Tactic:
constructor
State after:
case mp
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ x = y → ¬r x y

case mpr
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ ¬r x y → x = y

State before:
case mp
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ x = y → ¬r x y
Tactic:
intro | rfl => irreflexivity
State after:
no goals

State before:
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
x✝ : x = y
⊢ ¬r x x
Tactic:
irreflexivity
State after:
no goals

State before:
case mpr
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ ¬r x y → x = y
Tactic:
exact TightApartness.tight
State after:
no goals