[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
h : a * b ≤ c * d
⊢ min a b ≤ max c d
[PROOFSTEP]
simp_rw [min_le_iff, le_max_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b
[PROOFSTEP]
exact mul_lt_mul_of_lt_of_lt h.1.1 h.2.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ a * b
⊢ ?m.15077 h * 1 ≤ ?m.15077 h * b
[PROOFSTEP]
simpa only [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a * b ≤ a
⊢ ?m.15584 h * b ≤ ?m.15584 h * 1
[PROOFSTEP]
simpa only [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : b ≤ a * b
⊢ 1 * ?m.16128 h ≤ a * ?m.16128 h
[PROOFSTEP]
simpa only [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a * b ≤ b
⊢ a * ?m.16669 h ≤ 1 * ?m.16669 h
[PROOFSTEP]
simpa only [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ≤ a * b ↔ a * 1 ≤ a * b
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ≤ b * a ↔ 1 * a ≤ b * a
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * b ≤ a ↔ a * b ≤ a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * b ≤ b ↔ a * b ≤ 1 * b
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : a < a * b
⊢ ?m.21985 h * 1 < ?m.21985 h * b
[PROOFSTEP]
simpa only [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : a * b < a
⊢ ?m.22488 h * b < ?m.22488 h * 1
[PROOFSTEP]
simpa only [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : b < a * b
⊢ 1 * ?m.23024 h < a * ?m.23024 h
[PROOFSTEP]
simpa only [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : a * b < b
⊢ a * ?m.23557 h < 1 * ?m.23557 h
[PROOFSTEP]
simpa only [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
⊢ a < a * b ↔ a * 1 < a * b
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
⊢ a < b * a ↔ 1 * a < b * a
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
⊢ a * b < a ↔ a * b < a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
⊢ a * b < b ↔ a * b < 1 * b
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a = 1 ∧ b = 1 → a * b = 1
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha hb : 1 ≤ 1
⊢ 1 * 1 = 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
refine' ⟨fun h ↦ _, by rintro ⟨rfl, rfl⟩; rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ → a₂ * b₂ ≤ a₁ * b₁
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ b₁ : α
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁ * b₁ ≤ a₁ * b₁
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₂ * b₂ ≤ a₁ * b₁
⊢ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
simp only [eq_iff_le_not_lt, ha, hb, true_and]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₂ * b₂ ≤ a₁ * b₁
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
[PROOFSTEP]
refine' ⟨fun ha ↦ h.not_lt _, fun hb ↦ h.not_lt _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha✝ : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₂ * b₂ ≤ a₁ * b₁
ha : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h : a₂ * b₂ ≤ a₁ * b₁
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
{exact mul_lt_mul_of_lt_of_le ha hb
}
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha✝ : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₂ * b₂ ≤ a₁ * b₁
ha : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
exact mul_lt_mul_of_lt_of_le ha hb
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h : a₂ * b₂ ≤ a₁ * b₁
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
{exact mul_lt_mul_of_le_of_lt ha hb
}
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : MulOneClass α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h : a₂ * b₂ ≤ a₁ * b₁
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
[PROOFSTEP]
exact mul_lt_mul_of_le_of_lt ha hb
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
⊢ ∃ b, b * b ≤ a
[PROOFSTEP]
by_cases h : a < 1
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a
[PROOFSTEP]
use a
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
⊢ a * a ≤ a
[PROOFSTEP]
have : a * a < a * 1 := mul_lt_mul_left' h a
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a
[PROOFSTEP]
rw [mul_one] at this 
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a
[PROOFSTEP]
exact le_of_lt this
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 1
⊢ ∃ b, b * b ≤ a
[PROOFSTEP]
use 1
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 1
⊢ 1 * 1 ≤ a
[PROOFSTEP]
push_neg at h 
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a : α
h : 1 ≤ a
⊢ 1 * 1 ≤ a
[PROOFSTEP]
rwa [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d
[PROOFSTEP]
refine' ⟨fun h => _, fun h => congr_arg₂ (· * ·) h.1 h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac : a ≤ c
hbd : b ≤ d
h : a * b = c * d
⊢ a = c ∧ b = d
[PROOFSTEP]
rcases hac.eq_or_lt with (rfl | hac)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b d : α
hbd : b ≤ d
hac : a ≤ a
h : a * b = a * d
⊢ a = a ∧ b = d
[PROOFSTEP]
exact ⟨rfl, mul_left_cancel'' h⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac✝ : a ≤ c
hbd : b ≤ d
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d
[PROOFSTEP]
rcases eq_or_lt_of_le hbd with (rfl | hbd)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
hac✝ : a ≤ c
hac : a < c
hbd : b ≤ b
h : a * b = c * b
⊢ a = c ∧ b = b
[PROOFSTEP]
exact ⟨mul_right_cancel'' h, rfl⟩
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝² : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac✝ : a ≤ c
hbd✝ : b ≤ d
h : a * b = c * d
hac : a < c
hbd : b < d
⊢ a = c ∧ b = d
[PROOFSTEP]
exact ((Left.mul_lt_mul hac hbd).ne h).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d
[PROOFSTEP]
refine' ⟨fun h => _, fun h => congr_arg₂ (· * ·) h.1 h.2⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac : a ≤ c
hbd : b ≤ d
h : a * b = c * d
⊢ a = c ∧ b = d
[PROOFSTEP]
rcases hac.eq_or_lt with (rfl | hac)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b d : α
hbd : b ≤ d
hac : a ≤ a
h : a * b = a * d
⊢ a = a ∧ b = d
[PROOFSTEP]
exact ⟨rfl, mul_left_cancel'' h⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac✝ : a ≤ c
hbd : b ≤ d
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d
[PROOFSTEP]
rcases eq_or_lt_of_le hbd with (rfl | hbd)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
hac✝ : a ≤ c
hac : a < c
hbd : b ≤ b
h : a * b = c * b
⊢ a = c ∧ b = b
[PROOFSTEP]
exact ⟨mul_right_cancel'' h, rfl⟩
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : Semigroup α
inst✝⁴ : PartialOrder α
inst✝³ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝² : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
hac✝ : a ≤ c
hbd✝ : b ≤ d
h : a * b = c * d
hac : a < c
hbd : b < d
⊢ a = c ∧ b = d
[PROOFSTEP]
exact ((Right.mul_lt_mul hac hbd).ne h).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : LE α
a b : α
⊢ 1 * a ≤ 1 * b → a ≤ b
[PROOFSTEP]
simpa only [one_mul] using id
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CommSemigroup α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : CommSemigroup α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ a * b = a * c
[PROOFSTEP]
rwa [mul_comm a, mul_comm a]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : CommSemigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
ha : MulLECancellable a
⊢ b * a ≤ c * a ↔ b ≤ c
[PROOFSTEP]
rw [mul_comm b, mul_comm c, ha.mul_le_mul_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : MulLECancellable a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ a * b ≤ a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : CommMonoid α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : MulLECancellable a
⊢ a ≤ b * a ↔ 1 ≤ b
[PROOFSTEP]
rw [mul_comm, ha.le_mul_iff_one_le_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LE α
inst✝¹ : CommMonoid α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
ha : MulLECancellable a
⊢ b * a ≤ a ↔ b ≤ 1
[PROOFSTEP]
rw [mul_comm, ha.mul_le_iff_le_one_right]
