internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.sqrt_exists_unique
Proof state before:
M✝ : Type u_1
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
lt : x < y
this : a < a
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_exists_unique
Proof 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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] [inst : M ⊧ₘ* 𝐈open] (a x : M),
    x * x ≤ a ∧ a < (x + 1) * (x + 1) → ∀ (y : M), y * y ≤ a ∧ a < (y + 1) * (y + 1) → ¬y = x → x < y → False
lt : ¬x < y
⊢ False
Tactic:
exact this a y hy x hx (Ne.symm ne) (Ne.lt_of_le ne $ by simpa using lt)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_exists_unique
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] [inst : M ⊧ₘ* 𝐈open] (a x : M),
    x * x ≤ a ∧ a < (x + 1) * (x + 1) → ∀ (y : M), y * y ≤ a ∧ a < (y + 1) * (y + 1) → ¬y = x → x < y → False
lt : ¬x < y
⊢ y ≤ x
Tactic:
simpa using lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_exists_unique
Proof state before:
M✝ : Type u_1
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
lt : x < y
⊢ 0 ≤ x + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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₁ fun a => √a via sqrtDef
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 => (fun a => √a) (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val sqrtDef)
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 => (fun a => √a) (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val sqrtDef)
Tactic:
simp[sqrt_graph, sqrtDef, Matrix.vecHead, Matrix.vecTail]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_eq_of_le_of_le
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
x a : M
le : x * x ≤ a
h : a ≤ x * x + 2 * x
⊢ a < (x + 1) * (x + 1)
Tactic:
simp [add_mul_self_eq]
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
x a : M
le : x * x ≤ a
h : a ≤ x * x + 2 * x
⊢ a < x * x + 2 * x + 1
Theorem: LO.FirstOrder.Arith.Model.sqrt_eq_of_le_of_le
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
x a : M
le : x * x ≤ a
h : a ≤ x * x + 2 * x
⊢ a < x * x + 2 * x + 1
Tactic:
exact le_iff_lt_succ.mp h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_sqrt_le
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) ^ 2 ≤ a
Tactic:
simp [sq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_lt_sq
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 + 1) ^ 2
Tactic:
simp [sq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_mul_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 ≤ a * a ∧ a * a < (a + 1) * (a + 1)
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 : M
⊢ a * a < (a + 1) * (a + 1)
Theorem: LO.FirstOrder.Arith.Model.sqrt_mul_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 < (a + 1) * (a + 1)
Tactic:
exact mul_self_lt_mul_self (by simp) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_mul_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
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_mul_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 + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_sq
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 ^ 2 = a
Tactic:
simp [sq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_zero
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
⊢ √0 = 0
Tactic:
simpa using sqrt_mul_self (0 : M)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_one
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
⊢ √1 = 1
Tactic:
simpa using sqrt_mul_self (1 : M)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_two
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
⊢ 1 * 1 ≤ 2 ∧ 2 < (1 + 1) * (1 + 1)
Tactic:
simp [one_le_two, one_add_one_eq_two, one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_three
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
⊢ 1 * 1 ≤ 3 ∧ 3 < (1 + 1) * (1 + 1)
Tactic:
simp [one_add_one_eq_two, two_mul_two_eq_four, ←three_add_one_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_four
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
⊢ √4 = 2
Tactic:
simp [←two_mul_two_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_ne_square
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
⊢ 2 ≠ a ^ 2
Tactic:
intro h
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 : 2 = a ^ 2
⊢ False
Theorem: LO.FirstOrder.Arith.Model.two_ne_square
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 : 2 = a ^ 2
⊢ False
Tactic:
rcases show a = √2 from by rw [h]; simp with rfl
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
h : 2 = (√2) ^ 2
⊢ False
Theorem: LO.FirstOrder.Arith.Model.two_ne_square
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
h : 2 = (√2) ^ 2
⊢ False
Tactic:
simp [sqrt_two] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_ne_square
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 : 2 = a ^ 2
⊢ a = √2
Tactic:
rw [h]
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 : 2 = a ^ 2
⊢ a = √a ^ 2
Theorem: LO.FirstOrder.Arith.Model.two_ne_square
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 : 2 = a ^ 2
⊢ a = √a ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_add
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 * √a + 2 * √a + 1
Tactic:
have := sqrt_spec_lt a
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
this : a < (√a + 1) * (√a + 1)
⊢ a < √a * √a + 2 * √a + 1
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_add
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
this : a < (√a + 1) * (√a + 1)
⊢ a < √a * √a + 2 * √a + 1
Tactic:
rw [add_mul_self_eq] at this
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
this : a < √a * √a + 2 * √a * 1 + 1 * 1
⊢ a < √a * √a + 2 * √a + 1
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_add
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
this : a < √a * √a + 2 * √a * 1 + 1 * 1
⊢ a < √a * √a + 2 * √a + 1
Tactic:
simpa using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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:
by_contra A
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
A : ¬√a ≤ a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 ≤ a
⊢ False
Tactic:
have : a < a := calc
  a ≤ a^2    := le_sq a
  _ < (√a)^2 := by simpa [sq] using mul_self_lt_mul_self (by simp) (by simpa using A)
  _ ≤ a      := sq_sqrt_le a
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
A : ¬√a ≤ a
this : a < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 ≤ a
this : a < a
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 ≤ a
⊢ a ^ 2 < (√a) ^ 2
Tactic:
simpa [sq] using mul_self_lt_mul_self (by simp) (by simpa using A)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 ≤ a
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 ≤ a
⊢ a < √a
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_lt_self_of_one_lt
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 : 1 < a
⊢ √a < a
Tactic:
by_contra A
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 : 1 < a
A : ¬√a < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_lt_self_of_one_lt
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 : 1 < a
A : ¬√a < a
⊢ False
Tactic:
have : a * a ≤ √a * √a := mul_self_le_mul_self (by simp) (by simpa using A)
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 : 1 < a
A : ¬√a < a
this : a * a ≤ √a * √a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_lt_self_of_one_lt
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 : 1 < a
A : ¬√a < a
this : a * a ≤ √a * √a
⊢ False
Tactic:
have : a * a ≤ a := le_trans this (sqrt_spec_le a)
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 : 1 < a
A : ¬√a < a
this✝ : a * a ≤ √a * √a
this : a * a ≤ a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_lt_self_of_one_lt
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 : 1 < a
A : ¬√a < a
this✝ : a * a ≤ √a * √a
this : a * a ≤ a
⊢ False
Tactic:
exact not_lt.mpr this (lt_mul_self h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_lt_self_of_one_lt
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 : 1 < a
A : ¬√a < a
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_lt_self_of_one_lt
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 : 1 < a
A : ¬√a < a
⊢ a ≤ √a
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_of_le_sq
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 ^ 2 → √a ≤ b
Tactic:
intro h
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 ^ 2
⊢ √a ≤ b
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_of_le_sq
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 ^ 2
⊢ √a ≤ b
Tactic:
by_contra A
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 ^ 2
A : ¬√a ≤ b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_of_le_sq
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 ^ 2
A : ¬√a ≤ b
⊢ False
Tactic:
have : a < a := calc
  a ≤ b^2    := h
  _ < (√a)^2 := sq_lt_sq.mpr (by simpa using A)
  _ ≤ a      := by 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 ^ 2
A : ¬√a ≤ b
this : a < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_of_le_sq
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 ^ 2
A : ¬√a ≤ b
this : a < a
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_of_le_sq
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 ^ 2
A : ¬√a ≤ b
⊢ b < √a
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_le_of_le_sq
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 ^ 2
A : ¬√a ≤ b
⊢ (√a) ^ 2 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_lt_of_lt_sqrt
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 ^ 2 < b
Tactic:
intro h
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.sq_lt_of_lt_sqrt
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:
by_contra A
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 : ¬a ^ 2 < b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sq_lt_of_lt_sqrt
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 ^ 2 < b
⊢ False
Tactic:
exact not_le.mpr h (sqrt_le_of_le_sq $ show b ≤ a^2 from by simpa using A)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_lt_of_lt_sqrt
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 ^ 2 < b
⊢ b ≤ a ^ 2
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_graph
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 c : M
⊢ c = ⟪a, b⟫ ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = a * 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 b c : M
⊢ (c = if a < b then b * b + a else a * a + a + b) ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = a * a + a + b
Theorem: LO.FirstOrder.Arith.Model.pair_graph
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 c : M
⊢ (c = if a < b then b * b + a else a * a + a + b) ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = a * a + a + b
Tactic:
by_cases h : a < b
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 c : M
h : a < b
⊢ (c = if a < b then b * b + a else a * a + a + b) ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = 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 c : M
h : ¬a < b
⊢ (c = if a < b then b * b + a else a * a + a + b) ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = a * a + a + b
Theorem: LO.FirstOrder.Arith.Model.pair_graph
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 c : M
h : a < b
⊢ (c = if a < b then b * b + a else a * a + a + b) ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = a * a + a + b
Tactic:
simp [h, show ¬b ≤ a from by simpa using h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_graph
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 c : M
h : a < b
⊢ ¬b ≤ a
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_graph
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 c : M
h : ¬a < b
⊢ (c = if a < b then b * b + a else a * a + a + b) ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = a * a + a + b
Tactic:
simp [h, show b ≤ a from by simpa using h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_graph
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 c : M
h : ¬a < b
⊢ b ≤ a
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_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₂ fun a b => ⟪a, b⟫ via pairDef
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 2) → M
⊢ (fun v => v 0 = (fun v => (fun a b => ⟪a, b⟫) (v 0) (v 1)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val pairDef)
Theorem: LO.FirstOrder.Arith.Model.pair_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 2) → M
⊢ (fun v => v 0 = (fun v => (fun a b => ⟪a, b⟫) (v 0) (v 1)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val pairDef)
Tactic:
simp [pair_graph, pairDef]
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
⊢ ⟪π₁ a, π₂ a⟫ = a
Tactic:
simp [pi₁, 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,
      (if a - √a * √a < √a then (a - √a * √a, √a) else (√a, a - √a * √a - √a)).2⟫ =
    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
⊢ ⟪(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
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
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