awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Tree.Traversable
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₂ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₃ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₄ :
  Eq (α := Id (Tree β)) (Tree.node <$> pure (f v) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₅ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v)) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₆ :
  Eq (α := Id (Tree β)) (Tree.node (f v) <$> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₇ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v) (map f l)) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₈ :
  Eq (α := Id (Tree β)) (Tree.node (f v) (map f l) <$> pure (map f r)) (pure (Tree.node (f v) (map f l) (map f r)))
node₉ node₁₀ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v) (map f l) (map f r))) (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))

Tactic:
rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]

Premises used: LawfulApplicative.pure_seq, Tree.map, Function.comp_apply, LawfulApplicative.map_pure, Tree.traverse
-- Module: Mathlib.Data.Tree.Traversable
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : Tree α
nil : Eq (α := Id (Tree β)) (traverse (pure ∘ f) Tree.nil) (pure (map f Tree.nil))
node :
  ∀ (v : α) (l r : Tree α) (hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l)))
    (hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))),
    Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) t) (pure (map f t))

Tactic:
induction t with
  | nil => rw [traverse, map]
  | node v l r hl hr =>
    rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]

Premises used: Tree.node, Tree.nil, LawfulApplicative.pure_seq, Tree.map, Function.comp_apply, LawfulApplicative.map_pure, Tree.traverse
-- Module: Mathlib.Data.Tree.Traversable
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 β
nil : (fun {α : Type u} ↦ η.app α) (pure Tree.nil) = traverse (η.app β ∘ f) Tree.nil
nil₁ : Eq.{u_4 + 1} (α := G (Tree β)) ((fun {α : Type u} ↦ η.app α) (pure Tree.nil)) (pure Tree.nil)
nil₂ nil₃ : Eq.{u_4 + 1} (α := G (Tree β)) (pure Tree.nil) (pure Tree.nil)
⊢ (fun {α : Type u} ↦ η.app α) (traverse f Tree.nil) = traverse (η.app β ∘ f) Tree.nil

Tactic:
rw [traverse, traverse, η.preserves_pure]

Premises used: ApplicativeTransformation.preserves_pure, Tree.traverse
-- Module: Mathlib.Data.Tree.Traversable
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
node₇ 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)

Tactic:
rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]

Premises used: ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_map, Function.comp_apply, Tree.traverse
-- Module: Mathlib.Data.Tree.Traversable
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
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 (Tree.node v l r)) = traverse (η.app β ∘ f) (Tree.node v l r)
⊢ (fun {α : Type u} ↦ η.app α) (traverse f t) = traverse (η.app β ∘ f) t

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]

Premises used: Tree.node, Tree.nil, ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_pure, ApplicativeTransformation.preserves_map, Function.comp_apply, Tree.traverse
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
p : TwoPointing α
⊢ p.snd ≠ p.fst

Tactic:
p.fst_ne_snd.symm

Premises used: Ne.symm, TwoPointing.fst_ne_snd
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
p : TwoPointing α
⊢ p.swap.fst = p.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
p : TwoPointing α
⊢ p.swap.snd = p.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
p : TwoPointing α
⊢ p.swap.swap = p

Tactic:
rfl

Premises used: TwoPointing.swap, rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
p : TwoPointing α
⊢ Nontrivial α

Tactic:
⟨⟨p.fst, p.snd, p.fst_ne_snd⟩⟩

Premises used: TwoPointing.fst_ne_snd, Nontrivial.mk, Prod.fst, Exists.intro, TwoPointing.toProd, Prod.snd
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
β : Type u_2
p : TwoPointing α
q : TwoPointing β
inst : Nontrivial α
⊢ Nonempty.{u_1 + 1} (TwoPointing α)

Tactic:
let ⟨a, b, h⟩ := exists_pair_ne α
  ⟨⟨(a, b), h⟩⟩

Premises used: TwoPointing.mk, Prod.mk, _private.0.TwoPointing.instNonemptyOfNontrivial.match_1, Nonempty.intro, TwoPointing, Nonempty, exists_pair_ne
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
⊢ Nonempty.{u_1 + 1} (TwoPointing α) ↔ Nontrivial α

Tactic:
⟨fun ⟨p⟩ ↦ p.to_nontrivial, fun _ => inferInstance⟩

