Theorem: LO.FirstOrder.Arith.Model.pair_unpair (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 : M
⊢ ⟪π₁ a, π₂ a⟫ = a
Tactic:
simp [pi₁, pi₂, unpair]
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 : M
⊢ ⟪(if a - √a * √a < √a then (a - √a * √a, √a) else (√a, a - √a * √a - √a)).1,
      (if a - √a * √a < √a then (a - √a * √a, √a) else (√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 : M
⊢ ⟪(if a - √a * √a < √a then (a - √a * √a, √a) else (√a, a - √a * √a - √a)).1,
      (if a - √a * √a < √a then (a - √a * √a, √a) else (√a, a - √a * √a - √a)).2⟫ =
    a
Tactic:
split_ifs with 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 : M
h : a - √a * √a < √a
⊢ ⟪(a - √a * √a, √a).1, (a - √a * √a, √a).2⟫ = a

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 : M
h : ¬a - √a * √a < √a
⊢ ⟪(√a, a - √a * √a - √a).1, (√a, a - √a * √a - √a).2⟫ = 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 : M
h : a - √a * √a < √a
⊢ ⟪(a - √a * √a, √a).1, (a - √a * √a, √a).2⟫ = a
Tactic:
simp [pair, 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 : M
h : ¬a - √a * √a < √a
⊢ ⟪(√a, a - √a * √a - √a).1, (√a, a - √a * √a - √a).2⟫ = a
Tactic:
simp
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 : M
h : ¬a - √a * √a < √a
⊢ ⟪√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 : M
h : ¬a - √a * √a < √a
⊢ ⟪√a, a - √a * √a - √a⟫ = a
Tactic:
simp [pair, 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 : M
h : ¬a - √a * √a < √a
⊢ (if √a < a - √a * √a - √a then (a - √a * √a - √a) * (a - √a * √a - √a) + √a else √a * √a + √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 : M
h : ¬a - √a * √a < √a
⊢ (if √a < a - √a * √a - √a then (a - √a * √a - √a) * (a - √a * √a - √a) + √a else √a * √a + √a + (a - √a * √a - √a)) =
    a
Tactic:
have : a - √a * √a - √a ≤ √a := by simp [add_comm (2 * √a), ←two_mul]
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 : M
h : ¬a - √a * √a < √a
this : a - √a * √a - √a ≤ √a
⊢ (if √a < a - √a * √a - √a then (a - √a * √a - √a) * (a - √a * √a - √a) + √a else √a * √a + √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 : M
h : ¬a - √a * √a < √a
this : a - √a * √a - √a ≤ √a
⊢ (if √a < a - √a * √a - √a then (a - √a * √a - √a) * (a - √a * √a - √a) + √a else √a * √a + √a + (a - √a * √a - √a)) =
    a
Tactic:
simp [not_lt.mpr this]
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 : M
h : ¬a - √a * √a < √a
this : a - √a * √a - √a ≤ √a
⊢ √a * √a + √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 : M
h : ¬a - √a * √a < √a
this : a - √a * √a - √a ≤ √a
⊢ √a * √a + √a + (a - √a * √a - √a) = a
Tactic:
have :√a ≤ a - √a * √a := by simpa using 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 : M
h : ¬a - √a * √a < √a
this✝ : a - √a * √a - √a ≤ √a
this : √a ≤ a - √a * √a
⊢ √a * √a + √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 : M
h : ¬a - √a * √a < √a
this✝ : a - √a * √a - √a ≤ √a
this : √a ≤ a - √a * √a
⊢ √a * √a + √a + (a - √a * √a - √a) = a
Tactic:
calc
  √a * √a + √a + (a - √a * √a - √a) = √a * √a + (a - √a * √a) := by simp [add_assoc]
                                                                    rw [add_tsub_self_of_le, add_tsub_self_of_le] <;> simp [this]
  _                                 = a                       := add_tsub_self_of_le (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 : M
h : ¬a - √a * √a < √a
⊢ a - √a * √a - √a ≤ √a
Tactic:
simp [add_comm (2 * √a), ←two_mul]
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 : M
h : ¬a - √a * √a < √a
this : a - √a * √a - √a ≤ √a
⊢ √a ≤ a - √a * √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 : M
h : ¬a - √a * √a < √a
this✝ : a - √a * √a - √a ≤ √a
this : √a ≤ a - √a * √a
⊢ √a * √a + √a + (a - √a * √a - √a) = √a * √a + (a - √a * √a)
Tactic:
simp [add_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 : M
h : ¬a - √a * √a < √a
this✝ : a - √a * √a - √a ≤ √a
this : √a ≤ a - √a * √a
⊢ √a * √a + (√a + (a - √a * √a - √a)) = 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 : M
h : ¬a - √a * √a < √a
this✝ : a - √a * √a - √a ≤ √a
this : √a ≤ a - √a * √a
⊢ √a * √a + (√a + (a - √a * √a - √a)) = a
Tactic:
rw [add_tsub_self_of_le, add_tsub_self_of_le] <;> simp [this]
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 : M
h : ¬a - √a * √a < √a
this✝ : a - √a * √a - √a ≤ √a
this : √a ≤ a - √a * √a
⊢ √a * √a ≤ a
Tactic:
simp
State after:
no goals