Theorem: Fin.foldAllM_loop_succ' (Algdata/Data/Fin/Basic.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
k : Nat
h : i + (k + 1) = n + 1
⊢ foldAllM.loop f i a (k + 1) h =
    foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
induction k generalizing a i with
| zero => dsimp [Fin.foldAllM.loop]; cases h; simp only [pure_bind, bind_pure]
| succ k IH =>
  conv =>
    lhs; unfold Fin.foldAllM.loop; dsimp
    rhs; ext; rw [@IH (i+1) _ (i.succ_add (k+1) ▸ h)]
  simp only [← bind_assoc]
  rfl
State after:
no goals

State before:
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ foldAllM.loop f i a (Nat.zero + 1) h =
    foldAllM.loop (f ∘ castSucc) i a Nat.zero (_ : i + Nat.zero = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
dsimp [Fin.foldAllM.loop]
State after:
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }

State before:
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
cases h
State after:
case zero.refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
a : α
⊢ (do
      let __do_lift ← f { val := n, isLt := (_ : n < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }

State before:
case zero.refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
a : α
⊢ (do
      let __do_lift ← f { val := n, isLt := (_ : n < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
simp only [pure_bind, bind_pure]
State after:
no goals

State before:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ foldAllM.loop f i a (Nat.succ k + 1) h =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
conv =>
  lhs; unfold Fin.foldAllM.loop; dsimp
  rhs; ext; rw [@IH (i+1) _ (i.succ_add (k+1) ▸ h)]
State after:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (f { val := i, isLt := (_ : i < n + 1) } a >>= fun x =>
      foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }) =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }

State before:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (f { val := i, isLt := (_ : i < n + 1) } a >>= fun x =>
      foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }) =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
simp only [← bind_assoc]
State after:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
        let x ← f { val := i, isLt := (_ : i < n + 1) } a
        foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n)) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) } =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }

State before:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
        let x ← f { val := i, isLt := (_ : i < n + 1) } a
        foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n)) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) } =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
rfl
State after:
no goals