-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/BEq.lean
theorem isEqv_eq_decide (a b : List α) (r) :
    isEqv a b r = if h : a.length = b.length then
      decide (∀ (i : Nat) (h' : i < a.length), r (a[i]'(h ▸ h')) (b[i]'(h ▸ h'))) else false

Proof state:
case cons
α : Type u_1
r : α → α → Bool
a : α
as : List α
ih :
  ∀ (b : List α),
    as.isEqv b r =
      if h : as.length = b.length then decide (∀ (i : Nat) (h' : i < as.length), r as[i] b[i] = true) else false
b : List α
⊢ (a :: as).isEqv b r =
    if h : (a :: as).length = b.length then decide (∀ (i : Nat) (h' : i < (a :: as).length), r (a :: as)[i] b[i] = true)
    else false

Tactic:
cases b with
| nil => simp
| cons b bs =>
  simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]
  split <;> simp [Nat.forall_lt_succ_left']

Result:
no goals

Proof state:
α : Type u_1
a b : List α
r : α → α → Bool
⊢ a.isEqv b r = if h : a.length = b.length then decide (∀ (i : Nat) (h' : i < a.length), r a[i] b[i] = true) else false

Tactic:
induction a generalizing b with
| nil =>
  cases b <;> simp
| cons a as ih =>
  cases b with
  | nil => simp
  | cons b bs =>
    simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]
    split <;> simp [Nat.forall_lt_succ_left']

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
r : α → α → Bool
a : α
as : List α
ih :
  ∀ (b : List α),
    as.isEqv b r =
      if h : as.length = b.length then decide (∀ (i : Nat) (h' : i < as.length), r as[i] b[i] = true) else false
⊢ (a :: as).isEqv [] r =
    if h : (a :: as).length = [].length then
      decide (∀ (i : Nat) (h' : i < (a :: as).length), r (a :: as)[i] [][i] = true)
    else false

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
r : α → α → Bool
a : α
as : List α
ih :
  ∀ (b : List α),
    as.isEqv b r =
      if h : as.length = b.length then decide (∀ (i : Nat) (h' : i < as.length), r as[i] b[i] = true) else false
b : α
bs : List α
⊢ (a :: as).isEqv (b :: bs) r =
    if h : (a :: as).length = (b :: bs).length then
      decide (∀ (i : Nat) (h' : i < (a :: as).length), r (a :: as)[i] (b :: bs)[i] = true)
    else false

Tactic:
simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]

Result:
case cons.cons
α : Type u_1
r : α → α → Bool
a : α
as : List α
ih :
  ∀ (b : List α),
    as.isEqv b r =
      if h : as.length = b.length then decide (∀ (i : Nat) (h' : i < as.length), r as[i] b[i] = true) else false
b : α
bs : List α
⊢ (r a b &&
      if h : as.length = bs.length then decide (∀ (i : Nat) (h' : i < as.length), r as[i] bs[i] = true) else false) =
    if h : as.length = bs.length then decide (∀ (i : Nat) (h' : i < as.length + 1), r (a :: as)[i] (b :: bs)[i] = true)
    else false

Proof state:
case nil
α : Type u_1
r : α → α → Bool
b : List α
⊢ [].isEqv b r =
    if h : [].length = b.length then decide (∀ (i : Nat) (h' : i < [].length), r [][i] b[i] = true) else false

Tactic:
cases b <;> simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
r : α → α → Bool
a : α
as : List α
ih :
  ∀ (b : List α),
    as.isEqv b r =
      if h : as.length = b.length then decide (∀ (i : Nat) (h' : i < as.length), r as[i] b[i] = true) else false
b : α
bs : List α
⊢ (r a b &&
      if h : as.length = bs.length then decide (∀ (i : Nat) (h' : i < as.length), r as[i] bs[i] = true) else false) =
    if h : as.length = bs.length then decide (∀ (i : Nat) (h' : i < as.length + 1), r (a :: as)[i] (b :: bs)[i] = true)
    else false

Tactic:
split <;> simp [Nat.forall_lt_succ_left']

Result:
no goals