Theorem: IMOSL.Extra.EventuallyEqual.trans (IMOSLLean4/Extra/NatSequence/EventuallyEqual.lean)

State before:
α✝ : Sort u_1
a b c : Nat → α✝
h : EventuallyEqual a b
h0 : EventuallyEqual b c
⊢ EventuallyEqual a c
Tactic:
rcases h with ⟨N_a, N_b, h⟩
State after:
case intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
h0 : EventuallyEqual b c
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
⊢ EventuallyEqual a c

State before:
case intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
h0 : EventuallyEqual b c
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
⊢ EventuallyEqual a c
Tactic:
rcases h0 with ⟨K_b, K_c, h0⟩
State after:
case intro.intro.intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
K_b K_c : Nat
h0 : ∀ (k : Nat), b (k + K_b) = c (k + K_c)
⊢ EventuallyEqual a c

State before:
case intro.intro.intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
K_b K_c : Nat
h0 : ∀ (k : Nat), b (k + K_b) = c (k + K_c)
⊢ EventuallyEqual a c
Tactic:
refine ⟨K_b + N_a, K_c + N_b, λ k ↦ ?_⟩
State after:
case intro.intro.intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
K_b K_c : Nat
h0 : ∀ (k : Nat), b (k + K_b) = c (k + K_c)
k : Nat
⊢ a (k + (K_b + N_a)) = c (k + (K_c + N_b))

State before:
case intro.intro.intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
K_b K_c : Nat
h0 : ∀ (k : Nat), b (k + K_b) = c (k + K_c)
k : Nat
⊢ a (k + (K_b + N_a)) = c (k + (K_c + N_b))
Tactic:
rw [← Nat.add_assoc, h, Nat.add_right_comm, h0, Nat.add_right_comm, Nat.add_assoc]
State after:
no goals