awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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 : (α ::: β) 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
have h₀ : 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: apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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 (α ::: β)
⊢ 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 })
have 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)
Tactic: ext i ⟨x, _⟩ : 2
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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
⊢ 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)
have 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)
Tactic: cases i
Cleared hypotheses: i, x, property
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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)
⊢ 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)
have 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)
Tactic: cases i
Cleared hypotheses: i, x, property
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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)) }
⊢ (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) =
    (map (F := F) (α := 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))
              (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)
          u =
        x ∧
      map (F := F) (α := 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))
              (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)
          u =
        y)
have h₁ : 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: congr
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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)) }
⊢ 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
have 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
Tactic: ext i ⟨x, _⟩
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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)) }
⊢ 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
have 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
Tactic: ext i ⟨x, _⟩
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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))
⊢ (↑(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
have 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
Tactic: cases i
Cleared hypotheses: i, x, property
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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
⊢ (↑(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
have 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
Tactic: cases i
Cleared hypotheses: i, x, property
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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))
⊢ (↑(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
have 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
Tactic: cases i
Cleared hypotheses: i, x, property
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
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
⊢ (↑(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
have 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
Tactic: cases i
Cleared hypotheses: i, x, property
-- Lean 4 proof step from Mathlib.Control.Functor (goal)
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
⊢ @m = @m'
have h : ∀ (α β : Type u_1) (f : α → β) (x : F α), m f x = m' f x
Tactic: funext α β f x