internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_unpair
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ unpair ⟪a, b⟫ = (a, b)
Tactic:
simp [pair]
Proof 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 : M
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)
Tactic:
split_ifs with h
Proof 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 : M
h : a < b
⊢ unpair (b * b + 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 : M
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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 : M
h : a < b
⊢ unpair (b * b + a) = (a, b)
Tactic:
have : √(b * b + a) = b := sqrt_eq_of_le_of_le (by simp) (by simp; exact le_trans (le_of_lt h) (by simp))
Proof 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 : M
h : a < b
this : √(b * b + a) = b
⊢ unpair (b * b + a) = (a, b)
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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 : M
h : a < b
this : √(b * b + a) = b
⊢ unpair (b * b + a) = (a, b)
Tactic:
simp [unpair, this, show ¬b ≤ a from by simpa using h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ b * b ≤ b * b + a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ b * b + a ≤ b * b + 2 * b
Tactic:
simp
Proof 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 : M
h : a < b
⊢ a ≤ 2 * b
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ a ≤ 2 * b
Tactic:
exact le_trans (le_of_lt h) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ b ≤ 2 * b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
this : √(b * b + a) = b
⊢ ¬b ≤ a
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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 : M
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
Tactic:
have : √(a * a + (a + b)) = a :=
  sqrt_eq_of_le_of_le (by simp [add_assoc]) (by simp [add_assoc, two_mul, show b ≤ a from by simpa using h])
Proof 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 b : M
h : ¬a < b
this : √(a * a + (a + b)) = a
⊢ unpair (a * a + a + b) = (a, b)
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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 : M
h : ¬a < b
this : √(a * a + (a + b)) = a
⊢ unpair (a * a + a + b) = (a, b)
Tactic:
simp [unpair, this, add_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ a * a ≤ a * a + (a + b)
Tactic:
simp [add_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ a * a + (a + b) ≤ a * a + 2 * a
Tactic:
simp [add_assoc, two_mul, show b ≤ a from by simpa using h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unpair_pair
Proof 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
⊢ b ≤ a
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₁_pair
Proof 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
⊢ π₁⟪a, b⟫ = a
Tactic:
simp [pi₁]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₂_pair
Proof 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
⊢ π₂⟪a, b⟫ = b
Tactic:
simp [pi₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₁_le_self
Proof 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
Tactic:
simp [pi₁, unpair]
Proof 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 ≤ a
Theorem: LO.FirstOrder.Arith.Model.pi₁_le_self
Proof 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 ≤ a
Tactic:
split_ifs <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₂_le_self
Proof 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
Tactic:
simp [pi₂, unpair]
Proof 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)).2 ≤ a
Theorem: LO.FirstOrder.Arith.Model.pi₂_le_self
Proof 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)).2 ≤ a
Tactic:
split_ifs <;> simp [add_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_pair_left
Proof 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
⊢ a ≤ ⟪a, b⟫
Tactic:
simpa using pi₁_le_self ⟪a, b⟫
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_pair_right
Proof 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
⊢ b ≤ ⟪a, b⟫
Tactic:
simpa using pi₂_le_self ⟪a, b⟫
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_pair_left_of_pos
Proof 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
pos : 0 < a
b : M
⊢ a < ⟪a, b⟫
Tactic:
simp [pair]
Proof 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
pos : 0 < a
b : M
⊢ a < if a < b then b * b + a else a * a + a + b
Theorem: LO.FirstOrder.Arith.Model.lt_pair_left_of_pos
Proof 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
pos : 0 < a
b : M
⊢ a < if a < b then b * b + a else a * a + a + b
Tactic:
split_ifs
Proof 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
pos : 0 < a
b : M
h✝ : a < b
⊢ a < b * b + 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
pos : 0 < a
b : M
h✝ : ¬a < b
⊢ a < a * a + a + b
Theorem: LO.FirstOrder.Arith.Model.lt_pair_left_of_pos
Proof 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
pos : 0 < a
b : M
h✝ : a < b
⊢ a < b * b + a
Tactic:
simp
Proof 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
pos : 0 < a
b : M
h✝ : a < b
⊢ ¬b = 0
Theorem: LO.FirstOrder.Arith.Model.lt_pair_left_of_pos
Proof 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
pos : 0 < a
b : M
h✝ : a < b
⊢ ¬b = 0
Tactic:
exact pos_iff_ne_zero.mp <| pos_of_gt (by assumption)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_pair_left_of_pos
Proof 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
pos : 0 < a
b : M
h✝ : a < b
⊢ ?m.910972 < b
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_pair_left_of_pos
Proof 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
pos : 0 < a
b : M
h✝ : ¬a < b
⊢ a < a * a + a + b
Tactic:
calc
  a < a * a + a     := lt_add_of_pos_left a (by simpa using (pos_iff_ne_zero.mp pos))
  _ ≤ a * a + a + b := by simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_pair_left_of_pos
Proof 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
pos : 0 < a
b : M
h✝ : ¬a < b
⊢ 0 < a * a
Tactic:
simpa using (pos_iff_ne_zero.mp pos)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_pair_left_of_pos
Proof 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
pos : 0 < a
b : M
h✝ : ¬a < b
⊢ a * a + a ≤ a * a + a + b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof 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
⊢ 𝚺₀-Function₁ pi₁ via pi₁Def
Tactic:
intro v
Proof 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
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => π₁ v 0) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val pi₁Def)
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof 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
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => π₁ v 0) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val pi₁Def)
Tactic:
simp [pi₁Def]
Proof 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
v : Fin (Nat.succ 1) → M
⊢ v 0 = π₁ v 1 ↔ ∃ x ≤ v 1, v 1 = ⟪v 0, x⟫
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof 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
v : Fin (Nat.succ 1) → M
⊢ v 0 = π₁ v 1 ↔ ∃ x ≤ v 1, v 1 = ⟪v 0, x⟫
Tactic:
constructor
Proof state after:
case mp
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
⊢ v 0 = π₁ v 1 → ∃ x ≤ v 1, v 1 = ⟪v 0, x⟫

