how to use ext

Stream: general

[Frederick Pu]

when doing ext for proving two arrays equal you get the following

example (A B : Array Nat) : A = B := by
    ext

/- case h₁
    A B : Array Nat
    ⊢ A.size = B.size
case h₂
    A B : Array Nat
    i✝ : Nat
    hi₁✝ : i✝ < A.size
    hi₂✝ : i✝ < B.size
    ⊢ A[i✝] = B[i✝]
-/

how do you get access to the implicit variables in the second goal?

[Kyle Miller]

You could use the rename_i tactic to rename these inaccessible variables

[Frederick Pu]

but is there a way to like match each goal when using ext?

[Kyle Miller]

I think you can also do ext i h1 h2 to name the variables that appear

[Frederick Pu]

thx