internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
⊢ l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
Tactic:
induction l using induction_iSigmaZero
Proof state after:
case hP
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 iter T : M
H : IsSeries U I L A iter T
⊢ 𝚺₀-Predicate fun l => l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l

case zero
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 iter T : M
H : IsSeries U I L A iter T
⊢ 0 ≤ iter → T{L}[0] ≤ T{L}[0] + ‖I‖ * 0

case succ
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 iter T : M
H : IsSeries U I L A iter T
x✝ : M
a✝ : x✝ ≤ iter → T{L}[x✝] ≤ T{L}[0] + ‖I‖ * x✝
⊢ x✝ + 1 ≤ iter → T{L}[x✝ + 1] ≤ T{L}[0] + ‖I‖ * (x✝ + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ 0 ≤ iter → T{L}[0] ≤ T{L}[0] + ‖I‖ * 0
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ l + 1 ≤ iter → T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
case succ l IH =>
  intro h
  have IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l := IH (le_trans (by simp) h)
  calc
    T{L}[l + 1] ≤ T{L}[l] + ‖I‖           := (H l (succ_le_iff_lt.mp h)).le_add
    _           ≤ T{L}[0] + ‖I‖ * (l + 1) := by simpa [mul_add, ←add_assoc] using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.le_add
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ 𝚺₀-Predicate fun l => l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ 0 ≤ iter → T{L}[0] ≤ T{L}[0] + ‖I‖ * 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ l + 1 ≤ iter → T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
⊢ T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
⊢ T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
have IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l := IH (le_trans (by simp) 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH✝ : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH✝ : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
calc
  T{L}[l + 1] ≤ T{L}[l] + ‖I‖           := (H l (succ_le_iff_lt.mp h)).le_add
  _           ≤ T{L}[0] + ‖I‖ * (l + 1) := by simpa [mul_add, ←add_assoc] using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
⊢ l ≤ l + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH✝ : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ T{L}[l] + ‖I‖ ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
simpa [mul_add, ←add_assoc] using IH
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter n : M
H : Series U I L A iter n
⊢ n ≤ ‖I‖ * iter
Tactic:
rcases H with ⟨T, _, hT, hzero, rfl⟩
Proof state after:
case intro.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 iter T : M
left✝ : T < U
hT : IsSeries U I L A iter T
hzero : T{L}[0] = 0
⊢ T{L}[iter] ≤ ‖I‖ * iter
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.le_add
Proof state before:
case intro.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 iter T : M
left✝ : T < U
hT : IsSeries U I L A iter T
hzero : T{L}[0] = 0
⊢ T{L}[iter] ≤ ‖I‖ * iter
Tactic:
simpa [hzero] using hT.le_add iter (by rfl)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
left✝ : T < U
hT : IsSeries U I L A iter T
hzero : T{L}[0] = 0
⊢ iter ≤ iter
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter n₁ n₂ : M
H₁ : Series U I L A iter n₁
H₂ : Series U I L A iter n₂
⊢ n₁ = n₂
Tactic:
rcases H₁ with ⟨T₁, _, HT₁, Hₛ₁, rfl⟩
Proof state after:
case intro.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 iter n₂ : M
H₂ : Series U I L A iter n₂
T₁ : M
left✝ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
⊢ T₁{L}[iter] = n₂
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
Proof state before:
case intro.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 iter n₂ : M
H₂ : Series U I L A iter n₂
T₁ : M
left✝ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
⊢ T₁{L}[iter] = n₂
Tactic:
rcases H₂ with ⟨T₂, _, HT₂, Hₛ₂, rfl⟩
Proof state after:
case intro.intro.intro.intro.intro.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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ T₁{L}[iter] = T₂{L}[iter]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
Proof state before:
case intro.intro.intro.intro.intro.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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ T₁{L}[iter] = T₂{L}[iter]
Tactic:
suffices ∀ i ≤ iter, T₁{L}[i] = T₂{L}[i] from this iter (by rfl)
Proof state after:
case intro.intro.intro.intro.intro.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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ ∀ i ≤ iter, T₁{L}[i] = T₂{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
Proof state before:
case intro.intro.intro.intro.intro.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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ ∀ i ≤ iter, T₁{L}[i] = T₂{L}[i]
Tactic:
intro i
Proof state after:
case intro.intro.intro.intro.intro.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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
⊢ i ≤ iter → T₁{L}[i] = T₂{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
Proof state before:
case intro.intro.intro.intro.intro.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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
⊢ i ≤ iter → T₁{L}[i] = T₂{L}[i]
Tactic:
induction i using induction_iSigmaZero
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.hP
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ 𝚺₀-Predicate fun i => i ≤ iter → T₁{L}[i] = T₂{L}[i]

case intro.intro.intro.intro.intro.intro.intro.intro.zero
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ 0 ≤ iter → T₁{L}[0] = T₂{L}[0]

case intro.intro.intro.intro.intro.intro.intro.intro.succ
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
x✝ : M
a✝ : x✝ ≤ iter → T₁{L}[x✝] = T₂{L}[x✝]
⊢ x✝ + 1 ≤ iter → T₁{L}[x✝ + 1] = T₂{L}[x✝ + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ 0 ≤ iter → T₁{L}[0] = T₂{L}[0]
Tactic:
case zero => intro _; simp [Hₛ₁, Hₛ₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH : i ≤ iter → T₁{L}[i] = T₂{L}[i]
⊢ i + 1 ≤ iter → T₁{L}[i + 1] = T₂{L}[i + 1]
Tactic:
case succ i IH =>
  intro hi
  have IH : T₁{L}[i] = T₂{L}[i] := IH (le_trans (by simp) hi)
  have h₁ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₁{L}[i + 1]) := HT₁ i (lt_iff_succ_le.mpr hi)
  have h₂ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₂{L}[i + 1]) := by simpa [IH] using HT₂ i (lt_iff_succ_le.mpr hi)
  exact h₁.uniq h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
this : ∀ i ≤ iter, T₁{L}[i] = T₂{L}[i]
⊢ iter ≤ iter
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.hP
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ 𝚺₀-Predicate fun i => i ≤ iter → T₁{L}[i] = T₂{L}[i]
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
⊢ 0 ≤ iter → T₁{L}[0] = T₂{L}[0]
Tactic:
intro _
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
a✝ : 0 ≤ iter
⊢ T₁{L}[0] = T₂{L}[0]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
a✝ : 0 ≤ iter
⊢ T₁{L}[0] = T₂{L}[0]
Tactic:
simp [Hₛ₁, Hₛ₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH : i ≤ iter → T₁{L}[i] = T₂{L}[i]
⊢ i + 1 ≤ iter → T₁{L}[i + 1] = T₂{L}[i + 1]
Tactic:
intro hi
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
⊢ T₁{L}[i + 1] = T₂{L}[i + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
⊢ T₁{L}[i + 1] = T₂{L}[i + 1]
Tactic:
have IH : T₁{L}[i] = T₂{L}[i] := IH (le_trans (by simp) hi)
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH✝ : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
IH : T₁{L}[i] = T₂{L}[i]
⊢ T₁{L}[i + 1] = T₂{L}[i + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH✝ : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
IH : T₁{L}[i] = T₂{L}[i]
⊢ T₁{L}[i + 1] = T₂{L}[i + 1]
Tactic:
have h₁ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₁{L}[i + 1]) := HT₁ i (lt_iff_succ_le.mpr hi)
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH✝ : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
IH : T₁{L}[i] = T₂{L}[i]
h₁ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₁{L}[i + 1])
⊢ T₁{L}[i + 1] = T₂{L}[i + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH✝ : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
IH : T₁{L}[i] = T₂{L}[i]
h₁ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₁{L}[i + 1])
⊢ T₁{L}[i + 1] = T₂{L}[i + 1]
Tactic:
have h₂ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₂{L}[i + 1]) := by simpa [IH] using HT₂ i (lt_iff_succ_le.mpr hi)
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH✝ : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
IH : T₁{L}[i] = T₂{L}[i]
h₁ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₁{L}[i + 1])
h₂ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₂{L}[i + 1])
⊢ T₁{L}[i + 1] = T₂{L}[i + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH✝ : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
IH : T₁{L}[i] = T₂{L}[i]
h₁ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₁{L}[i + 1])
h₂ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₂{L}[i + 1])
⊢ T₁{L}[i + 1] = T₂{L}[i + 1]
Tactic:
exact h₁.uniq h₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
⊢ i ≤ i + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.uniq
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH✝ : i ≤ iter → T₁{L}[i] = T₂{L}[i]
hi : i + 1 ≤ iter
IH : T₁{L}[i] = T₂{L}[i]
h₁ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₁{L}[i + 1])
⊢ Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₂{L}[i + 1])
Tactic:
simpa [IH] using HT₂ i (lt_iff_succ_le.mpr hi)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A k n : M
H : SeriesSegment U I L A k n
⊢ n ≤ k
Tactic:
rcases H with ⟨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 k n nₖ : M
left✝ : nₖ ≤ n
hT : Series U I L A (k / ‖I‖) nₖ
hS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₖ n
⊢ n ≤ k
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.le
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 k n nₖ : M
left✝ : nₖ ≤ n
hT : Series U I L A (k / ‖I‖) nₖ
hS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₖ n
⊢ n ≤ k
Tactic:
calc
  n ≤ nₖ + k % ‖I‖              := hS.le_add
  _ ≤ ‖I‖ * (k / ‖I‖) + k % ‖I‖ := by simpa [mul_comm] using hT.le_add
  _ = k                         := div_add_mod k ‖I‖
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A k n nₖ : M
left✝ : nₖ ≤ n
hT : Series U I L A (k / ‖I‖) nₖ
hS : Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₖ n
⊢ nₖ + k % ‖I‖ ≤ ‖I‖ * (k / ‖I‖) + k % ‖I‖
Tactic:
simpa [mul_comm] using hT.le_add
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.initial
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
Upos : 0 < U
⊢ 0 ≤ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.initial
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
Upos : 0 < U
⊢ IsSeries U I L A (0 / ‖I‖) 0 ∧ 0{L}[0] = 0 ∧ 0{L}[0 / ‖I‖] = 0
Tactic:
simp [IsSeries]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.initial
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
Upos : 0 < U
⊢ IsSegment L A (‖I‖ * (0 / ‖I‖)) (0 % ‖I‖) 0 ∧ 0{L}[0] = 0 ∧ 0{L}[0 % ‖I‖] = 0
Tactic:
simp [IsSegment]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A U I L k : M
Upos : 0 < U
⊢ 0 ≤ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A U I L k : M
Upos : 0 < U
x✝³ : M
x✝² : x✝³ < k / ‖I‖
x✝¹ : M
x✝ : x✝¹ < ‖I‖
⊢ 0{L}[x✝¹ + 1] = 0{L}[x✝¹] + fbit 0 (‖I‖ * x✝³ + x✝¹)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A U I L k : M
Upos : 0 < U
x✝¹ : M
x✝ : x✝¹ < k / ‖I‖
⊢ 0{L}[0] = 0{L}[x✝¹] ∧ 0{L}[‖I‖] = 0{L}[x✝¹ + 1]
Tactic:
simp
Proof state after:
no goals