Premises used: Nontrivial, inferInstance, _private.0.TwoPointing.nonempty_two_pointing_iff.match_1, TwoPointing.to_nontrivial, Iff.intro
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
β : Type u_2
q : TwoPointing β
inst : Nonempty α
⊢ (pi α q).fst = const α q.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
β : Type u_2
q : TwoPointing β
inst : Nonempty α
⊢ (pi α q).snd = const α q.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
β : Type u_2
p : TwoPointing α
q : TwoPointing β
⊢ (p.prod q).fst = (p.fst, q.fst)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
β : Type u_2
p : TwoPointing α
q : TwoPointing β
⊢ (p.prod q).snd = (p.snd, q.snd)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
β : Type u_2
p : TwoPointing α
q : TwoPointing β
⊢ (p.sum q).fst = Sum.inl p.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
α : Type u_1
β : Type u_2
p : TwoPointing α
q : TwoPointing β
⊢ (p.sum q).snd = Sum.inr q.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
⊢ TwoPointing.bool.fst = false

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
⊢ TwoPointing.bool.snd = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
⊢ TwoPointing.prop.fst = False

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TwoPointing
Goal:
⊢ TwoPointing.prop.snd = True

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
h h₁ : ∀ (i : Fin2 n), f i = g i
⊢ f = g

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
i : Fin2 n
⊢ f i = g i

Tactic:
apply h
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f : α ⟹ β
⊢ comp (α := α) (β := β) (γ := β) (id (α := β)) f = f

Tactic:
rfl

Premises used: TypeVec.comp, TypeVec.id, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f : α ⟹ β
⊢ comp (α := α) (β := α) (γ := β) f (id (α := α)) = f

Tactic:
rfl

Premises used: TypeVec.comp, TypeVec.id, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
γ : TypeVec.{w} n
δ : TypeVec.{x} n
h : γ ⟹ δ
g : β ⟹ γ
f : α ⟹ β
⊢ comp (α := α) (β := β) (γ := δ) (comp (α := β) (β := γ) (γ := δ) h g) f =
    comp (α := α) (β := γ) (γ := δ) h (comp (α := α) (β := β) (γ := γ) g f)

Tactic:
rfl

Premises used: TypeVec.comp, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
β : Type u_1
i : Fin2 n
⊢ (α ::: β).drop i = α i

Tactic:
rfl

Premises used: TypeVec.append1, TypeVec.drop, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
β : Type u_1
⊢ (α ::: β).drop = α

Tactic:
funext fun _ => drop_append1

Premises used: funext, TypeVec.drop_append1, TypeVec
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
β : Type u_1
⊢ (α ::: β).last = β

Tactic:
rfl

Premises used: TypeVec.last, TypeVec.append1, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 (n + 1)
fz : (α.drop ::: α.last) Fin2.fz = α Fin2.fz
fs : ∀ (a : Fin2 n), (α.drop ::: α.last) a.fs = α a.fs
⊢ (α.drop ::: α.last) i = α i

Tactic:
cases i
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ (α.drop ::: α.last) Fin2.fz = α Fin2.fz

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
a : Fin2 n
⊢ (α.drop ::: α.last) a.fs = α a.fs

Tactic:
rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
C : TypeVec.{u_1} (n + 1) → Sort u
H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)
γ : TypeVec.{u_1} (n + 1)
rw : C (γ.drop ::: γ.last)
⊢ C γ

Tactic:
rw [← @append1_drop_last _ γ]

Premises used: TypeVec.append1_drop_last
-- Module: Mathlib.Data.TypeVec
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 (γ.drop ::: γ.last)

Tactic:
apply H
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
C : TypeVec.{u_1} (n + 1) → Sort u
H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)
α : TypeVec.{u_1} n
β : Type u_1
⊢ append1Cases (C := C) H (α ::: β) = H α β

Tactic:
rfl

Premises used: Eq.mpr, TypeVec.last, TypeVec.append1, TypeVec.append1Cases, TypeVec.drop, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
i : Fin2 0
⊢ α i → β i

Tactic:
apply Fin2.elim0 i

Premises used: Fin2.elim0
-- Module: Mathlib.Data.TypeVec
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

Tactic:
funext (fun x => ?_)

Premises used: funext, TypeVec.Arrow
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun (α := α) (β := β) f = dropFun (α := α) (β := β) g
h₁ : lastFun (α := α) (β := β) f = lastFun (α := α) (β := β) g
refine : ∀ (x : Fin2 (n + 1)), f x = g x
⊢ f = g

Tactic:
refine funext (fun x => ?_)

Premises used: funext
-- Module: Mathlib.Data.TypeVec
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)
fs : ∀ (a : Fin2 n), Eq (α := α a.fs → β a.fs) (f a.fs) (g a.fs)
⊢ f x = g x

Tactic:
cases x
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun (α := α) (β := β) f = dropFun (α := α) (β := β) g
h₁ : lastFun (α := α) (β := β) f = lastFun (α := α) (β := β) g
⊢ Eq (α := α Fin2.fz → β Fin2.fz) (f Fin2.fz) (g Fin2.fz)

Tactic:
apply h₁
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun (α := α) (β := β) f = dropFun (α := α) (β := β) g
h₁ : lastFun (α := α) (β := β) f = lastFun (α := α) (β := β) g
a : Fin2 n
⊢ Eq (α := α a.fs → β a.fs) (f a.fs) (g a.fs)

Tactic:
apply congr_fun h₀

Premises used: congr_fun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f : Arrow.{u_1, u_2} α.drop α'.drop
g : α.last → α'.last
⊢ dropFun (α := α) (β := α') (splitFun (α := α) (α' := α') f g) = f

Tactic:
rfl

Premises used: TypeVec.splitFun, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f : Arrow.{u_1, u_2} α.drop α'.drop
g : α.last → α'.last
⊢ lastFun (α := α) (β := α') (splitFun (α := α) (α' := α') f g) = g

Tactic:
rfl

Premises used: TypeVec.lastFun, TypeVec.splitFun, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
α' : TypeVec.{u_2} n
β : Type u_1
β' : Type u_2
f : α ⟹ α'
g : β → β'
⊢ dropFun (α := α ::: β) (β := α' ::: β') (appendFun (α := α) (α' := α') f g) = f

Tactic:
rfl

Premises used: TypeVec.appendFun, TypeVec.splitFun, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
α' : TypeVec.{u_2} n
β : Type u_1
β' : Type u_2
f : α ⟹ α'
g : β → β'
⊢ lastFun (α := α ::: β) (β := α' ::: β') (appendFun (α := α) (α' := α') f g) = g

Tactic:
rfl

Premises used: TypeVec.lastFun, TypeVec.appendFun, TypeVec.splitFun, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f : α ⟹ α'
⊢ splitFun (α := α) (α' := α') (dropFun (α := α) (β := α') f) (lastFun (α := α) (β := α') f) = f

Tactic:
eq_of_drop_last_eq rfl rfl

Premises used: TypeVec.eq_of_drop_last_eq, rfl
-- Module: Mathlib.Data.TypeVec
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'
rw :
  dropFun (α := α) (β := α') (splitFun (α := α) (α' := α') f' g') = f' ∧
    lastFun (α := α) (β := α') (splitFun (α := α) (α' := α') f' g') = g'
⊢ f = f' ∧ g = g'

Tactic:
rw [← dropFun_splitFun f g, H, ← lastFun_splitFun f g, H]

Premises used: TypeVec.dropFun_splitFun, TypeVec.lastFun_splitFun
-- Module: Mathlib.Data.TypeVec
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'
⊢ dropFun (α := α) (β := α') (splitFun (α := α) (α' := α') f' g') = f' ∧
    lastFun (α := α) (β := α') (splitFun (α := α) (α' := α') f' g') = g'

Tactic:
simp
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
α' : TypeVec.{u_2} n
β : Type u_1
β' : Type u_2
f f' : α ⟹ α'
g g' : β → β'
⊢ appendFun (α := α) (α' := α') f g = appendFun (α := α) (α' := α') f' g' → f = f' ∧ g = g'

Tactic:
splitFun_inj

Premises used: TypeVec.last, TypeVec.append1, TypeVec.appendFun, TypeVec.drop, TypeVec.splitFun_inj
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α₀ : TypeVec.{u_1} (n + 1)
α₁ : TypeVec.{u_2} (n + 1)
α₂ : TypeVec.{u_3} (n + 1)
f₀ : Arrow.{u_1, u_2} α₀.drop α₁.drop
f₁ : Arrow.{u_2, u_3} α₁.drop α₂.drop
g₀ : α₀.last → α₁.last
g₁ : α₁.last → α₂.last
⊢ splitFun (α := α₀) (α' := α₂) (comp (α := α₀.drop) (β := α₁.drop) (γ := α₂.drop) f₁ f₀) (g₁ ∘ g₀) =
    comp (α := α₀) (β := α₁) (γ := α₂) (splitFun (α := α₁) (α' := α₂) f₁ g₁) (splitFun (α := α₀) (α' := α₁) f₀ g₀)

Tactic:
eq_of_drop_last_eq rfl rfl

Premises used: TypeVec.eq_of_drop_last_eq, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
γ : TypeVec.{u_2} n
β : Type u_1
δ : Type u_2
ε : TypeVec.{u_3} (n + 1)
f₀ : ε.drop ⟹ α
f₁ : α ⟹ γ
g₀ : ε.last → β
g₁ : β → δ
⊢ comp (α := ε) (β := α ::: β) (γ := γ ::: δ) (appendFun (α := α) (α' := γ) f₁ g₁)
      (splitFun (α := ε) (α' := α ::: β) f₀ g₀) =
    splitFun (α := ε) (α' := γ ::: δ) (comp (α := ε.drop) (β := α) (γ := (γ ::: δ).drop) f₁ f₀) (g₁ ∘ g₀)

Tactic:
(splitFun_comp _ _ _ _).symm

Premises used: TypeVec.append1, TypeVec.splitFun_comp, TypeVec.appendFun, Eq.symm, TypeVec.drop
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α₀ : TypeVec.{u_1} n
α₁ : TypeVec.{u_2} n
α₂ : TypeVec.{u_3} n
β₀ : Type u_1
β₁ : Type u_2
β₂ : Type u_3
f₀ : α₀ ⟹ α₁
f₁ : α₁ ⟹ α₂
g₀ : β₀ → β₁
g₁ : β₁ → β₂
⊢ appendFun (α := α₀) (α' := α₂) (comp (α := α₀) (β := α₁) (γ := α₂) f₁ f₀) (g₁ ∘ g₀) =
    comp (α := α₀ ::: β₀) (β := α₁ ::: β₁) (γ := α₂ ::: β₂) (appendFun (α := α₁) (α' := α₂) f₁ g₁)
      (appendFun (α := α₀) (α' := α₁) f₀ g₀)

Tactic:
eq_of_drop_last_eq rfl rfl

Premises used: TypeVec.eq_of_drop_last_eq, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α₀ : TypeVec.{u_1} n
α₁ : TypeVec.{u_2} n
α₂ : TypeVec.{u_3} n
β₀ : Type u_1
β₁ : Type u_2
β₂ : Type u_3
f₀ : α₀ ⟹ α₁
f₁ : α₁ ⟹ α₂
g₀ : β₀ → β₁
g₁ : β₁ → β₂
⊢ comp (α := α₀ ::: β₀) (β := α₁ ::: β₁) (γ := α₂ ::: β₂) (appendFun (α := α₁) (α' := α₂) f₁ g₁)
      (appendFun (α := α₀) (α' := α₁) f₀ g₀) =
    appendFun (α := α₀) (α' := α₂) (comp (α := α₀) (β := α₁) (γ := α₂) f₁ f₀) (g₁ ∘ g₀)

Tactic:
eq_of_drop_last_eq rfl rfl

Premises used: TypeVec.eq_of_drop_last_eq, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
α₀ : TypeVec.{u_1} 0
f₀ : Arrow.{u_1, u_2} α₀ (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2))
⊢ comp (α := α₀) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (γ :=
      Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2))
      (nilFun (α := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) (β := Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)))
      f₀ =
    f₀

Tactic:
funext Fin2.elim0

Premises used: Fin2.elim0, funext, TypeVec.Arrow
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u} n
β₀ β₁ β₂ : Type u
g₀ : β₀ → β₁
g₁ : β₁ → β₂
⊢ Eq (α := α ::: β₀ ⟹ α ::: β₂) (appendFun (α := α) (α' := α) (id (α := α)) (g₁ ∘ g₀))
    (comp (α := α ::: β₀) (β := α ::: β₁) (γ := α ::: β₂) (appendFun (α := α) (α' := α) (id (α := α)) g₁)
      (appendFun (α := α) (α' := α) (id (α := α)) g₀))

Tactic:
eq_of_drop_last_eq rfl rfl

Premises used: TypeVec.eq_of_drop_last_eq, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α₀ : TypeVec.{u_1} (n + 1)
α₁ : TypeVec.{u_2} (n + 1)
α₂ : TypeVec.{u_3} (n + 1)
f₀ : α₀ ⟹ α₁
f₁ : α₁ ⟹ α₂
⊢ dropFun (α := α₀) (β := α₂) (comp (α := α₀) (β := α₁) (γ := α₂) f₁ f₀) =
    comp (α := α₀.drop) (β := α₁.drop) (γ := α₂.drop) (dropFun (α := α₁) (β := α₂) f₁) (dropFun (α := α₀) (β := α₁) f₀)

Tactic:
rfl

Premises used: TypeVec.comp, TypeVec.drop, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α₀ : TypeVec.{u_1} (n + 1)
α₁ : TypeVec.{u_2} (n + 1)
α₂ : TypeVec.{u_3} (n + 1)
f₀ : α₀ ⟹ α₁
f₁ : α₁ ⟹ α₂
⊢ lastFun (α := α₀) (β := α₂) (comp (α := α₀) (β := α₁) (γ := α₂) f₁ f₀) =
    lastFun (α := α₁) (β := α₂) f₁ ∘ lastFun (α := α₀) (β := α₁) f₀

Tactic:
rfl

Premises used: TypeVec.last, TypeVec.comp, TypeVec.lastFun, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
α' : TypeVec.{u_2} n
β : Type u_1
β' : Type u_2
f : Arrow.{u_1, u_2} (α ::: β) (α' ::: β')
⊢ appendFun (α := (α ::: β).drop) (α' := (α' ::: β').drop) (dropFun (α := α ::: β) (β := α' ::: β') f)
      (lastFun (α := α ::: β) (β := α' ::: β') f) =
    f

Tactic:
eq_of_drop_last_eq rfl rfl

Premises used: TypeVec.eq_of_drop_last_eq, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
β : Type u_1
⊢ Eq.{u_1 + 1} (α := α ::: β ⟹ α ::: β) (appendFun (α := α) (α' := α) (id (α := α)) _root_.id) (id (α := α ::: β))

Tactic:
eq_of_drop_last_eq rfl rfl

Premises used: TypeVec.eq_of_drop_last_eq, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
⊢ Subsingleton.{u_1 + 2} (TypeVec.{u_1} 0)

Tactic:
⟨fun _ _ => funext Fin2.elim0⟩

Premises used: Fin2.elim0, funext, Subsingleton.intro
-- Module: Mathlib.Data.TypeVec
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
e_a : Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2) = v
⊢ β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) = β v

Tactic:
congr
-- Module: Mathlib.Data.TypeVec
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
e_a : ∀ (i : Fin2 0), i.elim0 (C := fun (a : Fin2 0) ↦ Type u_2) = v i
⊢ Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2) = v

Tactic:
funext i
-- Module: Mathlib.Data.TypeVec
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
i : Fin2 0
⊢ i.elim0 (C := fun (a : Fin2 0) ↦ Type u_2) = v i

Tactic:
cases i
-- Module: Mathlib.Data.TypeVec
Goal:
n_1 n : ℕ
β : TypeVec.{u_2} (n + 1) → Sort u_1
f : (t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t)
v : TypeVec.{u_2} (n + 1)
⊢ β (v.drop ::: v.last) = β v

Tactic:
simp
-- Module: Mathlib.Data.TypeVec
Goal:
β : TypeVec.{u_2} 0 → Sort u_1
f : β (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2))
⊢ TypeVec.casesNil (β := β) f (Fin2.elim0 (C := fun (a : Fin2 0) ↦ Type u_2)) = f

Tactic:
rfl

Premises used: cast, TypeVec.casesNil, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
β : TypeVec.{u_2} (n + 1) → Sort u_1
f : (t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t)
v : TypeVec.{u_2} n
α : Type u_2
⊢ TypeVec.casesCons n (β := β) f (v ::: α) = f α v

Tactic:
rfl

Premises used: TypeVec.last, cast, TypeVec.append1, TypeVec.casesCons, TypeVec.drop, rfl