Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.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 I L A k n₁ n₂ : M
H₁ : SeriesSegment U I L A k n₁
H₂ : SeriesSegment U I L A k n₂
⊢ n₁ = n₂
Tactic:
rcases H₁ with ⟨nₘ₁, _, hT₁, hS₁⟩
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
H₂ : SeriesSegment 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₁ = n₂

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
H₂ : SeriesSegment 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₁ = n₂
Tactic:
rcases H₂ with ⟨nₘ₂, _, hT₂, hS₂⟩
State after:
case 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 n₁ 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ₘ₂ : 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₁ = n₂

State before:
case 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 n₁ 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ₘ₂ : 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₁ = n₂
Tactic:
rcases show nₘ₁ = nₘ₂ from hT₁.uniq hT₂
State after:
case intro.intro.intro.intro.intro.intro.refl
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₂ 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₁
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₁ = n₂

State before:
case intro.intro.intro.intro.intro.intro.refl
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₂ 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₁
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₁ = n₂
Tactic:
exact hS₁.uniq hS₂
State after:
no goals