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

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

State before:
case intro.intro
α✝ : Sort u_1
a b : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
⊢ EventuallyEqual b a
Tactic:
exact ⟨N_b, N_a, λ k ↦ (h k).symm⟩
State after:
no goals