awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
node :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    traverse (η.app β ∘ f) (Tree.node v l r)
node₁ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
⊢ (fun {α : Type u} ↦ η.app α) (traverse f (Tree.node v l r)) = traverse (η.app β ∘ f) (Tree.node v l r)
have node₂ : (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l) <*> (fun {α : Type u} ↦ η.app α) (traverse f r) =
  Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Tactic: rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
node :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    traverse (η.app β ∘ f) (Tree.node v l r)
node₁ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₂ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l) <*> (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
⊢ (fun {α : Type u} ↦ η.app α) (traverse f (Tree.node v l r)) = traverse (η.app β ∘ f) (Tree.node v l r)
have node₃ : (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
    (fun {α : Type u} ↦ η.app α) (traverse f r) =
  Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Tactic: rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
node :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    traverse (η.app β ∘ f) (Tree.node v l r)
node₁ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₂ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l) <*> (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₃ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
⊢ (fun {α : Type u} ↦ η.app α) (traverse f (Tree.node v l r)) = traverse (η.app β ∘ f) (Tree.node v l r)
have node₄ : Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
    (fun {α : Type u} ↦ η.app α) (traverse f r) =
  Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Tactic: rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
node :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    traverse (η.app β ∘ f) (Tree.node v l r)
node₁ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₂ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l) <*> (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₃ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₄ :
  Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
⊢ (fun {α : Type u} ↦ η.app α) (traverse f (Tree.node v l r)) = traverse (η.app β ∘ f) (Tree.node v l r)
have node₅ : Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*>
    (fun {α : Type u} ↦ η.app α) (traverse f r) =
  Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Tactic: rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
node :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    traverse (η.app β ∘ f) (Tree.node v l r)
node₁ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₂ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l) <*> (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₃ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₄ :
  Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₅ :
  Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
⊢ (fun {α : Type u} ↦ η.app α) (traverse f (Tree.node v l r)) = traverse (η.app β ∘ f) (Tree.node v l r)
have node₆ : Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r =
  Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Tactic: rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
node :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    traverse (η.app β ∘ f) (Tree.node v l r)
node₁ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₂ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l) <*> (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₃ :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₄ :
  Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> (fun {α : Type u} ↦ η.app α) (traverse f l) <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₅ :
  Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*>
      (fun {α : Type u} ↦ η.app α) (traverse f r) =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
node₆ :
  Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r =
    Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
⊢ (fun {α : Type u} ↦ η.app α) (traverse f (Tree.node v l r)) = traverse (η.app β ∘ f) (Tree.node v l r)
have node₇ : Tree.node <$> (fun {α : Type u} ↦ η.app α) (f v) <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r =
  Tree.node <$> η.app β (f v) <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Tactic: rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
t : Tree α
⊢ (fun {α : Type u} ↦ η.app α) (traverse f t) = traverse (η.app β ∘ f) t
have nil : (fun {α : Type u} ↦ η.app α) (traverse f nil) = traverse (η.app β ∘ f) nil
Tactic: induction t with
  | nil => rw [traverse, traverse, η.preserves_pure]
  | node v l r hl hr =>
    rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
t : Tree α
nil : (fun {α : Type u} ↦ η.app α) (traverse f Tree.nil) = traverse (η.app β ∘ f) Tree.nil
⊢ (fun {α : Type u} ↦ η.app α) (traverse f t) = traverse (η.app β ∘ f) t
have node : ∀ (v : α) (l r : Tree α) (hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l)
  (hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r),
  (fun {α : Type u} ↦ η.app α) (traverse f (node v l r)) = traverse (η.app β ∘ f) (node v l r)
Tactic: induction t with
  | nil => rw [traverse, traverse, η.preserves_pure]
  | node v l r hl hr =>
    rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 (n + 1)
⊢ (α.drop ::: α.last) i = α i
have fz : (α.drop ::: α.last) Fin2.fz = α Fin2.fz
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 (n + 1)
fz : (α.drop ::: α.last) Fin2.fz = α Fin2.fz
⊢ (α.drop ::: α.last) i = α i
have fs : ∀ (a : Fin2 n), (α.drop ::: α.last) a.fs = α a.fs
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
C : TypeVec.{u_1} (n + 1) → Sort u
H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)
γ : TypeVec.{u_1} (n + 1)
⊢ C γ
have rw : C (γ.drop ::: γ.last)
Tactic: rw [← @append1_drop_last _ γ]
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun (α := α) (β := β) f = dropFun (α := α) (β := β) g
h₁ : lastFun (α := α) (β := β) f = lastFun (α := α) (β := β) g
⊢ f = g
have refine : ∀ (x : Fin2 (n + 1)), f x = g x
Tactic: refine funext (fun x => ?_)
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun (α := α) (β := β) f = dropFun (α := α) (β := β) g
h₁ : lastFun (α := α) (β := β) f = lastFun (α := α) (β := β) g
x : Fin2 (n + 1)
⊢ f x = g x
have fz : Eq (α := α Fin2.fz → β Fin2.fz) (f Fin2.fz) (g Fin2.fz)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun (α := α) (β := β) f = dropFun (α := α) (β := β) g
h₁ : lastFun (α := α) (β := β) f = lastFun (α := α) (β := β) g
x : Fin2 (n + 1)
fz : Eq (α := α Fin2.fz → β Fin2.fz) (f Fin2.fz) (g Fin2.fz)
⊢ f x = g x
have fs : ∀ (a : Fin2 n), Eq (α := α a.fs → β a.fs) (f a.fs) (g a.fs)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : Arrow.{u_1, u_2} α.drop α'.drop
g g' : α.last → α'.last
H : splitFun (α := α) (α' := α') f g = splitFun (α := α) (α' := α') f' g'
⊢ f = f' ∧ g = g'
have rw : dropFun (α := α) (β := α') (splitFun (α := α) (α' := α') f' g') = f' ∧
  lastFun (α := α) (β := α') (splitFun (α := α) (α' := α') f' g') = g'
Tactic: rw [← dropFun_splitFun f g, H, ← lastFun_splitFun f g, H]
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
β : TypeVec.{u_2} 0 → Sort u_1
f : β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2))
v : TypeVec.{u_2} 0
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) = β v
have e_a : Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2) = v
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
β : TypeVec.{u_2} 0 → Sort u_1
f : β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2))
v : TypeVec.{u_2} 0
⊢ Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2) = v
have e_a : ∀ (i : Fin2 0), i.elim0 (C := fun (a : Fin2 0) ↦ Type u_2) = v i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
⊢ β v v' fs
have refine : β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
  β v v' fs
