internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_append_last
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i X : M
hi : i ≤ ‖I‖
hX : ‖X‖ ≤ ‖L‖
⊢ append I L S i X{L}[i] = (S % bexp (I # L) (i * ‖L‖) + X * bexp (I # L) (i * ‖L‖)){L}[i + 0]
Tactic:
simp [append]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_append_last
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i X : M
hi : i ≤ ‖I‖
hX : ‖X‖ ≤ ‖L‖
⊢ i + 0 ≤ ‖I‖
Tactic:
simpa using hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.ext_append_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
I L S i j X : M
hi : i ≤ ‖I‖
hij : j < i
⊢ (S % bexp (I # L) (i * ‖L‖) + S / bexp (I # L) (i * ‖L‖) * bexp (I # L) (i * ‖L‖)){L}[j] = S{L}[j]
Tactic:
rw [add_comm, mul_comm, div_add_mod]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.series
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
⊢ ∃ T S,
    IsSeries U I L A (k / ‖I‖) T ∧
      IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S ∧ T{L}[0] = 0 ∧ T{L}[k / ‖I‖] = S{L}[0] ∧ S{L}[k % ‖I‖] = n
Tactic:
rcases H with ⟨_, _, ⟨T, _, hT, hTₛ, hTₑ⟩, ⟨S, _, hS, rfl, rfl⟩⟩
Proof state after:
case intro.intro.intro.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 k T : M
left✝² : T < U
hT : IsSeries U I L A (k / ‖I‖) T
hTₛ : T{L}[0] = 0
S : M
left✝¹ : S < U
hS : IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S
hTₑ : T{L}[k / ‖I‖] = S{L}[0]
left✝ : S{L}[0] ≤ S{L}[k % ‖I‖]
⊢ ∃ T S_1,
    IsSeries U I L A (k / ‖I‖) T ∧
      IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S_1 ∧
        T{L}[0] = 0 ∧ T{L}[k / ‖I‖] = S_1{L}[0] ∧ S_1{L}[k % ‖I‖] = S{L}[k % ‖I‖]
Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.series
Proof state before:
case intro.intro.intro.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 k T : M
left✝² : T < U
hT : IsSeries U I L A (k / ‖I‖) T
hTₛ : T{L}[0] = 0
S : M
left✝¹ : S < U
hS : IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S
hTₑ : T{L}[k / ‖I‖] = S{L}[0]
left✝ : S{L}[0] ≤ S{L}[k % ‖I‖]
⊢ ∃ T S_1,
    IsSeries U I L A (k / ‖I‖) T ∧
      IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S_1 ∧
        T{L}[0] = 0 ∧ T{L}[k / ‖I‖] = S_1{L}[0] ∧ S_1{L}[k % ‖I‖] = S{L}[k % ‖I‖]
Tactic:
exact ⟨T, S, hT, hS, hTₛ, hTₑ, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
⊢ ∀ i ≤ intv, S{L}[i] ≤ S{L}[0] + i
Tactic:
intro 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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
⊢ i ≤ intv → S{L}[i] ≤ S{L}[0] + i
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
⊢ i ≤ intv → S{L}[i] ≤ S{L}[0] + i
Tactic:
induction i 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✝ L A start intv S : M
H : IsSegment L A start intv S
⊢ 𝚺₀-Predicate fun i => i ≤ intv → S{L}[i] ≤ S{L}[0] + i

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✝ L A start intv S : M
H : IsSegment L A start intv S
⊢ 0 ≤ intv → S{L}[0] ≤ S{L}[0] + 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✝ L A start intv S : M
H : IsSegment L A start intv S
x✝ : M
a✝ : x✝ ≤ intv → S{L}[x✝] ≤ S{L}[0] + x✝
⊢ x✝ + 1 ≤ intv → S{L}[x✝ + 1] ≤ S{L}[0] + (x✝ + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
⊢ 0 ≤ intv → S{L}[0] ≤ S{L}[0] + 0
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
⊢ i + 1 ≤ intv → S{L}[i + 1] ≤ S{L}[0] + (i + 1)
Tactic:
case succ i IH =>
  intro h
  have IH : S{L}[i] ≤ S{L}[0] + i := IH (le_trans (by simp) h)
  calc
    S{L}[i + 1] = S{L}[i] + fbit A (start + i) := H i (succ_le_iff_lt.mp h)
    _           ≤ S{L}[i] + 1                  := by simp
    _           ≤ S{L}[0] + (i + 1)            := by simp [←add_assoc, IH]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
⊢ 𝚺₀-Predicate fun i => i ≤ intv → S{L}[i] ≤ S{L}[0] + i
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
⊢ 0 ≤ intv → S{L}[0] ≤ S{L}[0] + 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
⊢ i + 1 ≤ intv → S{L}[i + 1] ≤ S{L}[0] + (i + 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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
h : i + 1 ≤ intv
⊢ S{L}[i + 1] ≤ S{L}[0] + (i + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
h : i + 1 ≤ intv
⊢ S{L}[i + 1] ≤ S{L}[0] + (i + 1)
Tactic:
have IH : S{L}[i] ≤ S{L}[0] + i := 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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH✝ : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
h : i + 1 ≤ intv
IH : S{L}[i] ≤ S{L}[0] + i
⊢ S{L}[i + 1] ≤ S{L}[0] + (i + 1)
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH✝ : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
h : i + 1 ≤ intv
IH : S{L}[i] ≤ S{L}[0] + i
⊢ S{L}[i + 1] ≤ S{L}[0] + (i + 1)
Tactic:
calc
  S{L}[i + 1] = S{L}[i] + fbit A (start + i) := H i (succ_le_iff_lt.mp h)
  _           ≤ S{L}[i] + 1                  := by simp
  _           ≤ S{L}[0] + (i + 1)            := by simp [←add_assoc, IH]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
h : i + 1 ≤ intv
⊢ i ≤ i + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH✝ : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
h : i + 1 ≤ intv
IH : S{L}[i] ≤ S{L}[0] + i
⊢ S{L}[i] + fbit A (start + i) ≤ S{L}[i] + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSegment.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✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH✝ : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
h : i + 1 ≤ intv
IH : S{L}[i] ≤ S{L}[0] + i
⊢ S{L}[i] + 1 ≤ S{L}[0] + (i + 1)
Tactic:
simp [←add_assoc, IH]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.refl
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 L A start n : M
hL : L # 1 ≤ U
hn : ‖n‖ ≤ ‖L‖
⊢ IsSegment L A start 0 n
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 L A start n : M
hL : L # 1 ≤ U
hn : ‖n‖ ≤ ‖L‖
i✝ : M
⊢ i✝ < 0 → n{L}[i✝ + 1] = n{L}[i✝] + fbit A (start + i✝)
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.refl
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 L A start n : M
hL : L # 1 ≤ U
hn : ‖n‖ ≤ ‖L‖
i✝ : M
⊢ i✝ < 0 → n{L}[i✝ + 1] = n{L}[i✝] + fbit A (start + i✝)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv nₛ nₑ : M
H : Segment U L A start intv nₛ nₑ
⊢ nₑ ≤ nₛ + intv
Tactic:
rcases H with ⟨S, _, hS, rfl, 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 L A start intv S : M
left✝ : S < U
hS : IsSegment L A start intv S
⊢ S{L}[intv] ≤ S{L}[0] + intv
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S : M
left✝ : S < U
hS : IsSegment L A start intv S
⊢ S{L}[intv] ≤ S{L}[0] + intv
Tactic:
exact hS.le_add intv (by rfl)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S : M
left✝ : S < U
hS : IsSegment L A start intv S
⊢ intv ≤ intv
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv nₛ nₑ₁ nₑ₂ : M
H₁ : Segment U L A start intv nₛ nₑ₁
H₂ : Segment U L A start intv nₛ nₑ₂
⊢ nₑ₁ = nₑ₂
Tactic:
rcases H₁ with ⟨S₁, _, HS₁, 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 L A start intv nₛ nₑ₂ : M
H₂ : Segment U L A start intv nₛ nₑ₂
S₁ : M
left✝ : S₁ < U
HS₁ : IsSegment L A start intv S₁
Hₛ : S₁{L}[0] = nₛ
⊢ S₁{L}[intv] = nₑ₂
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv nₛ nₑ₂ : M
H₂ : Segment U L A start intv nₛ nₑ₂
S₁ : M
left✝ : S₁ < U
HS₁ : IsSegment L A start intv S₁
Hₛ : S₁{L}[0] = nₛ
⊢ S₁{L}[intv] = nₑ₂
Tactic:
rcases H₂ with ⟨S₂, _, HS₂, rfl, 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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ S₁{L}[intv] = S₂{L}[intv]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ S₁{L}[intv] = S₂{L}[intv]
Tactic:
suffices ∀ i ≤ intv, S₁{L}[i] = S₂{L}[i] from this intv (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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ ∀ i ≤ intv, S₁{L}[i] = S₂{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ ∀ i ≤ intv, S₁{L}[i] = S₂{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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
⊢ i ≤ intv → S₁{L}[i] = S₂{L}[i]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
⊢ i ≤ intv → S₁{L}[i] = S₂{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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ 𝚺₀-Predicate fun i => i ≤ intv → S₁{L}[i] = S₂{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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ 0 ≤ intv → S₁{L}[0] = S₂{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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
x✝ : M
a✝ : x✝ ≤ intv → S₁{L}[x✝] = S₂{L}[x✝]
⊢ x✝ + 1 ≤ intv → S₁{L}[x✝ + 1] = S₂{L}[x✝ + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ 0 ≤ intv → S₁{L}[0] = S₂{L}[0]
Tactic:
case zero => intro _; exact Hₛ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
⊢ i + 1 ≤ intv → S₁{L}[i + 1] = S₂{L}[i + 1]
Tactic:
case succ i IH =>
  intro hi
  have h₁ : S₁{L}[i + 1] = S₁{L}[i] + fbit A (start + i) := HS₁ i (lt_iff_succ_le.mpr hi)
  have h₂ : S₂{L}[i + 1] = S₂{L}[i] + fbit A (start + i) := HS₂ i (lt_iff_succ_le.mpr hi)
  simp [IH (le_trans (by simp) hi), h₁, h₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
this : ∀ i ≤ intv, S₁{L}[i] = S₂{L}[i]
⊢ intv ≤ intv
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ 𝚺₀-Predicate fun i => i ≤ intv → S₁{L}[i] = S₂{L}[i]
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
⊢ 0 ≤ intv → S₁{L}[0] = S₂{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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
a✝ : 0 ≤ intv
⊢ S₁{L}[0] = S₂{L}[0]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
a✝ : 0 ≤ intv
⊢ S₁{L}[0] = S₂{L}[0]
Tactic:
exact Hₛ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
⊢ i + 1 ≤ intv → S₁{L}[i + 1] = S₂{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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
hi : i + 1 ≤ intv
⊢ S₁{L}[i + 1] = S₂{L}[i + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
hi : i + 1 ≤ intv
⊢ S₁{L}[i + 1] = S₂{L}[i + 1]
Tactic:
have h₁ : S₁{L}[i + 1] = S₁{L}[i] + fbit A (start + i) := HS₁ 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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
hi : i + 1 ≤ intv
h₁ : S₁{L}[i + 1] = S₁{L}[i] + fbit A (start + i)
⊢ S₁{L}[i + 1] = S₂{L}[i + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
hi : i + 1 ≤ intv
h₁ : S₁{L}[i + 1] = S₁{L}[i] + fbit A (start + i)
⊢ S₁{L}[i + 1] = S₂{L}[i + 1]
Tactic:
have h₂ : S₂{L}[i + 1] = S₂{L}[i] + fbit A (start + i) := HS₂ 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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
hi : i + 1 ≤ intv
h₁ : S₁{L}[i + 1] = S₁{L}[i] + fbit A (start + i)
h₂ : S₂{L}[i + 1] = S₂{L}[i] + fbit A (start + i)
⊢ S₁{L}[i + 1] = S₂{L}[i + 1]
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
hi : i + 1 ≤ intv
h₁ : S₁{L}[i + 1] = S₁{L}[i] + fbit A (start + i)
h₂ : S₂{L}[i + 1] = S₂{L}[i] + fbit A (start + i)
⊢ S₁{L}[i + 1] = S₂{L}[i + 1]
Tactic:
simp [IH (le_trans (by simp) hi), h₁, h₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.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 L A start intv S₁ : M
left✝¹ : S₁ < U
HS₁ : IsSegment L A start intv S₁
S₂ : M
left✝ : S₂ < U
HS₂ : IsSegment L A start intv S₂
Hₛ : S₁{L}[0] = S₂{L}[0]
i : M
IH : i ≤ intv → S₁{L}[i] = S₂{L}[i]
hi : i + 1 ≤ intv
h₁ : S₁{L}[i + 1] = S₁{L}[i] + fbit A (start + i)
h₂ : S₂{L}[i + 1] = S₂{L}[i] + fbit A (start + i)
⊢ i ≤ i + 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 ≤ iter, T{L}[l] ≤ T{L}[0] + ‖I‖ * l
Tactic:
intro l
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
⊢ l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l