-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem all_eq_allTR : @all = @allTR :=
  funext fun n => funext fun f =>
  let rec go : ∀ m n f, all (m + n) f = (all n (fun i h => f i (by omega)) && allTR.loop (m + n) f m (by omega))
    | 0,      n, f => by
      simp [allTR.loop]
      have t : 0 + n = n

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
⊢ (m.succ + n).all f = ((n.all fun i h => f i ⋯) && allTR.loop (m.succ + n) f m.succ ⋯)

Tactic:
have t : (m + 1) + n = m + (n + 1) := by omega

Result:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ (m.succ + n).all f = ((n.all fun i h => f i ⋯) && allTR.loop (m.succ + n) f m.succ ⋯)

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ (m + 1 + n).all f = ((n.all fun i h => f i ⋯) && (f (m + 1 + n - (m + 1)) ⋯ && allTR.loop (m + 1 + n) f m ⋯))

Tactic:
rw [all_congr t, allTR_loop_congr t, go, all, Bool.and_assoc]

Result:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ ((n.all fun i h => f i ⋯) && (f n ⋯ && allTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯)) =
    ((n.all fun i h => f i ⋯) && (f (m + 1 + n - (m + 1)) ⋯ && allTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯))

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
⊢ m + 1 + n = m + (n + 1)

Tactic:
omega

Result:
no goals

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
n : Nat
f : (i : Nat) → i < 0 + n → Bool
⊢ 0 + n = n

Tactic:
omega

Result:
no goals

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ (m.succ + n).all f = ((n.all fun i h => f i ⋯) && allTR.loop (m.succ + n) f m.succ ⋯)

Tactic:
rw [allTR.loop]

Result:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ (m.succ + n).all f = ((n.all fun i h => f i ⋯) && (f (m.succ + n - m.succ) ⋯ && allTR.loop (m.succ + n) f m ⋯))

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
n : Nat
f : (i : Nat) → i < 0 + n → Bool
⊢ (0 + n).all f = ((n.all fun i h => f i ⋯) && allTR.loop (0 + n) f 0 ⋯)

Tactic:
simp [allTR.loop]

Result:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
n : Nat
f : (i : Nat) → i < 0 + n → Bool
⊢ (0 + n).all f = n.all fun i h => f i ⋯

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
n : Nat
f : (i : Nat) → i < 0 + n → Bool
⊢ (0 + n).all f = n.all fun i h => f i ⋯

Tactic:
have t : 0 + n = n := by omega

Result:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
n : Nat
f : (i : Nat) → i < 0 + n → Bool
t : 0 + n = n
⊢ (0 + n).all f = n.all fun i h => f i ⋯

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ (m.succ + n).all f = ((n.all fun i h => f i ⋯) && (f (m.succ + n - m.succ) ⋯ && allTR.loop (m.succ + n) f m ⋯))

Tactic:
simp only [succ_eq_add_one]

Result:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ (m + 1 + n).all f = ((n.all fun i h => f i ⋯) && (f (m + 1 + n - (m + 1)) ⋯ && allTR.loop (m + 1 + n) f m ⋯))

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
n : Nat
f : (i : Nat) → i < 0 + n → Bool
t : 0 + n = n
⊢ (0 + n).all f = n.all fun i h => f i ⋯

Tactic:
rw [all_congr t]

Result:
no goals

Proof state:
case e_y.e_x.e_i
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ n = m + 1 + n - (m + 1)

Tactic:
omega

Result:
no goals

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ ((n.all fun i h => f i ⋯) && (f n ⋯ && allTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯)) =
    ((n.all fun i h => f i ⋯) && (f (m + 1 + n - (m + 1)) ⋯ && allTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯))

Tactic:
congr

Result:
case e_y.e_x.e_i
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m.succ + n → Bool
t : m + 1 + n = m + (n + 1)
⊢ n = m + 1 + n - (m + 1)

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m + n → Bool
⊢ m ≤ m + n

Tactic:
omega

Result:
no goals

Proof state:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
m n : Nat
f : (i : Nat) → i < m + n → Bool
i : Nat
h : i < n
⊢ i < m + n

Tactic:
omega

Result:
no goals