-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldrM_loop [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc))
    (x) : dfoldrM.loop (n+1) α f (i+1) h x =
      dfoldrM.loop n (α ∘ succ) (f ·.succ) i (by omega) x >>= f 0

Proof state:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
h : 0 + 1 < n + 1 + 1
x : α ⟨0 + 1, h⟩
⊢ f ⟨0, ⋯⟩ x >>= dfoldrM.loop (n + 1) α f 0 ⋯ = f 0 x >>= pure

Tactic:
rfl

Result:
no goals

Proof state:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
h : 0 + 1 < n + 1 + 1
x : α ⟨0 + 1, h⟩
⊢ dfoldrM.loop (n + 1) α f (0 + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) 0 ⋯ x >>= f 0

Tactic:
rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind]

Result:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
h : 0 + 1 < n + 1 + 1
x : α ⟨0 + 1, h⟩
⊢ f ⟨0, ⋯⟩ x >>= dfoldrM.loop (n + 1) α f 0 ⋯ = f 0 x

Proof state:
case succ.e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
i : Nat
ih :
  ∀ {h : i + 1 < n + 1 + 1} (x : α ⟨i + 1, h⟩),
    dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0
h : i + 1 + 1 < n + 1 + 1
x : α ⟨i + 1 + 1, h⟩
x✝ : α ⟨i + 1, ⋯⟩
⊢ dfoldrM.loop (n + 1) α f (i + 1) ⋯ x✝ = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x✝ >>= f 0

Tactic:
exact ih ..

Result:
no goals

Proof state:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
h : 0 + 1 < n + 1 + 1
x : α ⟨0 + 1, h⟩
⊢ f ⟨0, ⋯⟩ x >>= dfoldrM.loop (n + 1) α f 0 ⋯ = f 0 x

Tactic:
conv => rhs; rw [← bind_pure (f 0 x)]

Result:
case zero
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
h : 0 + 1 < n + 1 + 1
x : α ⟨0 + 1, h⟩
⊢ f ⟨0, ⋯⟩ x >>= dfoldrM.loop (n + 1) α f 0 ⋯ = f 0 x >>= pure

Proof state:
case succ.e_a
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
i : Nat
ih :
  ∀ {h : i + 1 < n + 1 + 1} (x : α ⟨i + 1, h⟩),
    dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0
h : i + 1 + 1 < n + 1 + 1
x : α ⟨i + 1 + 1, h⟩
⊢ dfoldrM.loop (n + 1) α f (i + 1) ⋯ = fun x => dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0

Tactic:
funext

Result:
case succ.e_a.h
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
i : Nat
ih :
  ∀ {h : i + 1 < n + 1 + 1} (x : α ⟨i + 1, h⟩),
    dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0
h : i + 1 + 1 < n + 1 + 1
x : α ⟨i + 1 + 1, h⟩
x✝ : α ⟨i + 1, ⋯⟩
⊢ dfoldrM.loop (n + 1) α f (i + 1) ⋯ x✝ = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x✝ >>= f 0

Proof state:
case succ
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
i : Nat
ih :
  ∀ {h : i + 1 < n + 1 + 1} (x : α ⟨i + 1, h⟩),
    dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0
h : i + 1 + 1 < n + 1 + 1
x : α ⟨i + 1 + 1, h⟩
⊢ f ⟨i + 1, ⋯⟩ x >>= dfoldrM.loop (n + 1) α f (i + 1) ⋯ =
    f ⟨i, ⋯⟩.succ x >>= fun x => dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0

Tactic:
congr

Result:
case succ.e_a
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
i : Nat
ih :
  ∀ {h : i + 1 < n + 1 + 1} (x : α ⟨i + 1, h⟩),
    dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0
h : i + 1 + 1 < n + 1 + 1
x : α ⟨i + 1 + 1, h⟩
⊢ dfoldrM.loop (n + 1) α f (i + 1) ⋯ = fun x => dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
i : Nat
h : i + 1 < n + 1 + 1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
x : α ⟨i + 1, h⟩
⊢ dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0

Tactic:
induction i with
| zero =>
  rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind]
  conv => rhs; rw [← bind_pure (f 0 x)]
  rfl
| succ i ih =>
  rw [dfoldrM_loop_succ, dfoldrM_loop_succ, bind_assoc]
  congr; funext; exact ih ..

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
i : Nat
ih :
  ∀ {h : i + 1 < n + 1 + 1} (x : α ⟨i + 1, h⟩),
    dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0
h : i + 1 + 1 < n + 1 + 1
x : α ⟨i + 1 + 1, h⟩
⊢ dfoldrM.loop (n + 1) α f (i + 1 + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) (i + 1) ⋯ x >>= f 0

Tactic:
rw [dfoldrM_loop_succ, dfoldrM_loop_succ, bind_assoc]

Result:
case succ
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1 + 1) → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
i : Nat
ih :
  ∀ {h : i + 1 < n + 1 + 1} (x : α ⟨i + 1, h⟩),
    dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0
h : i + 1 + 1 < n + 1 + 1
x : α ⟨i + 1 + 1, h⟩
⊢ f ⟨i + 1, ⋯⟩ x >>= dfoldrM.loop (n + 1) α f (i + 1) ⋯ =
    f ⟨i, ⋯⟩.succ x >>= fun x => dfoldrM.loop n (α ∘ succ) (fun x => f x.succ) i ⋯ x >>= f 0

Proof state:
m : Type ?u.2205 → Type ?u.2135
n : Nat
α : Fin (n + 1 + 1) → Type ?u.2205
i : Nat
h : i + 1 < n + 1 + 1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)
x : α ⟨i + 1, h⟩
⊢ i < n + 1

Tactic:
omega

Result:
no goals