internlm/Lean-Github huggingface dataset:
Theorem: Nat.dfold_congr
Proof state before:
case succ
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a : α 0
b : β 0
hab : HEq a b
n : Nat
IH : ∃ a b, HEq a b
⊢ ∃ a b, HEq a b
Tactic:
let ⟨a,b,hab⟩ := IH
Proof state after:
case succ
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a✝ : α 0
b✝ : β 0
hab✝ : HEq a✝ b✝
n : Nat
IH : ∃ a b, HEq a b
a : α n
b : β n
hab : HEq a b
⊢ ∃ a b, HEq a b
Theorem: Nat.dfold_congr
Proof state before:
case succ
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a✝ : α 0
b✝ : β 0
hab✝ : HEq a✝ b✝
n : Nat
IH : ∃ a b, HEq a b
a : α n
b : β n
hab : HEq a b
⊢ ∃ a b, HEq a b
Tactic:
exact ⟨f n a, g n b, hfg n a b hab⟩
Proof state after:
no goals
Theorem: Nat.dfold_congr
Proof state before:
case refl.refl.zero
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
⊢ dfold f zero a = dfold g zero a
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.dfold_congr
Proof state before:
case refl.refl.succ
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
n : Nat
IH : dfold f n a = dfold g n a
⊢ dfold f (succ n) a = dfold g (succ n) a
Tactic:
dsimp [dfold]
Proof state after:
case refl.refl.succ
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
n : Nat
IH : dfold f n a = dfold g n a
⊢ f n (dfold f n a) = g n (dfold g n a)
Theorem: Nat.dfold_congr
Proof state before:
case refl.refl.succ
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
n : Nat
IH : dfold f n a = dfold g n a
⊢ f n (dfold f n a) = g n (dfold g n a)
Tactic:
exact hfg n _ _ IH
Proof state after:
no goals
Theorem: Nat.dfold_hom
Proof 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]
Proof state after:
no goals
Theorem: Nat.dfold_hom
Proof 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
Proof state after:
no goals
Theorem: Nat.dfold_hom
Proof 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]
Proof 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))
Theorem: Nat.dfold_hom
Proof 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]
Proof state after:
no goals
Theorem: Nat.fold'_congr
Proof state before:
α : Type u
m n : Nat
h : m = n
f : Fin m → α → α
g : Fin n → α → α
hf : ∀ (i : Fin m) (j : Fin n) (a : α), i.val = j.val → f i a = g j a
init : α
⊢ fold' m f init = fold' n g init
Tactic:
cases h
Proof state after:
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
⊢ fold' m f init = fold' m g init
Theorem: Nat.fold'_congr
Proof state before:
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
⊢ fold' m f init = fold' m g init
Tactic:
have : f = g := funext fun i => funext fun a =>
  hf i i a rfl
Proof state after:
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
this : f = g
⊢ fold' m f init = fold' m g init
Theorem: Nat.fold'_congr
Proof state before:
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
this : f = g
⊢ fold' m f init = fold' m g init
Tactic:
cases this
Proof state after:
case refl.refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = f j a
⊢ fold' m f init = fold' m f init
Theorem: Nat.fold'_congr
Proof state before:
case refl.refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = f j a
⊢ fold' m f init = fold' m f init
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.fold'_succ
Proof state before:
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ fold' (n + 1) f init = f (Fin.last n) (fold' n (f ∘ Fin.castSucc) init)
Tactic:
dsimp [fold', dfold]
Proof state after:
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ f { val := n, isLt := (_ : Nat.le (n + 1) (n + 1)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1)) =
    f (Fin.last n)
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init)
        (_ : Nat.le n n))
Theorem: Nat.fold'_succ
Proof state before:
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ f { val := n, isLt := (_ : Nat.le (n + 1) (n + 1)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1)) =
    f (Fin.last n)
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init)
        (_ : Nat.le n n))
