case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y ↔ x = y
constructor
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y
swap
case mpr
R : Type u_1
inst✝ : Rack R
x : R
⊢ x ◃ x = x ◃ x

case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y

case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
rintro rfl
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
case mpr
R : Type u_1
inst✝ : Rack R
x : R
⊢ x ◃ x = x ◃ x

case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
rfl
case mp
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = y
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
intro h
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x

R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
case mp
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = y
trans (x ◃ x) ◃⁻¹ x ◃ x
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x

R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]
no goals
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]