Theorem: LO.FirstOrder.Arith.Model.pair_lt_pair_right (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₁ b₂ : M
h : b₁ < b₂
⊢ ⟪a, b₁⟫ < ⟪a, b₂⟫
Tactic:
by_cases h₁ : a < b₁ <;> simp [pair, h₁]
State after:
case pos
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₁ b₂ : M
h : b₁ < b₂
h₁ : a < b₁
⊢ b₁ * b₁ + a < if a < b₂ then b₂ * b₂ + a else a * a + a + b₂

case neg
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + a + b₁ < if a < b₂ then b₂ * b₂ + a else a * a + a + b₂

State before:
case pos
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₁ b₂ : M
h : b₁ < b₂
h₁ : a < b₁
⊢ b₁ * b₁ + a < if a < b₂ then b₂ * b₂ + a else a * a + a + b₂
Tactic:
simpa [lt_trans _ _ _ h₁ h, ←sq] using h
State after:
no goals

State before:
case neg
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + a + b₁ < if a < b₂ then b₂ * b₂ + a else a * a + a + b₂
Tactic:
by_cases h₂ : a < b₂ <;> simp [h₂, h]
State after:
case pos
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a + b₁ < b₂ * b₂ + a

State before:
case pos
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a + b₁ < b₂ * b₂ + a
Tactic:
calc
  a * a + a + b₁ < (a + 1) * (a + 1) + b₁ := by simp [add_mul_self_eq]; apply lt_succ_iff_le.mpr; simp
  _              ≤ b₂ * b₂ + b₁           := by simpa [←sq, succ_le_iff_lt] using h₂
  _              ≤ b₂ * b₂ + a            := by simpa using h₁
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a + b₁ < (a + 1) * (a + 1) + b₁
Tactic:
simp [add_mul_self_eq]
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a < a * a + 2 * a + 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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a < a * a + 2 * a + 1
Tactic:
apply lt_succ_iff_le.mpr
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a ≤ a * a + 2 * a

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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a ≤ a * a + 2 * a
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ (a + 1) * (a + 1) + b₁ ≤ b₂ * b₂ + b₁
Tactic:
simpa [←sq, succ_le_iff_lt] using h₂
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ b₂ * b₂ + b₁ ≤ b₂ * b₂ + a
Tactic:
simpa using h₁
State after:
no goals