case refine_1
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
⊢ r b c

case refine_2
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r b c
⊢ r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
⊢ Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
case refine_1
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
case refine_1
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
⊢ r b c
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
no goals
case refine_1
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
exact h a⁻¹ bc
case refine_2
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
case refine_2
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r b c
⊢ r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
no goals
case refine_2
M : Type ?u.747
N : Type u_1
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
exact h a⁻¹ bc