case mpr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
⊢ (∃ x ≤ v 1, v 1 = ⟪v 0, x⟫) → v 0 = π₁ v 1
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof state before:
case mp
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
⊢ v 0 = π₁ v 1 → ∃ x ≤ v 1, v 1 = ⟪v 0, x⟫
Tactic:
intro h
Proof state after:
case mp
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
h : v 0 = π₁ v 1
⊢ ∃ x ≤ v 1, v 1 = ⟪v 0, x⟫
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof state before:
case mp
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
h : v 0 = π₁ v 1
⊢ ∃ x ≤ v 1, v 1 = ⟪v 0, x⟫
Tactic:
exact ⟨π₂ v 1, by simp [←le_iff_lt_succ],  by simp [h]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof 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
v : Fin (Nat.succ 1) → M
h : v 0 = π₁ v 1
⊢ π₂ v 1 ≤ v 1
Tactic:
simp [←le_iff_lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof 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
v : Fin (Nat.succ 1) → M
h : v 0 = π₁ v 1
⊢ v 1 = ⟪v 0, π₂ v 1⟫
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof state before:
case mpr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
⊢ (∃ x ≤ v 1, v 1 = ⟪v 0, x⟫) → v 0 = π₁ v 1
Tactic:
rintro ⟨a, _, e⟩
Proof state after:
case mpr.intro.intro
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
a : M
left✝ : a ≤ v 1
e : v 1 = ⟪v 0, a⟫
⊢ v 0 = π₁ v 1
Theorem: LO.FirstOrder.Arith.Model.pi₁_defined
Proof state before:
case mpr.intro.intro
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
a : M
left✝ : a ≤ v 1
e : v 1 = ⟪v 0, a⟫
⊢ v 0 = π₁ v 1
Tactic:
simp [e]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pi₂_defined
Proof 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
⊢ 𝚺₀-Function₁ pi₂ via pi₂Def
Tactic:
intro v
Proof 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
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => π₂ v 0) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val pi₂Def)
Theorem: LO.FirstOrder.Arith.Model.pi₂_defined
Proof 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
v : Fin (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => π₂ v 0) fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val pi₂Def)
Tactic:
simp [pi₂Def]
Proof 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
v : Fin (Nat.succ 1) → M
⊢ v 0 = π₂ v 1 ↔ ∃ x ≤ v 1, v 1 = ⟪x, v 0⟫
Theorem: LO.FirstOrder.Arith.Model.pi₂_defined
Proof 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
v : Fin (Nat.succ 1) → M
⊢ v 0 = π₂ v 1 ↔ ∃ x ≤ v 1, v 1 = ⟪x, v 0⟫
Tactic:
constructor
Proof state after:
case mp
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
⊢ v 0 = π₂ v 1 → ∃ x ≤ v 1, v 1 = ⟪x, v 0⟫

case mpr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
⊢ (∃ x ≤ v 1, v 1 = ⟪x, v 0⟫) → v 0 = π₂ v 1
Theorem: LO.FirstOrder.Arith.Model.pi₂_defined
Proof state before:
case mp
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
⊢ v 0 = π₂ v 1 → ∃ x ≤ v 1, v 1 = ⟪x, v 0⟫
Tactic:
intro h
Proof state after:
case mp
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 1) → M
h : v 0 = π₂ v 1
⊢ ∃ x ≤ v 1, v 1 = ⟪x, v 0⟫