Theorem: Nat.dfold_hom (Fifteen/Data/Nat/Basic.lean)

State before:
α : Nat → Sort u
β : Nat → Sort v
f : (n : Nat) → α n → β n
g₁ : (n : Nat) → α n → α (n + 1)
g₂ : (n : Nat) → β n → β (n + 1)
n : Nat
init : α 0
H : ∀ (n : Nat) (a : α n), g₂ n (f n a) = f (n + 1) (g₁ n a)
⊢ dfold g₂ n (f 0 init) = f n (dfold g₁ n init)
Tactic:
induction n with
| zero => rfl
| succ n IH => dsimp [dfold]; rw [IH, H]
State after:
no goals

State before:
case zero
α : Nat → Sort u
β : Nat → Sort v
f : (n : Nat) → α n → β n
g₁ : (n : Nat) → α n → α (n + 1)
g₂ : (n : Nat) → β n → β (n + 1)
init : α 0
H : ∀ (n : Nat) (a : α n), g₂ n (f n a) = f (n + 1) (g₁ n a)
⊢ dfold g₂ zero (f 0 init) = f zero (dfold g₁ zero init)
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Nat → Sort u
β : Nat → Sort v
f : (n : Nat) → α n → β n
g₁ : (n : Nat) → α n → α (n + 1)
g₂ : (n : Nat) → β n → β (n + 1)
init : α 0
H : ∀ (n : Nat) (a : α n), g₂ n (f n a) = f (n + 1) (g₁ n a)
n : Nat
IH : dfold g₂ n (f 0 init) = f n (dfold g₁ n init)
⊢ dfold g₂ (succ n) (f 0 init) = f (succ n) (dfold g₁ (succ n) init)
Tactic:
dsimp [dfold]
State after:
case succ
α : Nat → Sort u
β : Nat → Sort v
f : (n : Nat) → α n → β n
g₁ : (n : Nat) → α n → α (n + 1)
g₂ : (n : Nat) → β n → β (n + 1)
init : α 0
H : ∀ (n : Nat) (a : α n), g₂ n (f n a) = f (n + 1) (g₁ n a)
n : Nat
IH : dfold g₂ n (f 0 init) = f n (dfold g₁ n init)
⊢ g₂ n (dfold g₂ n (f 0 init)) = f (succ n) (g₁ n (dfold g₁ n init))

State before:
case succ
α : Nat → Sort u
β : Nat → Sort v
f : (n : Nat) → α n → β n
g₁ : (n : Nat) → α n → α (n + 1)
g₂ : (n : Nat) → β n → β (n + 1)
init : α 0
H : ∀ (n : Nat) (a : α n), g₂ n (f n a) = f (n + 1) (g₁ n a)
n : Nat
IH : dfold g₂ n (f 0 init) = f n (dfold g₁ n init)
⊢ g₂ n (dfold g₂ n (f 0 init)) = f (succ n) (g₁ n (dfold g₁ n init))
Tactic:
rw [IH, H]
State after:
no goals