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

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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + a₂ + b
Tactic:
calc
  b * b + a₁ < b * b + b        := by simpa using h₁
  _          ≤ a₂ * a₂ + a₂     := add_le_add (mul_le_mul (by simpa using h₂) (by simpa using h₂) (by simp) (by simp)) (by simpa using h₂)
  _          ≤ a₂ * a₂ + a₂ + b := by 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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < b * b + b
Tactic:
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b ≤ a₂
Tactic:
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ 0 ≤ b
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ 0 ≤ 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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ a₂ * a₂ + a₂ ≤ a₂ * a₂ + a₂ + b
Tactic:
simp
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + a₁ + b < if a₂ < b then b * b + a₂ else a₂ * a₂ + a₂ + b
Tactic:
simp[show ¬a₂ < b from by simp; exact le_trans (by simpa using h₁) (le_of_lt h)]
State after:
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + a₁ < a₂ * a₂ + a₂

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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + a₁ < a₂ * a₂ + a₂
Tactic:
apply _root_.add_lt_add (by simpa [←sq] using h) 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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ ¬a₂ < b
Tactic:
simp
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ b ≤ 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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ b ≤ a₂
Tactic:
exact le_trans (by simpa using h₁) (le_of_lt 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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ b ≤ a₁
Tactic:
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ a₁ * a₁ < a₂ * a₂
Tactic:
simpa [←sq] using h
State after:
no goals