α : Type u_1
inst✝ : DecidableEq α
a b : Array α
⊢ (if h : size a = size b then isEqvAux a b h (fun x y => decide (x = y)) 0 else false) = true → a = b
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
⊢ (isEqv a b fun x y => decide (x = y)) = true → a = b
simp [Array.isEqv]
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : size a = size b
⊢ isEqvAux a b h✝ (fun x y => decide (x = y)) 0 = true → a = b

case inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : ¬size a = size b
⊢ False → a = b
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
⊢ (if h : size a = size b then isEqvAux a b h (fun x y => decide (x = y)) 0 else false) = true → a = b
split
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : size a = size b
⊢ isEqvAux a b h✝ (fun x y => decide (x = y)) 0 = true → a = b
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : size a = size b
⊢ isEqvAux a b h✝ (fun x y => decide (x = y)) 0 = true → a = b

case inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : ¬size a = size b
⊢ False → a = b
case inr => intro; contradiction
no goals
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : size a = size b
⊢ isEqvAux a b h✝ (fun x y => decide (x = y)) 0 = true → a = b
case inl hsz =>
 intro h
 have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h
 exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : ¬size a = size b
a✝ : False
⊢ a = b
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : ¬size a = size b
⊢ False → a = b
intro
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : ¬size a = size b
a✝ : False
⊢ a = b
contradiction
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
h : isEqvAux a b hsz (fun x y => decide (x = y)) 0 = true
⊢ a = b
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
⊢ isEqvAux a b hsz (fun x y => decide (x = y)) 0 = true → a = b
intro h
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
h : isEqvAux a b hsz (fun x y => decide (x = y)) 0 = true
aux : ∀ (j : Nat), 0 ≤ j → ∀ (high : j < size a), a[j] = b[j]
⊢ a = b
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
h : isEqvAux a b hsz (fun x y => decide (x = y)) 0 = true
⊢ a = b
have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
h : isEqvAux a b hsz (fun x y => decide (x = y)) 0 = true
aux : ∀ (j : Nat), 0 ≤ j → ∀ (high : j < size a), a[j] = b[j]
⊢ a = b
exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _