Theorem: LO.FirstOrder.Arith.Model.div_mul (Arithmetization/Basic/IOpen.lean)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
⊢ a / (b * c) = a / b / c
Tactic:
rcases zero_le b with (rfl | hb)
State after:
case inl
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a c : M
⊢ a / (0 * c) = a / 0 / c

case inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
⊢ a / (b * c) = a / b / c

State before:
case inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
⊢ a / (b * c) = a / b / c
Tactic:
rcases zero_le c with (rfl | hc)
State after:
case inr.inl
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
⊢ a / (b * 0) = a / b / 0

case inr.inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ a / (b * c) = a / b / c

State before:
case inr.inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ a / (b * c) = a / b / c
Tactic:
exact div_eq_of
  (by calc
        b * c * (a / b / c) ≤ b * (a / b) := by simp [mul_assoc]; exact mul_le_mul_left (mul_div_le_pos (a / b) hc)
        _                   ≤ a := mul_div_le_pos a hb)
  (by calc
        a < b * (a / b + 1)         := lt_mul_div_succ a hb
        _ ≤ b * c * (a / b / c + 1) := by simp [mul_assoc]; exact mul_le_mul_left (lt_iff_succ_le.mp <| lt_mul_div_succ (a / b) hc))
State after:
no goals

State before:
case inl
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a c : M
⊢ a / (0 * c) = a / 0 / c
Tactic:
simp
State after:
no goals

State before:
case inr.inl
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
⊢ a / (b * 0) = a / b / 0
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ b * c * (a / b / c) ≤ a
Tactic:
calc
  b * c * (a / b / c) ≤ b * (a / b) := by simp [mul_assoc]; exact mul_le_mul_left (mul_div_le_pos (a / b) hc)
  _                   ≤ a := mul_div_le_pos a hb
State after:
no goals

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ b * c * (a / b / c) ≤ b * (a / b)
Tactic:
simp [mul_assoc]
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ b * (c * (a / b / c)) ≤ b * (a / b)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ b * (c * (a / b / c)) ≤ b * (a / b)
Tactic:
exact mul_le_mul_left (mul_div_le_pos (a / b) hc)
State after:
no goals

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ a < b * c * (a / b / c + 1)
Tactic:
calc
  a < b * (a / b + 1)         := lt_mul_div_succ a hb
  _ ≤ b * c * (a / b / c + 1) := by simp [mul_assoc]; exact mul_le_mul_left (lt_iff_succ_le.mp <| lt_mul_div_succ (a / b) hc)
State after:
no goals

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ b * (a / b + 1) ≤ b * c * (a / b / c + 1)
Tactic:
simp [mul_assoc]
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ b * (a / b + 1) ≤ b * (c * (a / b / c + 1))

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b c : M
hb : 0 < b
hc : 0 < c
⊢ b * (a / b + 1) ≤ b * (c * (a / b / c + 1))
Tactic:
exact mul_le_mul_left (lt_iff_succ_le.mp <| lt_mul_div_succ (a / b) hc)
State after:
no goals