internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
hb : a % b + 1 = b
this : b * (a / b + 1) = a + 1
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b
Tactic:
constructor <;> { rw [←this]; simp [pos, hb] }
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
hb : a % b + 1 = b
⊢ b * (a / b + 1) = b * (a / b) + a % b + 1
Tactic:
simp [hb, add_assoc, mul_add]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
hb : a % b + 1 = b
⊢ b * (a / b) + a % b + 1 = a + 1
Tactic:
simp [div_add_mod a b]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inl.h.right
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
hb : a % b + 1 = b
this : b * (a / b + 1) = a + 1
⊢ (a + 1) % b = 0 ∧ a % b + 1 = b
Tactic:
rw [←this]
Proof state after:
case inr.inl.h.right
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
hb : a % b + 1 = b
this : b * (a / b + 1) = a + 1
⊢ b * (a / b + 1) % b = 0 ∧ a % b + 1 = b
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inl.h.right
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
hb : a % b + 1 = b
this : b * (a / b + 1) = a + 1
⊢ b * (a / b + 1) % b = 0 ∧ a % b + 1 = b
Tactic:
simp [pos, hb]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
⊢ (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Tactic:
right
Proof state after:
case inr.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
⊢ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
⊢ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Tactic:
have : b * (a / b) + (a % b + 1) = a + 1 := by simp [←add_assoc, div_add_mod a b]
Proof state after:
case inr.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1
Tactic:
constructor
Proof state after:
case inr.inr.h.left
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ (a + 1) / b = a / b

case inr.inr.h.right
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ (a + 1) % b = a % b + 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
⊢ b * (a / b) + (a % b + 1) = a + 1
Tactic:
simp [←add_assoc, div_add_mod a b]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inr.h.left
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ (a + 1) / b = a / b
Tactic:
rw [←this, mul_comm b, div_mul_add_self (a / b) (a % b + 1) pos]
Proof state after:
case inr.inr.h.left
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ a / b + (a % b + 1) / b = a / b
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inr.h.left
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ a / b + (a % b + 1) / b = a / b
Tactic:
simp [ltb]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inr.h.right
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ (a + 1) % b = a % b + 1
Tactic:
rw [←this, mul_comm b, mod_mul_add _ _ pos]
Proof state after:
case inr.inr.h.right
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ (a % b + 1) % b = a % b + 1
Theorem: LO.FirstOrder.Arith.Model.Nuon.div_mod_succ
Proof state before:
case inr.inr.h.right
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
a b : M
pos : 0 < b
ltb : a % b + 1 < b
this : b * (a / b) + (a % b + 1) = a + 1
⊢ (a % b + 1) % b = a % b + 1
Tactic:
simp [ltb]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have hhk : (k + 1)/‖I‖ ≤ ‖I‖ := by simpa using div_monotone (succ_le_iff_lt.mpr hk) ‖I‖
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have hnk : n ≤ k := H.le
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have Ipos : 0 < I := by simpa using pos_of_gt hk
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
rcases H with ⟨nₘ, hnₘn, HT, HS⟩
Proof state after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖ := by
  have : k / ‖I‖ < ‖I‖ := div_lt_of_lt_mul (by simpa [sq] using hk)
  calc
    ‖nₘ + ‖I‖‖ ≤ ‖‖I‖ * (k / ‖I‖ + 1)‖ := length_monotone <| by simp [mul_add, HT.le_add]
    _        ≤ ‖‖I‖^2‖                 := length_monotone <| by simp[sq]; exact mul_le_mul_left (lt_iff_succ_le.mp this)
    _        ≤ ‖L‖                     := hIL
Proof state after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
rcases div_mod_succ k ‖I‖ with (⟨hdiv, hmodsucc, hmod⟩ | ⟨hdiv, hmod⟩)
Proof state after:
case intro.intro.intro.inl.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)

