Theorem: Nat.fold_hom (Algdata/Init/Nat.lean)

State before:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
⊢ fold g₂ (succ n) (f init) = f (fold g₁ (succ n) init)
Tactic:
dsimp [Nat.fold]
State after:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
⊢ g₂ n (fold g₂ n (f init)) = f (g₁ n (fold g₁ n init))

State before:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
⊢ g₂ n (fold g₂ n (f init)) = f (g₁ n (fold g₁ n init))
Tactic:
have IH := IH λ i a h => hf i a (trans h n.lt_succ_self)
State after:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH✝ : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
IH : fold g₂ n (f init) = f (fold g₁ n init)
⊢ g₂ n (fold g₂ n (f init)) = f (g₁ n (fold g₁ n init))

State before:
α : Type u
β : Type v
f : α → β
g₁ : Nat → α → α
g₂ : Nat → β → β
n✝ : Nat
init : α
hf✝ : ∀ (i : Nat) (a : α), i < n✝ → g₂ i (f a) = f (g₁ i a)
n : Nat
IH✝ : (∀ (i : Nat) (a : α), i < n → g₂ i (f a) = f (g₁ i a)) → fold g₂ n (f init) = f (fold g₁ n init)
hf : ∀ (i : Nat) (a : α), i < succ n → g₂ i (f a) = f (g₁ i a)
IH : fold g₂ n (f init) = f (fold g₁ n init)
⊢ g₂ n (fold g₂ n (f init)) = f (g₁ n (fold g₁ n init))
Tactic:
rw [IH, hf n _ n.lt_succ_self]
State after:
no goals