[GOAL]
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ExistsMulOfLE α
a b : α
h : a < b
⊢ ∃ c, 1 < c ∧ a * c = b
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_mul_of_le h.le
[GOAL]
case intro
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ExistsMulOfLE α
a c : α
h : a < a * c
⊢ ∃ c_1, 1 < c_1 ∧ a * c_1 = a * c
[PROOFSTEP]
exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩
[GOAL]
α : Type u
inst✝⁵ : LinearOrder α
inst✝⁴ : DenselyOrdered α
inst✝³ : Monoid α
inst✝² : ExistsMulOfLE α
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 : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
x : α
hxb : b < x
⊢ a ≤ x
[PROOFSTEP]
obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le
[GOAL]
case intro
α : Type u
inst✝⁵ : LinearOrder α
inst✝⁴ : DenselyOrdered α
inst✝³ : Monoid α
inst✝² : ExistsMulOfLE α
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 : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε
[PROOFSTEP]
exact h _ ((lt_mul_iff_one_lt_right' b).1 hxb)
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ b * a
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ a * b
[PROOFSTEP]
exact le_self_mul
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ (∃ c, b = a * c) → a ≤ b
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a c✝ d c : α
⊢ a ≤ a * c
[PROOFSTEP]
exact le_self_mul
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ a ≤ b ↔ ∃ c, b = c * a
[PROOFSTEP]
simp only [mul_comm _ a, le_iff_exists_mul]
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
⊢ 1 < a * b ↔ 1 < a ∨ 1 < b
[PROOFSTEP]
simp only [one_lt_iff_ne_one, Ne.def, mul_eq_one_iff, not_and_or]
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a < b
⊢ ∃ c x, a * c = b
[PROOFSTEP]
obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le
[GOAL]
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c✝ d : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ c x, a * c = b
[PROOFSTEP]
refine' ⟨c, one_lt_iff_ne_one.2 _, hc.symm⟩
[GOAL]
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c✝ d : α
h : a < b
c : α
hc : b = a * c
⊢ c ≠ 1
[PROOFSTEP]
rintro rfl
[GOAL]
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a < b
hc : b = a * 1
⊢ False
[PROOFSTEP]
simp [hc, lt_irrefl] at h 
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a ≤ c
⊢ a = 1 * a
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a ≤ b
⊢ a = a * 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ a < b ↔ ∃ c, c > 1 ∧ b = a * c
[PROOFSTEP]
rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]
[GOAL]
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c
[PROOFSTEP]
apply exists_congr
[GOAL]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ ∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1
[PROOFSTEP]
intro c
[GOAL]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c
[PROOFSTEP]
rw [and_comm, and_congr_left_iff, gt_iff_lt]
[GOAL]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ b = a * c → (a ≠ b ↔ 1 < c)
[PROOFSTEP]
rintro rfl
[GOAL]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c ↔ 1 < c
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c → 1 < c
[PROOFSTEP]
rw [one_lt_iff_ne_one]
[GOAL]
case h.mp
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c → c ≠ 1
[PROOFSTEP]
apply mt
[GOAL]
case h.mp.h₁
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ c = 1 → a = a * c
[PROOFSTEP]
rintro rfl
[GOAL]
case h.mp.h₁
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ a = a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
case h.mpr
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ 1 < c → a ≠ a * c
[PROOFSTEP]
rw [← (self_le_mul_right a c).lt_iff_ne]
[GOAL]
case h.mpr
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ 1 < c → a < a * c
[PROOFSTEP]
apply lt_mul_of_one_lt_right'
[GOAL]
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
cases' le_total a b with hb hb
[GOAL]
case inl
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : a ≤ b
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
simp [hb, le_mul_right]
[GOAL]
case inr
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
cases' le_total a c with hc hc
[GOAL]
case inr.inl
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
simp [hc, le_mul_left]
[GOAL]
case inr.inr
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
[PROOFSTEP]
simp [hb, hc]
[GOAL]
α : Type u
inst✝ : CanonicallyLinearOrderedMonoid α
a b c : α
⊢ min (a * b) c = min (min a c * min b c) c
[PROOFSTEP]
simpa [min_comm _ c] using min_mul_distrib c a b
