Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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 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⟩
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₂

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

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

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

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

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

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

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

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

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

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