Tactic:
apply congrArg
Proof state after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Theorem: Nat.fold'_succ
Proof state before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Tactic:
let mot₁ : Nat → Type u := fun i => i ≤ n+1 → α
Proof state after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Theorem: Nat.fold'_succ
Proof state before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Tactic:
let mot₂ : Nat → Type u := fun i => i ≤ n → α
Proof state after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Theorem: Nat.fold'_succ
Proof state before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n)
Tactic:
suffices ∀ (k : Nat) (hk : k ≤ n), dfold (α:=mot₁) _ k (fun _ => init) (.step hk) = dfold (α:=mot₂) _ k (fun _ => init) hk
from this n .refl
Proof state after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
⊢ ∀ (k : Nat) (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
Theorem: Nat.fold'_succ
Proof state before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
⊢ ∀ (k : Nat) (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
Tactic:
intro k hk
Proof state after:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
hk : k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
Theorem: Nat.fold'_succ
Proof state before:
case h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
hk : k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
Tactic:
induction k with
| zero => rfl
| succ k IH =>
  dsimp [dfold]; apply congrArg
  exact IH (Nat.le_of_succ_le hk)
Proof state after:
no goals
Theorem: Nat.fold'_succ
Proof state before:
case h.zero
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
hk : zero ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) zero (fun x => init) (_ : Nat.le zero (succ n)) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) zero (fun x => init) hk
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.fold'_succ
Proof state before:
case h.succ
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) (succ k) (fun x => init)
      (_ : Nat.le (succ k) (succ n)) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) (succ k) (fun x => init) hk
Tactic:
dsimp [dfold]
Proof state after:
case h.succ
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ f { val := k, isLt := (_ : Nat.le (succ k) (succ n)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1)) =
    f (Fin.castSucc { val := k, isLt := hk })
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n))
Theorem: Nat.fold'_succ
Proof state before:
case h.succ
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ f { val := k, isLt := (_ : Nat.le (succ k) (succ n)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1)) =
    f (Fin.castSucc { val := k, isLt := hk })
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n))
Tactic:
apply congrArg
Proof state after:
case h.succ.h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n)
Theorem: Nat.fold'_succ
Proof state before:
case h.succ.h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n)
Tactic:
exact IH (Nat.le_of_succ_le hk)
Proof state after:
no goals
Theorem: Nat.fold'_induction
Proof state before:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (fold' n f init)
Tactic:
dsimp [fold', dfold]
Proof state after:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Theorem: Nat.fold'_induction
Proof state before:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
Tactic:
refine dfold_induction (α := fun i => i ≤ n → α) (motive := fun i a => (h : i ≤ n) → motive i (a h)) _ n (fun _ => init) (fun _ => zero) ?_ .refl
Proof state after:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ ∀ (n_1 : Nat) (a : (fun i => i ≤ n → α) n_1),
    (fun i a => ∀ (h : i ≤ n), motive i (a h)) n_1 a →
      (fun i a => ∀ (h : i ≤ n), motive i (a h)) (n_1 + 1) fun hi => f { val := n_1, isLt := hi } (a (_ : n_1 ≤ n))
Theorem: Nat.fold'_induction
Proof state before:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ ∀ (n_1 : Nat) (a : (fun i => i ≤ n → α) n_1),
    (fun i a => ∀ (h : i ≤ n), motive i (a h)) n_1 a →
      (fun i a => ∀ (h : i ≤ n), motive i (a h)) (n_1 + 1) fun hi => f { val := n_1, isLt := hi } (a (_ : n_1 ≤ n))
Tactic:
intro i a IH hi
Proof state after:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
i : Nat
a : i ≤ n → α
IH : ∀ (h : i ≤ n), motive i (a h)
hi : i + 1 ≤ n
⊢ motive (i + 1) (f { val := i, isLt := hi } (a (_ : i ≤ n)))
Theorem: Nat.fold'_induction
Proof state before:
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
i : Nat
a : i ≤ n → α
IH : ∀ (h : i ≤ n), motive i (a h)
hi : i + 1 ≤ n
⊢ motive (i + 1) (f { val := i, isLt := hi } (a (_ : i ≤ n)))
Tactic:
exact succ i hi _ (IH _)
Proof state after:
no goals
Theorem: Nat.fold'_hom
Proof 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']
Proof 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))
Theorem: Nat.fold'_hom
Proof 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 → α
Proof 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))
Theorem: Nat.fold'_hom
Proof 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 → β
Proof 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))
Theorem: Nat.fold'_hom
Proof 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)
Proof 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))
Theorem: Nat.fold'_hom
Proof 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)
Proof 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))
Theorem: Nat.fold'_hom
Proof 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)
Proof 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))