A tactic for "reaching" inside a quantified statement?

Stream: Is there code for X?

[Kent Van Vels]

I am trying to show a claim related to Cauchy sequences. I understand there is support in mathlib for Cauchy sequences, but I want to understand this myself. I get to this state in my proof/code.

u0 u1 : cauchy_seqQ,
h0 : ∀ (ε : ℚ), 0 < ε → (∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |u0.z n - u1.z n| ≤ ε)
⊢ ∀ (ε : ℚ), 0 < ε → (∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |u1.z n - u0.z n| ≤ ε)

Is there a way to use abs_sub_comm inside the conclusion somehow so I can use the h0 hypothesis?

I can unwrap and rewrap the quantifiers, but I am thinking there has to be a better way. Any help is appreciated.

[Yaël Dillies]

Use simp_rw :wink:

[Kent Van Vels]

Thank you. It worked great.

[Kyle Miller]

I once made a tactic for this situation, and to use it you'd write something like enter h0 with ε hε N n hN. But that's not in mathlib, and it might not even work anymore.

Another suggestion is simpa [abs_sub_comm] using h0

[Alex J. Best]

tactic#conv can also be very useful for things like this, where you need very precise control of the rewrites. Sometimes it can be a little inconvenient if the rewrites have nontrivial side conditions though