Theorem: LO.FirstOrder.Arith.Model.Nuon.SeriesSegment.series (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 : 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⟩⟩
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‖]

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