Theorem: LO.FirstOrder.Arith.Model.Nuon.Segment.uniq (Arithmetization/OmegaOne/Nuon.lean)

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⟩
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ₑ₂

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⟩
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]

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)
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]

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
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]

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
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]

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ₛ
State after:
no goals

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₂]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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 _
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]

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ₛ
State after:
no goals

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
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]

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)
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]

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)
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]

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₂]
State after:
no goals

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
State after:
no goals