-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1)
    (x) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x =
      f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .)

Proof state:
case refl.e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
x✝ : α ⟨n + 1, ⋯⟩
⊢ dfoldlM.loop (n + 1) α f (n + 1) ⋯ x✝ = dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) n h x✝

Tactic:
rw [dfoldlM_loop_eq, dfoldlM_loop_eq]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
⊢ dfoldlM.loop (n + 1) α f i ⋯ x = do
    let x ← f ⟨i, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x

Tactic:
if h' : i < n then
  rw [dfoldlM_loop_lt _ h _]
  congr; funext
  rw [dfoldlM_loop_lt _ h' _, dfoldlM_loop]; rfl
else
  cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
  rw [dfoldlM_loop_lt]
  congr; funext
  rw [dfoldlM_loop_eq, dfoldlM_loop_eq]

Result:
no goals

Proof state:
case e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
x✝ : α ⟨i + 1, ⋯⟩
⊢ (do
      let x ← f ⟨i + 1, ?e_a.h.h✝⟩ x✝
      dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) (i + 1) ?e_a.h.h✝ x) =
    f ⟨i, h'⟩.succ x✝ >>= dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) (i + 1) ⋯

case e_a.h.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
x✝ : α ⟨i + 1, ⋯⟩
⊢ i + 1 < n + 1

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : ¬i < n
⊢ dfoldlM.loop (n + 1) α f i ⋯ x = do
    let x ← f ⟨i, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x

Tactic:
cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')

Result:
case refl
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
⊢ dfoldlM.loop (n + 1) α f n ⋯ x = do
    let x ← f ⟨n, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) n h x

Proof state:
case refl
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
⊢ f ⟨n, ?refl.h⟩ x >>= dfoldlM.loop (n + 1) α f (n + 1) ⋯ = do
    let x ← f ⟨n, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) n h x

case refl.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
⊢ n < n + 1

Tactic:
congr

Result:
case refl.e_a
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
⊢ dfoldlM.loop (n + 1) α f (n + 1) ⋯ = fun x => dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) n h x

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
⊢ f ⟨i, h⟩ x >>= dfoldlM.loop (n + 1) α f (i + 1) ⋯ = do
    let x ← f ⟨i, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
⊢ dfoldlM.loop (n + 1) α f (i + 1) ⋯ = fun x => dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x

Proof state:
case e_a
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
⊢ dfoldlM.loop (n + 1) α f (i + 1) ⋯ = fun x => dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x

Tactic:
funext

Result:
case e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
x✝ : α ⟨i + 1, ⋯⟩
⊢ dfoldlM.loop (n + 1) α f (i + 1) ⋯ x✝ = dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x✝

Proof state:
case e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
x✝ : α ⟨i + 1, ⋯⟩
⊢ dfoldlM.loop (n + 1) α f (i + 1) ⋯ x✝ = dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x✝

Tactic:
rw [dfoldlM_loop_lt _ h' _, dfoldlM_loop]

Result:
case e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
x✝ : α ⟨i + 1, ⋯⟩
⊢ (do
      let x ← f ⟨i + 1, ?e_a.h.h✝⟩ x✝
      dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) (i + 1) ?e_a.h.h✝ x) =
    f ⟨i, h'⟩.succ x✝ >>= dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) (i + 1) ⋯

case e_a.h.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
x✝ : α ⟨i + 1, ⋯⟩
⊢ i + 1 < n + 1

Proof state:
case refl.e_a
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
⊢ dfoldlM.loop (n + 1) α f (n + 1) ⋯ = fun x => dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) n h x

Tactic:
funext

Result:
case refl.e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : n < n + 1
x : α ⟨n, ⋯⟩
h' : ¬n < n
x✝ : α ⟨n + 1, ⋯⟩
⊢ dfoldlM.loop (n + 1) α f (n + 1) ⋯ x✝ = dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) n h x✝

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
⊢ dfoldlM.loop (n + 1) α f i ⋯ x = do
    let x ← f ⟨i, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x

Tactic:
rw [dfoldlM_loop_lt _ h _]

Result:
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
inst✝ : Monad m
f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)
h : i < n + 1
x : α ⟨i, ⋯⟩
h' : i < n
⊢ f ⟨i, h⟩ x >>= dfoldlM.loop (n + 1) α f (i + 1) ⋯ = do
    let x ← f ⟨i, h⟩ x
    dfoldlM.loop n (α ∘ succ) (fun x1 x2 => f x1.succ x2) i h x