-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem rel_of_isEqvAux
    {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
    (heqv : Array.isEqvAux a b hsz r i hi)
    {j : Nat} (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))

Proof state:
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : ¬j < i
⊢ r a[j] b[j] = true

Tactic:
replace hj' : j = i := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp hj') hj

Result:
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : j = i
⊢ r a[j] b[j] = true

Proof state:
case zero
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j : Nat
hi : 0 ≤ a.size
heqv : a.isEqvAux b hsz r 0 hi = true
hj : j < 0
⊢ r a[j] b[j] = true

Tactic:
contradiction

Result:
no goals

Proof state:
case succ
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
heqv : a.isEqvAux b hsz r (i + 1) hi = true
hj : j < i + 1
⊢ r a[j] b[j] = true

Tactic:
simp only [Array.isEqvAux, Bool.and_eq_true, decide_eq_true_eq] at heqv

Result:
case succ
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
⊢ r a[j] b[j] = true

Proof state:
case succ
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
⊢ r a[j] b[j] = true

Tactic:
by_cases hj' : j < i

Result:
case pos
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : j < i
⊢ r a[j] b[j] = true

case neg
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : ¬j < i
⊢ r a[j] b[j] = true

Proof state:
case neg
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : ¬j < i
⊢ r a[j] b[j] = true

Tactic:
next =>
  replace hj' : j = i := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp hj') hj
  subst hj'
  exact heqv.left

Result:
no goals

Proof state:
case pos
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : j < i
⊢ r a[j] b[j] = true

case neg
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : ¬j < i
⊢ r a[j] b[j] = true

Tactic:
next =>
  exact ih _ heqv.right hj'

Result:
case neg
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : ¬j < i
⊢ r a[j] b[j] = true

Proof state:
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : j = i
⊢ r a[j] b[j] = true

Tactic:
subst hj'

Result:
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j : Nat
ih : ∀ (hi : j ≤ a.size), a.isEqvAux b hsz r j hi = true → ∀ (hj : j < j), r a[j] b[j] = true
hi : j + 1 ≤ a.size
hj : j < j + 1
heqv : r a[j] b[j] = true ∧ a.isEqvAux b hsz r j ⋯ = true
⊢ r a[j] b[j] = true

Proof state:
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j i : Nat
ih : ∀ (hi : i ≤ a.size), a.isEqvAux b hsz r i hi = true → ∀ (hj : j < i), r a[j] b[j] = true
hi : i + 1 ≤ a.size
hj : j < i + 1
heqv : r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true
hj' : j < i
⊢ r a[j] b[j] = true

Tactic:
exact ih _ heqv.right hj'

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
i : Nat
hi : i ≤ a.size
heqv : a.isEqvAux b hsz r i hi = true
j : Nat
hj : j < i
⊢ r a[j] b[j] = true

Tactic:
induction i with
| zero => contradiction
| succ i ih =>
  simp only [Array.isEqvAux, Bool.and_eq_true, decide_eq_true_eq] at heqv
  by_cases hj' : j < i
  next =>
    exact ih _ heqv.right hj'
  next =>
    replace hj' : j = i := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp hj') hj
    subst hj'
    exact heqv.left

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
j : Nat
ih : ∀ (hi : j ≤ a.size), a.isEqvAux b hsz r j hi = true → ∀ (hj : j < j), r a[j] b[j] = true
hi : j + 1 ≤ a.size
hj : j < j + 1
heqv : r a[j] b[j] = true ∧ a.isEqvAux b hsz r j ⋯ = true
⊢ r a[j] b[j] = true

Tactic:
exact heqv.left

Result:
no goals