internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
lt✝¹ : a < 3
lt✝ : a < 2
lt : a < 1
⊢ a = 0
Tactic:
simpa using lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_three_iff_eq_zero_or_one_or_two_or_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3 → a ≤ 3
Tactic:
rintro (rfl | rfl | rfl | rfl) <;> simp [one_le_two, ←two_add_one_eq_three]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_two_eq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 2 * 2 = 4
Tactic:
rw [←one_add_one_eq_two, mul_add, add_mul, mul_one, ←add_assoc,
  one_add_one_eq_two, two_add_one_eq_three, three_add_one_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_pow_two_eq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 2 ^ 2 = 4
Tactic:
simp [sq, two_mul_two_eq_four]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 0 < 2
Tactic:
exact _root_.two_pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ a ≤ a * a
Tactic:
have : 0 ≤ a := by exact zero_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
this : 0 ≤ a
⊢ a ≤ a * a
Theorem: LO.FirstOrder.Arith.Model.le_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
this : 0 ≤ a
⊢ a ≤ a * a
Tactic:
rcases this with (rfl | pos) <;> simp [*, ←pos_iff_one_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ 0 ≤ a
Tactic:
exact zero_le a
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ a ≤ a ^ 2
Tactic:
simp [sq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a ^ 2 ≤ b ^ 2 ↔ a ≤ b
Tactic:
simp [sq]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a * a ≤ b * b ↔ a ≤ b
Theorem: LO.FirstOrder.Arith.Model.sq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a * a ≤ b * b ↔ a ≤ b
Tactic:
symm
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a ≤ b ↔ a * a ≤ b * b
Theorem: LO.FirstOrder.Arith.Model.sq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a ≤ b ↔ a * a ≤ b * b
Tactic:
apply mul_self_le_mul_self_iff <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a ^ 2 < b ^ 2 ↔ a < b
Tactic:
simp [sq]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a * a < b * b ↔ a < b
Theorem: LO.FirstOrder.Arith.Model.sq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a * a < b * b ↔ a < b
Tactic:
symm
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a < b ↔ a * a < b * b
Theorem: LO.FirstOrder.Arith.Model.sq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a < b ↔ a * a < b * b
Tactic:
apply mul_self_lt_mul_self_iff <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_mul_of_pos_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : 0 < b
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_mul_of_pos_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : 0 < b
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_two_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 0 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_le_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ c
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_le_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ c
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_of_mul_lt_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : a * b < a * c
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_of_mul_lt_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b * a < c * a
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow_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 ⊧ₘ* 𝐏𝐀⁻
a b c x : M
⊢ x ^ 3 = x * x * x
Tactic:
rw [← two_add_one_eq_three, pow_add, sq]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c x : M
⊢ x * x * x ^ 1 = x * x * x
Theorem: LO.FirstOrder.Arith.Model.pow_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 ⊧ₘ* 𝐏𝐀⁻
a b c x : M
⊢ x * x * x ^ 1 = x * x * x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow_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 ⊧ₘ* 𝐏𝐀⁻
a b c x : M
⊢ x ^ 4 = x * x * x * x
Tactic:
rw [← three_add_one_eq_four, pow_add, pow_three]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c x : M
⊢ x * x * x * x ^ 1 = x * x * x * x
Theorem: LO.FirstOrder.Arith.Model.pow_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 ⊧ₘ* 𝐏𝐀⁻
a b c x : M
⊢ x * x * x * x ^ 1 = x * x * x * x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow_four_eq_sq_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 ⊧ₘ* 𝐏𝐀⁻
a b c x : M
⊢ x ^ 4 = (x ^ 2) ^ 2
Tactic:
simp [pow_four, sq, mul_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.one_lt_mul_self_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
h : ¬1 < a
⊢ ¬1 < a * a
Tactic:
push_neg at 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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
h : a ≤ 1
⊢ a * a ≤ 1
Theorem: LO.FirstOrder.Arith.Model.one_lt_mul_self_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
h : a ≤ 1
⊢ a * a ≤ 1
Tactic:
exact mul_le_one' h h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.opos_lt_sq_pos_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ 0 < a ^ 2 ↔ 0 < a
Tactic:
simp [sq, pos_iff_ne_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.one_lt_sq_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ 1 < a ^ 2 ↔ 1 < a
Tactic:
simp [sq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_self_eq_one_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ ¬a * a = 1 ↔ ¬a = 1
Tactic:
simp [ne_iff_lt_or_gt]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sq_eq_one_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ a ^ 2 = 1 ↔ a = 1
Tactic:
simp [sq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c i : M
h : 2 ≤ i
⊢ 2 * i ≤ i ^ 2
Tactic:
simp [sq]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c i : M
h : 2 ≤ i
⊢ 2 * i ≤ i * i
Theorem: LO.FirstOrder.Arith.Model.two_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c i : M
h : 2 ≤ i
⊢ 2 * i ≤ i * i
Tactic:
exact mul_le_mul_right h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_le_sq_add_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 ⊧ₘ* 𝐏𝐀⁻
a b c i : M
⊢ 2 * i ≤ i ^ 2 + 1
Tactic:
rcases zero_le i with (rfl | pos)
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 2 * 0 ≤ 0 ^ 2 + 1

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c i : M
pos : 0 < i
⊢ 2 * i ≤ i ^ 2 + 1
Theorem: LO.FirstOrder.Arith.Model.two_mul_le_sq_add_one
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 2 * 0 ≤ 0 ^ 2 + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_le_sq_add_one
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 ⊧ₘ* 𝐏𝐀⁻
a b c i : M
pos : 0 < i
⊢ 2 * i ≤ i ^ 2 + 1
Tactic:
rcases pos_iff_one_le.mp pos with (rfl | lt)
Proof state after:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
pos : 0 < 1
⊢ 2 * 1 ≤ 1 ^ 2 + 1

case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c i : M
pos : 0 < i
lt : 1 < i
⊢ 2 * i ≤ i ^ 2 + 1
Theorem: LO.FirstOrder.Arith.Model.two_mul_le_sq_add_one
Proof state before:
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
pos : 0 < 1
⊢ 2 * 1 ≤ 1 ^ 2 + 1
Tactic:
simp [one_add_one_eq_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_le_sq_add_one
Proof state before:
case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c i : M
pos : 0 < i
lt : 1 < i
⊢ 2 * i ≤ i ^ 2 + 1
Tactic:
exact le_trans (two_mul_le_sq (one_lt_iff_two_le.mp lt)) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_le_sq_add_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 ⊧ₘ* 𝐏𝐀⁻
a b c i : M
pos : 0 < i
lt : 1 < i
⊢ i ^ 2 ≤ i ^ 2 + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c i : M
h : 2 < i
⊢ 2 * i < i ^ 2
Tactic:
simp [sq]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c i : M
h : 2 < i
⊢ 2 * i < i * i
Theorem: LO.FirstOrder.Arith.Model.two_mul_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 ⊧ₘ* 𝐏𝐀⁻
a b c i : M
h : 2 < i
⊢ 2 * i < i * i
Tactic:
exact (mul_lt_mul_right (show 0 < i from pos_of_gt h)).mpr h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.succ_le_double_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
h : 0 < a
⊢ a + 1 ≤ 2 * a
Tactic:
simpa [two_mul] using pos_iff_one_le.mp h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_add_one_lt_two_mul_of_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : a < b
⊢ 2 * a + 1 < 2 * (a + 1)
Tactic:
simp [mul_add, one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_add_one_lt_two_mul_of_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : a < b
⊢ 2 * (a + 1) ≤ 2 * b
Tactic:
simp [←lt_iff_succ_le, h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_add_add_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c✝ a b c : M
⊢ a ≤ a + b + c
Tactic:
simp [add_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_add_add_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c✝ a b c : M
⊢ b ≤ a + b + c
Tactic:
simp [add_right_comm a b c]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_le_cancel
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ AddLECancellable a
Tactic:
intro b c
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c✝ a b c : M
⊢ a + b ≤ a + c → b ≤ c
Theorem: LO.FirstOrder.Arith.Model.add_le_cancel
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c✝ a b c : M
⊢ a + b ≤ a + c → b ≤ c
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.val_npow
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c : M
k : ℕ
a : M
⊢ (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
Tactic:
induction k <;> simp [Operator.npow_zero, Operator.npow_succ, Operator.val_comp, Matrix.empty_eq, Matrix.comp_vecCons']
Proof state after:
case succ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝¹ b c a : M
n✝ : ℕ
a✝ : (Operator.npow ℒₒᵣ n✝).val ![a] = a ^ n✝
⊢ (op(*).val fun i => (![Operator.npow ℒₒᵣ n✝, Operator.bvar 0] i).val ![a]) = a ^ (n✝ + 1)
Theorem: LO.FirstOrder.Arith.Model.val_npow
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
k : ℕ
IH : (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
⊢ (op(*).val fun i => (![Operator.npow ℒₒᵣ k, Operator.bvar 0] i).val ![a]) = a ^ (k + 1)
Tactic:
case succ k IH =>
  rw [Matrix.fun_eq_vec₂ (v := fun i => Operator.val ((Operator.npow ℒₒᵣ k :> ![Operator.bvar 0]) i) ![a]), pow_succ]
  simp [npowRec, mul_comm a, IH]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.val_npow
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
k : ℕ
IH : (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
⊢ (op(*).val fun i => (![Operator.npow ℒₒᵣ k, Operator.bvar 0] i).val ![a]) = a ^ (k + 1)
Tactic:
rw [Matrix.fun_eq_vec₂ (v := fun i => Operator.val ((Operator.npow ℒₒᵣ k :> ![Operator.bvar 0]) i) ![a]), pow_succ]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
k : ℕ
IH : (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
⊢ op(*).val
      ![(![Operator.npow ℒₒᵣ k, Operator.bvar 0] 0).val ![a], (![Operator.npow ℒₒᵣ k, Operator.bvar 0] 1).val ![a]] =
    a ^ k * a
Theorem: LO.FirstOrder.Arith.Model.val_npow
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
k : ℕ
IH : (Operator.npow ℒₒᵣ k).val ![a] = a ^ k
⊢ op(*).val
      ![(![Operator.npow ℒₒᵣ k, Operator.bvar 0] 0).val ![a], (![Operator.npow ℒₒᵣ k, Operator.bvar 0] 1).val ![a]] =
    a ^ k * a
Tactic:
simp [npowRec, mul_comm a, IH]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eval_ballLTSucc
Proof state before:
M : Type u_1
inst✝¹⁴ : Zero M
inst✝¹³ : One M
inst✝¹² : Add M
inst✝¹¹ : Mul M
inst✝¹⁰ : LT M
inst✝⁹ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
L : Language
inst✝⁸ : L.LT
inst✝⁷ : L.Zero
inst✝⁶ : L.One
inst✝⁵ : L.Add
inst✝⁴ : Structure L M
inst✝³ : Structure.LT L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
ξ : Type u_2
n : ℕ
e : Fin n → M
ε : ξ → M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
⊢ (Semiformula.Evalm M e ε) (Semiformula.ballLTSucc t p) ↔ ∀ x ≤ valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
Tactic:
simp [Semiformula.eval_ballLTSucc, lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eval_bexLTSucc
Proof state before:
M : Type u_1
inst✝¹⁴ : Zero M
inst✝¹³ : One M
inst✝¹² : Add M
inst✝¹¹ : Mul M
inst✝¹⁰ : LT M
inst✝⁹ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
L : Language
inst✝⁸ : L.LT
inst✝⁷ : L.Zero
inst✝⁶ : L.One
inst✝⁵ : L.Add
inst✝⁴ : Structure L M
inst✝³ : Structure.LT L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
ξ : Type u_2
n : ℕ
e : Fin n → M
ε : ξ → M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
⊢ (Semiformula.Evalm M e ε) (Semiformula.bexLTSucc t p) ↔ ∃ x ≤ valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
Tactic:
simp [Semiformula.eval_bexLTSucc, lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Theory.mem_indScheme_of_mem
Proof state before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
p : Semiformula L ℕ 1
hp : C p
⊢ ∀ᶠ* succInd p ∈ indScheme L C
Tactic:
simp [indScheme]
Proof state after:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
p : Semiformula L ℕ 1
hp : C p
⊢ ∃ p_1, C p_1 ∧ ∀ᶠ* succInd p = ∀ᶠ* succInd p_1
Theorem: LO.FirstOrder.Arith.Theory.mem_indScheme_of_mem
Proof state before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
p : Semiformula L ℕ 1
hp : C p
⊢ ∃ p_1, C p_1 ∧ ∀ᶠ* succInd p = ∀ᶠ* succInd p_1
Tactic:
exact ⟨p, hp, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Theory.mem_iOpen_of_qfree
Proof state before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
p : Semiformula L ℕ 1
hp : p.Open
⊢ ∀ᶠ* succInd p ∈ indScheme L Semiformula.Open
Tactic:
exact ⟨p, hp, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Theory.indScheme_subset
Proof state before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
⊢ indScheme L C ⊆ indScheme L C'
Tactic:
intro _
Proof state after:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
a✝ : Sentence L
⊢ a✝ ∈ indScheme L C → a✝ ∈ indScheme L C'
Theorem: LO.FirstOrder.Arith.Theory.indScheme_subset
Proof state before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
a✝ : Sentence L
⊢ a✝ ∈ indScheme L C → a✝ ∈ indScheme L C'
Tactic:
simp [indScheme]
Proof state after:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
a✝ : Sentence L
⊢ ∀ (x : Semiformula L ℕ 1), C x → a✝ = ∀ᶠ* succInd x → ∃ p, C' p ∧ a✝ = ∀ᶠ* succInd p
Theorem: LO.FirstOrder.Arith.Theory.indScheme_subset
Proof state before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
a✝ : Sentence L
⊢ ∀ (x : Semiformula L ℕ 1), C x → a✝ = ∀ᶠ* succInd x → ∃ p, C' p ∧ a✝ = ∀ᶠ* succInd p
Tactic:
rintro p hp rfl
Proof state after:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
p : Semiformula L ℕ 1
hp : C p
⊢ ∃ p_1, C' p_1 ∧ ∀ᶠ* succInd p = ∀ᶠ* succInd p_1
Theorem: LO.FirstOrder.Arith.Theory.indScheme_subset
Proof state before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
p : Semiformula L ℕ 1
hp : C p
⊢ ∃ p_1, C' p_1 ∧ ∀ᶠ* succInd p = ∀ᶠ* succInd p_1
Tactic:
exact ⟨p, h hp, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.induction_eval
Proof state before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
p : Semiformula L ℕ 1
hp : C p
v : ℕ → M
⊢ (Semiformula.Evalm M ![0] v) p →
    (∀ (x : M), (Semiformula.Evalm M ![x] v) p → (Semiformula.Evalm M ![x + 1] v) p) →
      ∀ (x : M), (Semiformula.Evalm M ![x] v) p
Tactic:
have : M ⊧ₘ (∀ᶠ* succInd p) :=
  ModelsTheory.models (T := Theory.indScheme _ C) M (by simpa using Theory.mem_indScheme_of_mem hp)
Proof state after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
p : Semiformula L ℕ 1
hp : C p
v : ℕ → M
this : M ⊧ₘ ∀ᶠ* succInd p
⊢ (Semiformula.Evalm M ![0] v) p →
    (∀ (x : M), (Semiformula.Evalm M ![x] v) p → (Semiformula.Evalm M ![x + 1] v) p) →
      ∀ (x : M), (Semiformula.Evalm M ![x] v) p