[GOAL]
M : Type u_1
N : Type u_2
μ : 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
[PROOFSTEP]
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
[GOAL]
case refine_1
M : Type u_1
N : Type u_2
μ : 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
[PROOFSTEP]
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
[GOAL]
case refine_1
M : Type u_1
N : Type u_2
μ : 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))
[PROOFSTEP]
exact h a⁻¹ bc
[GOAL]
case refine_2
M : Type u_1
N : Type u_2
μ : 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)
[PROOFSTEP]
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc 
[GOAL]
case refine_2
M : Type u_1
N : Type u_2
μ : 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)
[PROOFSTEP]
exact h a⁻¹ bc
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
⊢ Covariant N N (swap fun x x_1 => x * x_1) r ↔ Contravariant N N (swap fun x x_1 => x * x_1) r
[PROOFSTEP]
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
[GOAL]
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (swap fun x x_1 => x * x_1) r
a b c : N
bc : r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
⊢ r b c
[PROOFSTEP]
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
[GOAL]
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (swap fun x x_1 => x * x_1) r
a b c : N
bc : r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)
[PROOFSTEP]
exact h a⁻¹ bc
[GOAL]
case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (swap fun x x_1 => x * x_1) r
a b c : N
bc : r b c
⊢ r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
[PROOFSTEP]
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc 
[GOAL]
case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (swap fun x x_1 => x * x_1) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
[PROOFSTEP]
exact h a⁻¹ bc
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
⊢ (Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
[PROOFSTEP]
intro h a b c bc
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Covariant M N μ fun x x_1 => x < x_1
a : M
b c : N
bc : b ≤ c
⊢ μ a b ≤ μ a c
[PROOFSTEP]
rcases le_iff_eq_or_lt.mp bc with (rfl | bc)
[GOAL]
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Covariant M N μ fun x x_1 => x < x_1
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b
[PROOFSTEP]
exact rfl.le
[GOAL]
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Covariant M N μ fun x x_1 => x < x_1
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c
[PROOFSTEP]
exact (h _ bc).le
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
⊢ (Contravariant M N μ fun x x_1 => x ≤ x_1) → Contravariant M N μ fun x x_1 => x < x_1
[PROOFSTEP]
refine fun h a b c bc ↦ lt_iff_le_and_ne.mpr ⟨h a bc.le, ?_⟩
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Contravariant M N μ fun x x_1 => x ≤ x_1
a : M
b c : N
bc : (fun x x_1 => x < x_1) (μ a b) (μ a c)
⊢ b ≠ c
[PROOFSTEP]
rintro rfl
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Contravariant M N μ fun x x_1 => x ≤ x_1
a : M
b : N
bc : μ a b < μ a b
⊢ False
[PROOFSTEP]
exact lt_irrefl _ bc
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : CommSemigroup N
⊢ Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r
[PROOFSTEP]
rw [flip_mul]
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : CommSemigroup N
⊢ Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
[PROOFSTEP]
rw [flip_mul]
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : N
bc : b < c
⊢ a * b < a * c
[PROOFSTEP]
cases' lt_iff_le_and_ne.mp bc with bc cb
[GOAL]
case intro
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : N
bc✝ : b < c
bc : b ≤ c
cb : b ≠ c
⊢ a * b < a * c
[PROOFSTEP]
exact lt_iff_le_and_ne.mpr ⟨CovariantClass.elim a bc, (mul_ne_mul_right a).mpr cb⟩
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : N
bc : b < c
⊢ swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c
[PROOFSTEP]
cases' lt_iff_le_and_ne.mp bc with bc cb
[GOAL]
case intro
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : N
bc✝ : b < c
bc : b ≤ c
cb : b ≠ c
⊢ swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c
[PROOFSTEP]
exact lt_iff_le_and_ne.mpr ⟨CovariantClass.elim a bc, (mul_ne_mul_left a).mpr cb⟩
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : a * b ≤ a * c
⊢ b ≤ c
[PROOFSTEP]
cases' le_iff_eq_or_lt.mp bc with h h
[GOAL]
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : a * b ≤ a * c
h : a * b = a * c
⊢ b ≤ c
[PROOFSTEP]
exact ((mul_right_inj a).mp h).le
[GOAL]
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : a * b ≤ a * c
h : a * b < a * c
⊢ b ≤ c
[PROOFSTEP]
exact (ContravariantClass.elim _ h).le
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : swap (fun x x_1 => x * x_1) a b ≤ swap (fun x x_1 => x * x_1) a c
⊢ b ≤ c
[PROOFSTEP]
cases' le_iff_eq_or_lt.mp bc with h h
[GOAL]
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : swap (fun x x_1 => x * x_1) a b ≤ swap (fun x x_1 => x * x_1) a c
h : swap (fun x x_1 => x * x_1) a b = swap (fun x x_1 => x * x_1) a c
⊢ b ≤ c
[PROOFSTEP]
exact ((mul_left_inj a).mp h).le
[GOAL]
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : swap (fun x x_1 => x * x_1) a b ≤ swap (fun x x_1 => x * x_1) a c
h : swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c
⊢ b ≤ c
[PROOFSTEP]
exact (ContravariantClass.elim _ h).le
