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
P : β → Prop
x : F (α ::: β)
⊢ LiftP' (α := α ::: β) (F := F) (α.PredLast' P) x ↔ LiftP (F := F) (α := α ::: β) (α.PredLast P) x
have dsimp : (∃ (u : F fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }),
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x) ↔
  ∃ (u : F fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)),
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) u =
      x
Tactic: dsimp only [LiftP, LiftP']
-- 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
P : β → Prop
x : F (α ::: β)
⊢ (∃ (u : F fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
        x) ↔
    ∃ (u : F fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) u =
        x
have h₀ : comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
    { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) =
  TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 })
Tactic: apply exists_iff_exists_of_mono F (f _ n α) (g _ n α)
-- 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
P : β → Prop
x : F (α ::: β)
h₀ :
  comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 })
⊢ (∃ (u : F fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
        x) ↔
    ∃ (u : F fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) u =
        x
have h₁ : ∀ (u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }),
  map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P))
        (map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β :=
          fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) u) =
      x
Tactic: apply exists_iff_exists_of_mono F (f _ n α) (g _ n α)
-- 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
P : β → Prop
x : F (α ::: β)
⊢ comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 })
have h₀ : ∀ (i : Fin2 (n + 1)) (x : (α ::: β) i) (property : α.PredLast P x),
  (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) i
          (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) i) =
    (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) i
          (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) i)
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
P : β → Prop
x_1 : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property : α.PredLast P x
⊢ (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) i
          (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) i) =
    (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) i
          (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) i)
have h₀ : ∀ (x : (α ::: β) Fin2.fz) (property : α.PredLast P x),
  (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) Fin2.fz
          (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) Fin2.fz) =
    (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) Fin2.fz
          (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) Fin2.fz)
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
P : β → Prop
x_1 : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property : α.PredLast P x
h₀ :
  ∀ (x : (α ::: β) Fin2.fz) (property : α.PredLast P x),
    (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) Fin2.fz
            (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ α.PredLast P p_1) x property)) :
        (α ::: β) Fin2.fz) =
      (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) Fin2.fz
            (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ α.PredLast P p_1) x property)) :
        (α ::: β) Fin2.fz)
⊢ (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) i
          (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) i) =
    (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) i
          (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) i)
have h₁ : ∀ (a : Fin2 n) (x : (α ::: β) a.fs) (property : α.PredLast P x),
  (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) a.fs
          (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) a.fs) =
    (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) a.fs
          (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) a.fs)
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
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P))
        (map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β :=
          fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) u) =
      x
have h₁ : map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
      (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
    x ↔
  map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
      (comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β :=
        fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (γ := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) (f P n α))
      u =
    x
Tactic: rw [MvFunctor.map_map]
-- 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
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β :=
          fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (γ := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) (f P n α))
        u =
      x
have h₁ : map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
      (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
    x ↔
  map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
      (fun (i : Fin2 (n + 1)) (x : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) ↦
        (↑(f P n α i x) : (α ::: β) i))
      u =
    x
Tactic: dsimp +unfoldPartialApp [(· ⊚ ·)]
-- 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
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
this :
  Eq.{u + 1} (α := (i : Fin2 (n + 1)) → (self : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) → (α ::: β) i)
    (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)))
    fun (i : Fin2 (n + 1)) (x : (fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) i) ↦
    (↑(f P n α i x) : (α ::: β) i)
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) (x : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) ↦
          (↑(f P n α i x) : (α ::: β) i))
        u =
      x
have rw : map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
      (fun (i : Fin2 (n + 1))
          (x : (fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) i) ↦
        (↑(f P n α i x) : (α ::: β) i))
      u =
    x ↔
  map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
      (fun (i : Fin2 (n + 1)) (x : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) ↦
        (↑(f P n α i x) : (α ::: β) i))
      u =
    x
Tactic: rw [this]
-- 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
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) (x : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) ↦
          (↑(f P n α i x) : (α ::: β) i))
        u =
      x
