internlm/Lean-Github huggingface dataset:
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 = ⟪x, v 0⟫
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 1, v 0⟫
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 = ⟪x, v 0⟫) → 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 = ⟪a, v 0⟫
⊢ 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 = ⟪a, v 0⟫
⊢ v 0 = π₂ v 1
Tactic:
simp [e]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
⊢ ⟪a₁, b⟫ < ⟪a₂, b⟫
Tactic:
by_cases h₁ : a₁ < b <;> simp [pair, 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₁ 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
Theorem: LO.FirstOrder.Arith.Model.pair_lt_pair_left
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₁ 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]
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + a₂ + b
Theorem: LO.FirstOrder.Arith.Model.pair_lt_pair_left
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₁ 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < b * b + b
Tactic:
simpa using h₁
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b ≤ a₂
Tactic:
simpa using h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ 0 ≤ b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ 0 ≤ a₂
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ a₂ * a₂ + a₂ ≤ a₂ * a₂ + a₂ + b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_pair_left
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₁ 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)]
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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + a₁ < a₂ * a₂ + a₂
Theorem: LO.FirstOrder.Arith.Model.pair_lt_pair_left
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₁ 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ ¬a₂ < 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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ b ≤ a₂
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ b ≤ a₂
Tactic:
exact le_trans (by simpa using h₁) (le_of_lt h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ b ≤ a₁
Tactic:
simpa using h₁
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ a₂ : M
h : a₁ < a₂
b : M
h₁ : ¬a₁ < b
⊢ a₁ * a₁ < a₂ * a₂
Tactic:
simpa [←sq] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_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₁ a₂ : M
h : a₁ ≤ a₂
b : M
⊢ ⟪a₁, b⟫ ≤ ⟪a₂, b⟫
Tactic:
rcases h with (rfl | lt)
Proof state after:
case inl
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₁, b⟫

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₁ a₂ b : M
lt : a₁ < a₂
⊢ ⟪a₁, b⟫ ≤ ⟪a₂, b⟫
Theorem: LO.FirstOrder.Arith.Model.pair_le_pair_left
Proof state before:
case inl
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₁, b⟫
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_le_pair_left
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₁ a₂ b : M
lt : a₁ < a₂
⊢ ⟪a₁, b⟫ ≤ ⟪a₂, b⟫
Tactic:
exact le_of_lt (pair_lt_pair_left lt b)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ b₂ : M
h : b₁ < b₂
⊢ ⟪a, b₁⟫ < ⟪a, b₂⟫
Tactic:
by_cases h₁ : a < b₁ <;> simp [pair, 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₁ 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₂
Theorem: LO.FirstOrder.Arith.Model.pair_lt_pair_right
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₁ 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_pair_right
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₁ 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]
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a + b₁ < b₂ * b₂ + a
Theorem: LO.FirstOrder.Arith.Model.pair_lt_pair_right
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₁ 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₁
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ 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]
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a < a * a + 2 * a + 1
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ 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
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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a ≤ a * a + 2 * a
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + a ≤ a * a + 2 * a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ 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₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_lt_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₁ b₂ : M
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ b₂ * b₂ + b₁ ≤ b₂ * b₂ + a
Tactic:
simpa using h₁
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_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₁ b₂ : M
h : b₁ ≤ b₂
⊢ ⟪a, b₁⟫ ≤ ⟪a, b₂⟫
Tactic:
rcases h with (rfl | lt)
Proof state after:
case inl
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, b₁⟫

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 b₁ b₂ : M
lt : b₁ < b₂
⊢ ⟪a, b₁⟫ ≤ ⟪a, b₂⟫
Theorem: LO.FirstOrder.Arith.Model.pair_le_pair_right
Proof state before:
case inl
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, b₁⟫
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_le_pair_right
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 b₁ b₂ : M
lt : b₁ < b₂
⊢ ⟪a, b₁⟫ ≤ ⟪a, b₂⟫
Tactic:
exact le_of_lt (pair_lt_pair_right a lt)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_polybound
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 + b + 1) ^ 2
Tactic:
by_cases h : a < b <;> simp [pair, h, sq, add_mul_self_eq, two_mul]
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
⊢ b * b + a ≤ a * a + (a + a) * b + b * b + (a + b + (a + b)) + 1

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
⊢ a * a + a + b ≤ a * a + (a + a) * b + b * b + (a + b + (a + b)) + 1
Theorem: LO.FirstOrder.Arith.Model.pair_polybound
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
⊢ b * b + a ≤ a * a + (a + a) * b + b * b + (a + b + (a + b)) + 1
Tactic:
simp [←add_assoc, add_right_comm _ a]
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
⊢ b * b ≤ a * a + (a + a) * b + b * b + b + b + 1 + a
Theorem: LO.FirstOrder.Arith.Model.pair_polybound
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
⊢ b * b ≤ a * a + (a + a) * b + b * b + b + b + 1 + a
Tactic:
simp [add_right_comm _ (b * b)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_polybound
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
⊢ a * a + a + b ≤ a * a + (a + a) * b + b * b + (a + b + (a + b)) + 1
Tactic:
simp [←add_assoc, add_right_comm _ b]
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
⊢ a * a + a ≤ a * a + (a + a) * b + b * b + a + a + 1 + b
Theorem: LO.FirstOrder.Arith.Model.pair_polybound
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
⊢ a * a + a ≤ a * a + (a + a) * b + b * b + a + a + 1 + b
Tactic:
simp [add_right_comm _ a]
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
⊢ a * a ≤ a * a + (a + a) * b + b * b + 1 + b + a
Theorem: LO.FirstOrder.Arith.Model.pair_polybound
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
⊢ a * a ≤ a * a + (a + a) * b + b * b + 1 + b + a
Tactic:
simp [add_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_ext_iff
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₁ a₂ b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ → ⟪a₁, b₁⟫ = ⟪a₂, b₂⟫
Tactic:
rintro ⟨rfl, rfl⟩
Proof state after:
case 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
a₁ b₁ : M
⊢ ⟪a₁, b₁⟫ = ⟪a₁, b₁⟫
Theorem: LO.FirstOrder.Arith.Model.pair_ext_iff
Proof state before:
case 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
a₁ b₁ : M
⊢ ⟪a₁, b₁⟫ = ⟪a₁, b₁⟫
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
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
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ ∀ (x : M), P x
Tactic:
intro x
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
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ P x
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
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
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ Structure.ORing L M
Tactic:
case inst => exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
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
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
Tactic:
case inst => exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
case Γ
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ Polarity
Tactic:
exact Γ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
case 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
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ ℕ
Tactic:
exact m
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
case hP
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ DefinablePred ?m.1056264 (Γ.coe, m) fun x => P x
Tactic:
exact hP
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
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
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ Structure.ORing L M
Tactic:
exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
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
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
Tactic:
exact inferInstance
Proof state after:
no goals