Theorem: Array.ext_iff (LeanColls/Data/Array.lean)

State before:
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ A = B ↔ ∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]
Tactic:
constructor
State after:
case mp
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ A = B → ∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]

case mpr
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ (∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]) → A = B

State before:
case mp
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ A = B → ∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]
Tactic:
rintro rfl
State after:
case mp
α : Type u_1
A : Array α
h : A.size = A.size
⊢ ∀ (i : ℕ) (h1 h2 : i < A.size), A[i] = A[i]

State before:
case mp
α : Type u_1
A : Array α
h : A.size = A.size
⊢ ∀ (i : ℕ) (h1 h2 : i < A.size), A[i] = A[i]
Tactic:
simp
State after:
no goals

State before:
case mpr
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ (∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]) → A = B
Tactic:
apply ext _ _ h
State after:
no goals