Theorem: Fin.foldAll_induction (Algdata/Data/Fin/Basic.lean)

State before:
n : Nat
α : Type u
motive : Nat → α → Prop
f : Fin n → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive n (foldAll f init)
Tactic:
induction n generalizing init with
| zero => exact h0
| succ n IH =>
  dsimp [foldAll]
  rw [Fin.foldAllM_succ' (m:=Id)]
  refine hf ⟨n,n.lt_succ_self⟩ _ ?_
  refine IH _ init h0 ?_
  intro i x H
  exact hf ⟨i.1, .step i.2⟩ x H
State after:
no goals

State before:
case zero
α : Type u
motive : Nat → α → Prop
f : Fin Nat.zero → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin Nat.zero) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive Nat.zero (foldAll f init)
Tactic:
exact h0
State after:
no goals

State before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (foldAll f init)
Tactic:
dsimp [foldAll]
State after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM f init))

State before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM f init))
Tactic:
rw [Fin.foldAllM_succ' (m:=Id)]
State after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM (f ∘ castSucc) init >>= f { val := n, isLt := (_ : n < Nat.succ n) }))

State before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM (f ∘ castSucc) init >>= f { val := n, isLt := (_ : n < Nat.succ n) }))
Tactic:
refine hf ⟨n,n.lt_succ_self⟩ _ ?_
State after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (↑{ val := n, isLt := (_ : n < Nat.succ n) }) (foldAllM (f ∘ castSucc) init)

State before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (↑{ val := n, isLt := (_ : n < Nat.succ n) }) (foldAllM (f ∘ castSucc) init)
Tactic:
refine IH _ init h0 ?_
State after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ ∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) ((f ∘ castSucc) i x)

State before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ ∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) ((f ∘ castSucc) i x)
Tactic:
intro i x H
State after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
i : Fin n
x : α
H : motive (↑i) x
⊢ motive (↑i + 1) ((f ∘ castSucc) i x)

State before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
i : Fin n
x : α
H : motive (↑i) x
⊢ motive (↑i + 1) ((f ∘ castSucc) i x)
Tactic:
exact hf ⟨i.1, .step i.2⟩ x H
State after:
no goals