case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) i = true
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
⊢ a[j] = b[j]

case inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) i = true
j : Nat
low : i ≤ j
high : j < size a
h : ¬i < size a
⊢ a[j] = b[j]
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) i = true
j : Nat
low : i ≤ j
high : j < size a
⊢ a[j] = b[j]
by_cases h : i < a.size
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv :
  (if h : i < size a then
      let_fun this := (_ : i < size b);
      decide (a[i] = b[i]) && isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1)
    else true) =
    true
⊢ a[j] = b[j]
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) i = true
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
⊢ a[j] = b[j]
unfold Array.isEqvAux at heqv
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
⊢ a[j] = b[j]
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv :
  (if h : i < size a then
      let_fun this := (_ : i < size b);
      decide (a[i] = b[i]) && isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1)
    else true) =
    true
⊢ a[j] = b[j]
simp [h] at heqv
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
hind : ∀ (j : Nat), i + 1 ≤ j → ∀ (high : j < size a), a[j] = b[j]
⊢ a[j] = b[j]
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
⊢ a[j] = b[j]
have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
hind : ∀ (j : Nat), i + 1 ≤ j → ∀ (high : j < size a), a[j] = b[j]
heq : i = j
⊢ a[j] = b[j]

case inl.inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
hind : ∀ (j : Nat), i + 1 ≤ j → ∀ (high : j < size a), a[j] = b[j]
heq : ¬i = j
⊢ a[j] = b[j]
case inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
hind : ∀ (j : Nat), i + 1 ≤ j → ∀ (high : j < size a), a[j] = b[j]
⊢ a[j] = b[j]
by_cases heq : i = j
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
hind : ∀ (j : Nat), i + 1 ≤ j → ∀ (high : j < size a), a[j] = b[j]
low : i ≤ i
high : i < size a
⊢ a[i] = b[i]
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
hind : ∀ (j : Nat), i + 1 ≤ j → ∀ (high : j < size a), a[j] = b[j]
heq : i = j
⊢ a[j] = b[j]
subst heq
no goals
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
hind : ∀ (j : Nat), i + 1 ≤ j → ∀ (high : j < size a), a[j] = b[j]
low : i ≤ i
high : i < size a
⊢ a[i] = b[i]
exact heqv.1
no goals
case inl.inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
j : Nat
low : i ≤ j
high : j < size a
h : i < size a
heqv : a[i] = b[i] ∧ isEqvAux a b hsz (fun x y => decide (x = y)) (i + 1) = true
hind : ∀ (j : Nat), i + 1 ≤ j → ∀ (high : j < size a), a[j] = b[j]
heq : ¬i = j
⊢ a[j] = b[j]
exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne low heq)) high
case inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) i = true
j : Nat
low : i ≤ j
high : j < size a
h : ¬i < size a
heq : i = size a
⊢ a[j] = b[j]
case inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) i = true
j : Nat
low : i ≤ j
high : j < size a
h : ¬i < size a
⊢ a[j] = b[j]
have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
case inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
j : Nat
high : j < size a
hi : size a ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) (size a) = true
low : size a ≤ j
h : ¬size a < size a
⊢ a[j] = b[j]
case inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
i : Nat
hi : i ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) i = true
j : Nat
low : i ≤ j
high : j < size a
h : ¬i < size a
heq : i = size a
⊢ a[j] = b[j]
subst heq
no goals
case inr
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
hsz : size a = size b
j : Nat
high : j < size a
hi : size a ≤ size a
heqv : isEqvAux a b hsz (fun x y => decide (x = y)) (size a) = true
low : size a ≤ j
h : ¬size a < size a
⊢ a[j] = b[j]
exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)