Theorem: LO.FirstOrder.Arith.Model.div_monotone (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 : M
h : a ≤ b
c : M
⊢ a / c ≤ b / c
Tactic:
rcases zero_le c with (rfl | pos)
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 b : M
h : a ≤ b
⊢ a / 0 ≤ b / 0

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 : M
h : a ≤ b
c : M
pos : 0 < c
⊢ a / c ≤ 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 : M
h : a ≤ b
c : M
pos : 0 < c
⊢ a / c ≤ b / c
Tactic:
by_contra A
State after:
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 : M
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
⊢ False

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 : M
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
⊢ False
Tactic:
have : b / c + 1 ≤ a / c := succ_le_iff_lt.mpr (by simpa using A)
State after:
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 : M
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
this : b / c + 1 ≤ a / c
⊢ False

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 : M
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
this : b / c + 1 ≤ a / c
⊢ False
Tactic:
have : a < a := calc
  a ≤ b               := h
  _ < c * (b / c + 1) := lt_mul_div b pos
  _ ≤ c * (a / c)     := mul_le_mul_left this
  _ ≤ a               := mul_div_le a c
State after:
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 : M
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
this✝ : b / c + 1 ≤ a / c
this : a < a
⊢ False

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 : M
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
this✝ : b / c + 1 ≤ a / c
this : a < a
⊢ False
Tactic:
simp_all
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 b : M
h : a ≤ b
⊢ a / 0 ≤ 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 : M
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
⊢ b / c < a / c
Tactic:
simpa using A
State after:
no goals