-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem any_eq_anyTR : @any = @anyTR :=
  funext fun n => funext fun f =>
  let rec go : ∀ m n f, any (m + n) f = (any n (fun i h => f i (by omega)) || anyTR.loop (m + n) f m (by omega))
    | 0,      n, f => by
      simp [anyTR.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
t : m + 1 + n = m + (n + 1)
⊢ (m + 1 + n).any f = ((n.any fun i h => f i ⋯) || (f (m + 1 + n - (m + 1)) ⋯ || anyTR.loop (m + 1 + n) f m ⋯))

Tactic:
rw [any_congr t, anyTR_loop_congr t, go, any, Bool.or_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.any fun i h => f i ⋯) || (f n ⋯ || anyTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯)) =
    ((n.any fun i h => f i ⋯) || (f (m + 1 + n - (m + 1)) ⋯ || anyTR.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
t : m + 1 + n = m + (n + 1)
⊢ ((n.any fun i h => f i ⋯) || (f n ⋯ || anyTR.loop (m + (n + 1)) (fun i h => f i ⋯) m ⋯)) =
    ((n.any fun i h => f i ⋯) || (f (m + 1 + n - (m + 1)) ⋯ || anyTR.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
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
⊢ (m.succ + n).any f = ((n.any fun i h => f i ⋯) || anyTR.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).any f = ((n.any fun i h => f i ⋯) || anyTR.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 + n → Bool
i : Nat
h : i < n
⊢ i < m + n

Tactic:
omega

Result:
no goals

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).any f = n.any fun i h => f i ⋯

Tactic:
rw [any_congr t]

Result:
no goals

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
n : Nat
f : (i : Nat) → i < 0 + n → Bool
⊢ (0 + n).any f = ((n.any fun i h => f i ⋯) || anyTR.loop (0 + n) f 0 ⋯)

Tactic:
simp [anyTR.loop]

Result:
n✝ : Nat
f✝ : (i : Nat) → i < n✝ → Bool
n : Nat
f : (i : Nat) → i < 0 + n → Bool
⊢ (0 + n).any f = n.any 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).any f = ((n.any fun i h => f i ⋯) || anyTR.loop (m.succ + n) f m.succ ⋯)

Tactic:
rw [anyTR.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).any f = ((n.any fun i h => f i ⋯) || (f (m.succ + n - m.succ) ⋯ || anyTR.loop (m.succ + n) f m ⋯))

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).any f = ((n.any fun i h => f i ⋯) || (f (m.succ + n - m.succ) ⋯ || anyTR.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).any f = ((n.any fun i h => f i ⋯) || (f (m + 1 + n - (m + 1)) ⋯ || anyTR.loop (m + 1 + n) f 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:
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
n : Nat
f : (i : Nat) → i < 0 + n → Bool
⊢ (0 + n).any f = n.any 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).any f = n.any fun i h => f i ⋯