Tactic: refine cast ?_ f
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
⊢ v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
have h : ∀ (i : Fin2 0), v i = i.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (hypothesis)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β v v' fs
have eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
Tactic: have eq₁ : v = Fin2.elim0 := by funext i; contradiction
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
⊢ v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
have h : ∀ (i : Fin2 0), v' i = i.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (hypothesis)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β v v' fs
have eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
Tactic: have eq₂ : v' = Fin2.elim0 := by funext i; contradiction
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
⊢ fs = nilFun (α := v) (β := v')
have h : ∀ (i : Fin2 0), fs i = nilFun (α := v) (β := v') i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.TypeVec (hypothesis)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β v v' fs
have eq₃ : fs = nilFun (α := v) (β := v')
Tactic: have eq₃ : fs = nilFun := by funext i; contradiction
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v : TypeVec.{u_2} 0
v' : TypeVec.{u_3} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
eq₃ : fs = nilFun (α := v) (β := v')
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β v v' fs
have refl : ∀ (fs : Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) v')
  (eq₃ : fs = nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β := v')),
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) v' fs
Tactic: cases eq₁
Cleared hypotheses: v, fs, eq₁, eq₃
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v ⟹ v' → Sort u_1
f :
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
    (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3)))
v' : TypeVec.{u_3} 0
eq₂ : v' = Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)
fs : Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) v'
eq₃ : fs = nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β := v')
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) v' fs
have refl : ∀
  (fs :
    Arrow.{u_2, u_3} (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)))
  (eq₃ :
    fs =
      nilFun (α := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3))),
  β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β :=
        Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_3))) =
    β (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_2)) (Fin2.elim0 (C := fun (i : Fin2 0) ↦ Type u_3)) fs
Tactic: cases eq₂
Cleared hypotheses: v', eq₂, fs, eq₃