have h₁ : Eq.{u + 1} (α := (i : Fin2 (n + 1)) → (self : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) → (α ::: β) i)
  (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)))
  fun (i : Fin2 (n + 1)) (x : (fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) i) ↦
  (↑(f P n α i x) : (α ::: β) i)
Tactic: suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw [this]
-- 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
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
⊢ Eq.{u + 1} (α := (i : Fin2 (n + 1)) → (self : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) → (α ::: β) i)
    (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)))
    fun (i : Fin2 (n + 1)) (x : (fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) i) ↦
    (↑(f P n α i x) : (α ::: β) i)
have h₁ : ∀ (i : Fin2 (n + 1)) (x : (α ::: β) i) (property : ofRepeat (α.PredLast' P i x)),
  (↑(Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property) : (α ::: β) i) =
    (↑(f P n α i (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property)) : (α ::: β) i)
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
P : β → Prop
x_1 : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property : ofRepeat (α.PredLast' P i x)
⊢ (↑(Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property) : (α ::: β) i) =
    (↑(f P n α i (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property)) : (α ::: β) i)
have h₁ : ∀ (x : (α ::: β) Fin2.fz) (property : ofRepeat (α.PredLast' P Fin2.fz x)),
  (↑(Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ ofRepeat (α.PredLast' P Fin2.fz p_1)) x property) :
      (α ::: β) Fin2.fz) =
    (↑(f P n α Fin2.fz
          (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ ofRepeat (α.PredLast' P Fin2.fz p_1)) x property)) :
      (α ::: β) Fin2.fz)
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
P : β → Prop
x_1 : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property : ofRepeat (α.PredLast' P i x)
h₁ :
  ∀ (x : (α ::: β) Fin2.fz) (property : ofRepeat (α.PredLast' P Fin2.fz x)),
    (↑(Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ ofRepeat (α.PredLast' P Fin2.fz p_1)) x property) :
        (α ::: β) Fin2.fz) =
      (↑(f P n α Fin2.fz
            (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ ofRepeat (α.PredLast' P Fin2.fz p_1)) x property)) :
        (α ::: β) Fin2.fz)
⊢ (↑(Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property) : (α ::: β) i) =
    (↑(f P n α i (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property)) : (α ::: β) i)
have h₂ : ∀ (a : Fin2 n) (x : (α ::: β) a.fs) (property : ofRepeat (α.PredLast' P a.fs x)),
  (↑(Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ ofRepeat (α.PredLast' P a.fs p_1)) x property) : (α ::: β) a.fs) =
    (↑(f P n α a.fs (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ ofRepeat (α.PredLast' P a.fs p_1)) x property)) :
      (α ::: β) a.fs)
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
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x :
  (fun (i : Fin2 (x_1 + 1)) ↦
      { p_1 : (α ::: β) i × (α ::: β) i //
        ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
    i.fs
⊢ ofRepeat
      (α.RelLast' rr i.fs
        (prod.mk (α := α ::: β) (β := α ::: β) i.fs (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1
          (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2)) =
    ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2)
have erw : ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2) =
  ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2)
Tactic: erw [repeatEq_iff_eq]
-- 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
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x : (fun (i : Fin2 (x_1 + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) i.fs
⊢ α.RelLast rr (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2 =
    ofRepeat
      (α.RelLast' rr i.fs
        (prod.mk (α := α ::: β) (β := α ::: β) i.fs (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1
          (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2))
have simp : ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2) =
  ofRepeat
    (α.RelLast' rr i.fs
      (prod.mk (α := α ::: β) (β := α ::: β) i.fs (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1
        (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2))
Tactic: simp only [RelLast]
-- 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
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x : (fun (i : Fin2 (x_1 + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) i.fs
⊢ ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2) =
    ofRepeat
      (α.RelLast' rr i.fs
        (prod.mk (α := α ::: β) (β := α ::: β) i.fs (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1
          (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2))
have erw : ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2) =
  ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2)
Tactic: erw [repeatEq_iff_eq]
-- 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 (α ::: β)
⊢ LiftR' (α := α ::: β) (F := F) (α.RelLast' rr) x y ↔ LiftR (F := F) (α := α ::: β) (α.RelLast rr) x y
have 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
Tactic: dsimp only [LiftR, LiftR']