Theorem: Nat.fold'_hom (Fifteen/Data/Nat/Basic.lean)

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
⊢ fold' n g₂ (f init) = f (fold' n g₁ init)
Tactic:
dsimp [fold']
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
let α' : Nat → Type u := fun i => i ≤ n → α
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
let β' : Nat → Type v := fun i => i ≤ n → β
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
let f' : (i : Nat) → α' i → β' i :=
  fun i ha hi => f (ha hi)
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
let g₁' : (i : Nat) → α' i → α' (i+1) :=
  fun i x hi => g₁ ⟨i,hi⟩ (x <| Nat.le_of_lt hi)
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
let g₂' : (i : Nat) → β' i → β' (i+1) :=
  fun i y hi => g₂ ⟨i,hi⟩ (y <| Nat.le_of_lt hi)
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
let init' : α' 0 := fun _ => init
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
suffices ∀ (k : Nat), dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init') by
  rw [this n]
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
⊢ ∀ (k : Nat), dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
⊢ ∀ (k : Nat), dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')
Tactic:
intro k
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k : Nat
⊢ dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k : Nat
⊢ dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')
Tactic:
refine dfold_hom f' g₁' g₂' k init' ?_
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k : Nat
⊢ ∀ (n : Nat) (a : α' n), g₂' n (f' n a) = f' (n + 1) (g₁' n a)

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k : Nat
⊢ ∀ (n : Nat) (a : α' n), g₂' n (f' n a) = f' (n + 1) (g₁' n a)
Tactic:
intro i x
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ g₂' i (f' i x) = f' (i + 1) (g₁' i x)

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ g₂' i (f' i x) = f' (i + 1) (g₁' i x)
Tactic:
dsimp
State after:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ (fun hi => g₂ { val := i, isLt := hi } (f (x (_ : i ≤ n)))) = fun hi =>
    f (g₁ { val := i, isLt := hi } (x (_ : i ≤ n)))

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ (fun hi => g₂ { val := i, isLt := hi } (f (x (_ : i ≤ n)))) = fun hi =>
    f (g₁ { val := i, isLt := hi } (x (_ : i ≤ n)))
Tactic:
simp only [H]
State after:
no goals

State before:
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
this : ∀ (k : Nat), dfold g₂' k (f' 0 init') = f' k (dfold g₁' k init')
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
rw [this n]
State after:
no goals