Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y ↔ y * x * y⁻¹ = x
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
⊢ x ◃ y = y ↔ y ◃ x = x
dsimp [Conj] at *
case mp
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y → y * x * y⁻¹ = x

case mpr
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
⊢ y * x * y⁻¹ = x → x * y * x⁻¹ = y
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y ↔ y * x * y⁻¹ = x
constructor
no goals
case mp
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y → y * x * y⁻¹ = x

case mpr
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
⊢ y * x * y⁻¹ = x → x * y * x⁻¹ = y
repeat' intro h; conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp
case mpr
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
⊢ x * y * x⁻¹ = y
case mpr
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
⊢ y * x * y⁻¹ = x → x * y * x⁻¹ = y
intro h
no goals
case mpr
Q : Type ?u.63822
inst✝¹ : Quandle Q
G : Type u_1
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
⊢ x * y * x⁻¹ = y
conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp