awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
dsimp :
  (∃ (u :
      F fun (i : Fin2 (n + 1)) ↦
        { p : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
            { p : (α ::: β) i × (α ::: β) i //
              ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) })
            (β := α ::: β)
            (fun (i : Fin2 (n + 1))
                (t :
                  { p : (α ::: β) i × (α ::: β) i //
                    ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ↦
              (↑t : (α ::: β) i × (α ::: β) i).1)
            u =
          x ∧
        map (F := F) (α := fun (i : Fin2 (n + 1)) ↦
            { p : (α ::: β) i × (α ::: β) i //
              ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) })
            (β := α ::: β)
            (fun (i : Fin2 (n + 1))
                (t :
                  { p : (α ::: β) i × (α ::: β) i //
                    ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ↦
              (↑t : (α ::: β) i × (α ::: β) i).2)
            u =
          y) ↔
    ∃ (u : F fun (i : Fin2 (n + 1)) ↦ { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }) (β :=
            α ::: β)
            (fun (i : Fin2 (n + 1)) (t : { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }) ↦
              (↑t : (α ::: β) i × (α ::: β) i).1)
            u =
          x ∧
        map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }) (β :=
            α ::: β)
            (fun (i : Fin2 (n + 1)) (t : { p : (α ::: β) i × (α ::: β) i // α.RelLast rr p.1 p.2 }) ↦
              (↑t : (α ::: β) i × (α ::: β) i).2)
            u =
          y
⊢ LiftR' (α := α ::: β) (F := F) (α.RelLast' rr) x y ↔ LiftR (F := F) (α := α ::: β) (α.RelLast rr) x y

Tactic:
dsimp only [LiftR, LiftR']

Premises used: MvFunctor.LiftR, MvFunctor.LiftR'
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
h₀ :
  ∀ (i : Fin2 (n + 1)) (x : (α ::: β) i × (α ::: β) i) (property : α.RelLast rr x.1 x.2),
    comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (β :=
        fun (i : Fin2 (n + 1)) ↦
        { p_1 : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
        (γ := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
        (g' rr n α) i (Subtype.mk (p := fun (p_1 : (α ::: β) i × (α ::: β) i) ↦ α.RelLast rr p_1.1 p_1.2) x property) =
      TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) i
        (Subtype.mk (p := fun (p_1 : (α ::: β) i × (α ::: β) i) ↦ α.RelLast rr p_1.1 p_1.2) x property)
⊢ comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (β :=
      fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i × (α ::: β) i //
        ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
      (γ := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
      (g' rr n α) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 })

Tactic:
ext i ⟨x, _⟩ : 2
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property : α.RelLast rr x.1 x.2
h₀ :
  ∀ (x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) (property : α.RelLast rr x.1 x.2),
    comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (β :=
        fun (i : Fin2 (n + 1)) ↦
        { p_1 : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
        (γ := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
        (g' rr n α) Fin2.fz
        (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦ α.RelLast rr p_1.1 p_1.2) x property) =
      TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) Fin2.fz
        (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦ α.RelLast rr p_1.1 p_1.2) x property)
h₁ :
  ∀ (a : Fin2 n) (x : (α ::: β) a.fs × (α ::: β) a.fs) (property : α.RelLast rr x.1 x.2),
    comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (β :=
        fun (i : Fin2 (n + 1)) ↦
        { p_1 : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
        (γ := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
        (g' rr n α) a.fs
        (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs × (α ::: β) a.fs) ↦ α.RelLast rr p_1.1 p_1.2) x property) =
      TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) a.fs
        (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs × (α ::: β) a.fs) ↦ α.RelLast rr p_1.1 p_1.2) x property)
⊢ comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (β :=
      fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i × (α ::: β) i //
        ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
      (γ := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
      (g' rr n α) i (Subtype.mk (p := fun (p_1 : (α ::: β) i × (α ::: β) i) ↦ α.RelLast rr p_1.1 p_1.2) x property) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) i
      (Subtype.mk (p := fun (p_1 : (α ::: β) i × (α ::: β) i) ↦ α.RelLast rr p_1.1 p_1.2) x property)

Tactic:
cases i
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property : α.RelLast rr x.1 x.2
⊢ comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (β :=
      fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i × (α ::: β) i //
        ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
      (γ := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
      (g' rr n α) Fin2.fz
      (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦ α.RelLast rr p_1.1 p_1.2) x property) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) Fin2.fz
      (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦ α.RelLast rr p_1.1 p_1.2) x property)

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
a : Fin2 n
x : (α ::: β) a.fs × (α ::: β) a.fs
property : α.RelLast rr x.1 x.2
⊢ comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (β :=
      fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i × (α ::: β) i //
        ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
      (γ := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) (f' rr n α)
      (g' rr n α) a.fs
      (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs × (α ::: β) a.fs) ↦ α.RelLast rr p_1.1 p_1.2) x property) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) a.fs
      (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs × (α ::: β) a.fs) ↦ α.RelLast rr p_1.1 p_1.2) x property)

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
h₁ :
  ∀ (i : Fin2 (n + 1)) (x : (α ::: β) i × (α ::: β) i)
    (property : ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i x.1 x.2))),
    (↑(Subtype.mk (p := fun (p : (α ::: β) i × (α ::: β) i) ↦
              ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2))) x property) :
          (α ::: β) i × (α ::: β) i).1 =
      (↑(f' rr n α i
              (Subtype.mk (p := fun (p : (α ::: β) i × (α ::: β) i) ↦
                ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2))) x property)) :
          (α ::: β) i × (α ::: β) i).1
⊢ Eq.{u + 1} (α :=
    (fun (i : Fin2 (n + 1)) ↦
        { p : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ⟹
      α ::: β)
    (fun (i : Fin2 (n + 1))
        (t :
          { p : (α ::: β) i × (α ::: β) i //
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ↦
      (↑t : (α ::: β) i × (α ::: β) i).1)
    fun (i : Fin2 (n + 1))
      (x :
        { p_1 : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }) ↦
    (↑(f' rr n α i x) : (α ::: β) i × (α ::: β) i).1

Tactic:
ext i ⟨x, _⟩
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
h₁ :
  ∀ (i : Fin2 (n + 1)) (x : (α ::: β) i × (α ::: β) i)
    (property : ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i x.1 x.2))),
    (↑(Subtype.mk (p := fun (p : (α ::: β) i × (α ::: β) i) ↦
              ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2))) x property) :
          (α ::: β) i × (α ::: β) i).2 =
      (↑(f' rr n α i
              (Subtype.mk (p := fun (p : (α ::: β) i × (α ::: β) i) ↦
                ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2))) x property)) :
          (α ::: β) i × (α ::: β) i).2
⊢ Eq.{u + 1} (α :=
    (fun (i : Fin2 (n + 1)) ↦
        { p : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ⟹
      α ::: β)
    (fun (i : Fin2 (n + 1))
        (t :
          { p : (α ::: β) i × (α ::: β) i //
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2)) }) ↦
      (↑t : (α ::: β) i × (α ::: β) i).2)
    fun (i : Fin2 (n + 1))
      (x :
        { p_1 : (α ::: β) i × (α ::: β) i //
          ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }) ↦
    (↑(f' rr n α i x) : (α ::: β) i × (α ::: β) i).2

Tactic:
ext i ⟨x, _⟩
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property : ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i x.1 x.2))
h₁ :
  ∀ (x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz)
    (property : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz x.1 x.2))),
    (↑(Subtype.mk (p := fun (p : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦
              ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz p.1 p.2))) x property) :
          (α ::: β) Fin2.fz × (α ::: β) Fin2.fz).1 =
      (↑(f' rr n α Fin2.fz
              (Subtype.mk (p := fun (p : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦
                ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz p.1 p.2))) x property)) :
          (α ::: β) Fin2.fz × (α ::: β) Fin2.fz).1
h₂ :
  ∀ (a : Fin2 n) (x : (α ::: β) a.fs × (α ::: β) a.fs)
    (property : ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs x.1 x.2))),
    (↑(Subtype.mk (p := fun (p : (α ::: β) a.fs × (α ::: β) a.fs) ↦
              ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs p.1 p.2))) x property) :
          (α ::: β) a.fs × (α ::: β) a.fs).1 =
      (↑(f' rr n α a.fs
              (Subtype.mk (p := fun (p : (α ::: β) a.fs × (α ::: β) a.fs) ↦
                ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs p.1 p.2))) x property)) :
          (α ::: β) a.fs × (α ::: β) a.fs).1
⊢ (↑(Subtype.mk (p := fun (p : (α ::: β) i × (α ::: β) i) ↦
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2))) x property) :
        (α ::: β) i × (α ::: β) i).1 =
    (↑(f' rr n α i
            (Subtype.mk (p := fun (p : (α ::: β) i × (α ::: β) i) ↦
              ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2))) x property)) :
        (α ::: β) i × (α ::: β) i).1

Tactic:
cases i
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property : ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i x.1 x.2))
h₁ :
  ∀ (x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz)
    (property : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz x.1 x.2))),
    (↑(Subtype.mk (p := fun (p : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦
              ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz p.1 p.2))) x property) :
          (α ::: β) Fin2.fz × (α ::: β) Fin2.fz).2 =
      (↑(f' rr n α Fin2.fz
              (Subtype.mk (p := fun (p : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦
                ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz p.1 p.2))) x property)) :
          (α ::: β) Fin2.fz × (α ::: β) Fin2.fz).2
h₂ :
  ∀ (a : Fin2 n) (x : (α ::: β) a.fs × (α ::: β) a.fs)
    (property : ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs x.1 x.2))),
    (↑(Subtype.mk (p := fun (p : (α ::: β) a.fs × (α ::: β) a.fs) ↦
              ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs p.1 p.2))) x property) :
          (α ::: β) a.fs × (α ::: β) a.fs).2 =
      (↑(f' rr n α a.fs
              (Subtype.mk (p := fun (p : (α ::: β) a.fs × (α ::: β) a.fs) ↦
                ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs p.1 p.2))) x property)) :
          (α ::: β) a.fs × (α ::: β) a.fs).2
⊢ (↑(Subtype.mk (p := fun (p : (α ::: β) i × (α ::: β) i) ↦
            ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2))) x property) :
        (α ::: β) i × (α ::: β) i).2 =
    (↑(f' rr n α i
            (Subtype.mk (p := fun (p : (α ::: β) i × (α ::: β) i) ↦
              ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p.1 p.2))) x property)) :
        (α ::: β) i × (α ::: β) i).2

Tactic:
cases i
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz x.1 x.2))
⊢ (↑(Subtype.mk (p := fun (p : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦
            ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz p.1 p.2))) x property) :
        (α ::: β) Fin2.fz × (α ::: β) Fin2.fz).1 =
    (↑(f' rr n α Fin2.fz
            (Subtype.mk (p := fun (p : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦
              ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz p.1 p.2))) x property)) :
        (α ::: β) Fin2.fz × (α ::: β) Fin2.fz).1

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
a : Fin2 n
x : (α ::: β) a.fs × (α ::: β) a.fs
property : ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs x.1 x.2))
⊢ (↑(Subtype.mk (p := fun (p : (α ::: β) a.fs × (α ::: β) a.fs) ↦
            ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs p.1 p.2))) x property) :
        (α ::: β) a.fs × (α ::: β) a.fs).1 =
    (↑(f' rr n α a.fs
            (Subtype.mk (p := fun (p : (α ::: β) a.fs × (α ::: β) a.fs) ↦
              ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs p.1 p.2))) x property)) :
        (α ::: β) a.fs × (α ::: β) a.fs).1

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property : ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz x.1 x.2))
⊢ (↑(Subtype.mk (p := fun (p : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦
            ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz p.1 p.2))) x property) :
        (α ::: β) Fin2.fz × (α ::: β) Fin2.fz).2 =
    (↑(f' rr n α Fin2.fz
            (Subtype.mk (p := fun (p : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz) ↦
              ofRepeat (α.RelLast' rr Fin2.fz (prod.mk (α := α ::: β) (β := α ::: β) Fin2.fz p.1 p.2))) x property)) :
        (α ::: β) Fin2.fz × (α ::: β) Fin2.fz).2

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x_1 y : F (α ::: β)
u :
  F fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i × (α ::: β) i //
      ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) }
a : Fin2 n
x : (α ::: β) a.fs × (α ::: β) a.fs
property : ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs x.1 x.2))
⊢ (↑(Subtype.mk (p := fun (p : (α ::: β) a.fs × (α ::: β) a.fs) ↦
            ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs p.1 p.2))) x property) :
        (α ::: β) a.fs × (α ::: β) a.fs).2 =
    (↑(f' rr n α a.fs
            (Subtype.mk (p := fun (p : (α ::: β) a.fs × (α ::: β) a.fs) ↦
              ofRepeat (α.RelLast' rr a.fs (prod.mk (α := α ::: β) (β := α ::: β) a.fs p.1 p.2))) x property)) :
        (α ::: β) a.fs × (α ::: β) a.fs).2

Tactic:
rfl
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type v
α : Type u
inst : Functor F
inst_1 : LawfulFunctor F
⊢ Eq.{v + 1} (α := F α → F α) (fun (x : F α) ↦ id <$> x) id

Tactic:
funext id_map

Premises used: funext, LawfulFunctor.id_map
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type v
α β γ : Type u
inst : Functor F
inst_1 : LawfulFunctor F
f : α → β
g : β → γ
⊢ Eq.{v + 1} (α := F α → F γ) ((fun (x : F β) ↦ g <$> x) ∘ fun (x : F α) ↦ f <$> x) fun (x : F α) ↦ (g ∘ f) <$> x

Tactic:
funext fun _ => (comp_map _ _ _).symm

Premises used: funext, Eq.symm, LawfulFunctor.comp_map
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
h : ∀ (α β : Type u_1) (f : α → β) (x : F α), m f x = m' f x
⊢ @m = @m'

Tactic:
funext α β f x
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
f : α → β
x : F α
⊢ m f x = m' f x

Tactic:
apply H
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
refl :
  ∀ (H2 : LawfulFunctor F) (H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x),
    { map := @m, mapConst := @mc : Functor F } = { map := @m, mapConst := @mc' }
⊢ { map := @m, mapConst := @mc : Functor F } = { map := @m', mapConst := @mc' }

Tactic:
cases show @m = @m' by funext α β f x; apply H
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
refl : @mc = @mc'
⊢ { map := @m, mapConst := @mc : Functor F } = { map := @m, mapConst := @mc' }

Tactic:
congr
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
refl : ∀ (α β : Type u_1), Eq (α := α → F β → F α) mc mc'
⊢ @mc = @mc'

Tactic:
funext α β
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
⊢ ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)

Tactic:
have E1 := @map_const _ ⟨@m, @mc⟩ H1
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
E1 : ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)
⊢ ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)

Tactic:
have E2 := @map_const _ ⟨@m, @mc'⟩ H2