case intro.intro.intro.inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖
hmod : (k + 1) % ‖I‖ = k % ‖I‖ + 1
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
⊢ (k + 1) / ‖I‖ ≤ ‖I‖
Tactic:
simpa using div_monotone (succ_le_iff_lt.mpr hk) ‖I‖
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
H : SeriesSegment U I L A k n
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
⊢ 0 < I
Tactic:
simpa using pos_of_gt hk
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
⊢ ‖nₘ + ‖I‖‖ ≤ ‖L‖
Tactic:
have : k / ‖I‖ < ‖I‖ := div_lt_of_lt_mul (by simpa [sq] using hk)
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
this : k / ‖I‖ < ‖I‖
⊢ ‖nₘ + ‖I‖‖ ≤ ‖L‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
this : k / ‖I‖ < ‖I‖
⊢ ‖nₘ + ‖I‖‖ ≤ ‖L‖
Tactic:
calc
  ‖nₘ + ‖I‖‖ ≤ ‖‖I‖ * (k / ‖I‖ + 1)‖ := length_monotone <| by simp [mul_add, HT.le_add]
  _        ≤ ‖‖I‖^2‖                 := length_monotone <| by simp[sq]; exact mul_le_mul_left (lt_iff_succ_le.mp this)
  _        ≤ ‖L‖                     := hIL
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
⊢ k < ‖I‖ * ‖I‖
Tactic:
simpa [sq] using hk
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
this : k / ‖I‖ < ‖I‖
⊢ nₘ + ‖I‖ ≤ ‖I‖ * (k / ‖I‖ + 1)
Tactic:
simp [mul_add, HT.le_add]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
this : k / ‖I‖ < ‖I‖
⊢ ‖I‖ * (k / ‖I‖ + 1) ≤ ‖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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
this : k / ‖I‖ < ‖I‖
⊢ ‖I‖ * (k / ‖I‖ + 1) ≤ ‖I‖ * ‖I‖
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
this : k / ‖I‖ < ‖I‖
⊢ ‖I‖ * (k / ‖I‖ + 1) ≤ ‖I‖ * ‖I‖
Tactic:
exact mul_le_mul_left (lt_iff_succ_le.mp this)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case intro.intro.intro.inl.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k) := by
  simpa [div_add_mod, hmod] using HS.succ hU (mod_lt _ $ by simp [Ipos]) hnₘL
Proof state after:
case intro.intro.intro.inl.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
Proof state before:
case intro.intro.intro.inl.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Tactic:
have : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k) := by
  simpa [hdiv] using HT.succ hU hIL this (lt_iff_succ_le.mpr $ by simpa [hdiv] using hhk)
Proof state after:
case intro.intro.intro.inl.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
this✝ : Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
this : Series U I L A ((k + 1) / ‖I‖) (n + fbit A k)
⊢ SeriesSegment U I L A (k + 1) (n + fbit A k)
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
⊢ Segment U L A (‖I‖ * (k / ‖I‖)) ‖I‖ nₘ (n + fbit A k)
Tactic:
simpa [div_add_mod, hmod] using HS.succ hU (mod_lt _ $ by simp [Ipos]) hnₘL
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.succ
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✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos✝ : 0 < I
k n : M
hk : k < ‖I‖ ^ 2
hhk : (k + 1) / ‖I‖ ≤ ‖I‖
hnk : n ≤ k
Ipos : 0 < I
nₘ : M
hnₘn : nₘ ≤ n
HT : Series U I L A (k / ‖I‖) nₘ
HS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₘ n
hnₘL : ‖nₘ + ‖I‖‖ ≤ ‖L‖
hdiv : (k + 1) / ‖I‖ = k / ‖I‖ + 1
hmodsucc : (k + 1) % ‖I‖ = 0
hmod : k % ‖I‖ + 1 = ‖I‖
⊢ 0 < ‖I‖
Tactic:
simp [Ipos]
Proof state after:
no goals