Theorem: Fin.foldAllM.loop_succ (Algdata/Data/Fin/Basic.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
k : Nat
h : i + (k + 1) = n + 1
⊢ loop f i a (k + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b k (_ : i + k = n)
Tactic:
induction k generalizing n f i a
State after:
case zero
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ loop f i a (Nat.zero + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b Nat.zero (_ : i + Nat.zero = n)

case succ
m : Type u → Type v
inst✝ : Monad m
α : Type u
n✝ : Nat
n_ih✝ :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (n✝ + 1) = n + 1},
    loop f i a (n✝ + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b n✝ (_ : i + n✝ = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ n✝ + 1) = n + 1
⊢ loop f i a (Nat.succ n✝ + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ n✝) (_ : i + Nat.succ n✝ = n)

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

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ loop f i a (Nat.succ k + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
case succ k h_ind =>
  conv =>
    lhs
    change do loop f i.succ (← f ⟨i, h ▸ Nat.lt_add_of_pos_right k.succ.zero_lt_succ⟩ a) k.succ (by rw [←h, Nat.add_succ, Nat.succ_add, Nat.add_succ]; rfl)
  apply bind_congr; intro b
  rw [h_ind]
  rfl
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ loop f i a (Nat.zero + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b Nat.zero (_ : i + Nat.zero = n)
Tactic:
rfl
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ loop f i a (Nat.succ k + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
conv =>
  lhs
  change do loop f i.succ (← f ⟨i, h ▸ Nat.lt_add_of_pos_right k.succ.zero_lt_succ⟩ a) k.succ (by rw [←h, Nat.add_succ, Nat.succ_add, Nat.add_succ]; rfl)
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      loop f (Nat.succ i) __do_lift (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1)) =
    do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      loop f (Nat.succ i) __do_lift (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1)) =
    do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
apply bind_congr
State after:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ ∀ (a : α),
    loop f (Nat.succ i) a (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1) =
      loop (f ∘ succ) i a (Nat.succ k) (_ : i + Nat.succ k = n)

State before:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ ∀ (a : α),
    loop f (Nat.succ i) a (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1) =
      loop (f ∘ succ) i a (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
intro b
State after:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
b : α
⊢ loop f (Nat.succ i) b (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1) =
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)

State before:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
b : α
⊢ loop f (Nat.succ i) b (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1) =
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
rw [h_ind]
State after:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
b : α
⊢ (do
      let b ← f { val := Nat.succ i, isLt := (_ : Nat.succ i < n + 1) } b
      loop (f ∘ succ) (Nat.succ i) b k (_ : Nat.succ i + k = n)) =
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)

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

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ Nat.succ i + Nat.succ k = n + 1
Tactic:
rw [←h, Nat.add_succ, Nat.succ_add, Nat.add_succ]
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ Nat.succ (Nat.succ (i + k)) = Nat.succ (i + (k + 1))

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