awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
⊢ dest P (α := α) (corec P (α := α) g x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) (g x)
have trans : dest P (α := α) (corec P (α := α) g x) =
  Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
    (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
      (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
        ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
      ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
          (fun (b : β) ↦
            dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
          fun (b : β) ↦
          lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
        lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))))
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
trans :
  dest P (α := α) (corec P (α := α) g x) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
      (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
        (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))))
⊢ dest P (α := α) (corec P (α := α) g x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) (g x)
have trans₁ : Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
    (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
      (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
        ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
      ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
          (fun (b : β) ↦
            dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
          fun (b : β) ↦
          lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
        lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))) =
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) (g x)
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
trans :
  dest P (α := α) (corec P (α := α) g x) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
      (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
        (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))))
trans₁ :
  Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
      (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
        (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) (g x)
⊢ dest P (α := α) (corec P (α := α) g x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) (g x)
have trans₂ : (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α)
Tactic: trans
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B a) (β := α ::: β) f)))
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f))
have rw : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
    (splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
      ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
          (fun (b : β) ↦
            dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
          fun (b : β) ↦
          lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
        lastFun (α := P.B a) (β := α ::: β) f)))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
    (TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f))
Tactic: rw [MvPFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B a) (β := α ::: β) f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f))
have e_snd : splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
    ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
        (fun (b : β) ↦
          dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        fun (b : β) ↦
        lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
      lastFun (α := P.B a) (β := α ::: β) f) =
  TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
| TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f
have rw : splitFun (α := P.B a) (α' := α ::: P.M α)
  (TypeVec.comp (α := (P.B a).drop) (β := α) (γ := (α ::: P.M α).drop) (TypeVec.id (α := α))
    (dropFun (α := P.B a) (β := α ::: β) f))
  (corec P (α := α) g ∘ lastFun (α := P.B a) (β := α ::: β) f)
Tactic: rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
      ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
          (fun (b : β) ↦
            dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
          fun (b : β) ↦
          lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
        lastFun (α := P.B a) (β := α ::: β) f) =
    TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f
have e_snd : splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
    ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
        (fun (b : β) ↦
          dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        fun (b : β) ↦
        lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
      lastFun (α := P.B a) (β := α ::: β) f) =
  splitFun (α := P.B a) (α' := α ::: P.M α)
    (TypeVec.comp (α := (P.B a).drop) (β := α) (γ := (α ::: P.M α).drop) (TypeVec.id (α := α))
      (dropFun (α := P.B a) (β := α ::: β) f))
    (corec P (α := α) g ∘ lastFun (α := P.B a) (β := α ::: β) f)
Tactic: conv_rhs => rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' (splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁'))
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
have generalize : ∀ (ff : P.B a' ⟹ α ::: P.M α) (ef : splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' = ff)
  (e₁ :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff)),
  ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
Tactic: generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff at e₁
Cleared hypotheses: e₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' = ff
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff)
he₁' : (↑P.last : (α : Type u) → Type u) P.last.M := PFunctor.M.dest a₁
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
have rcases : ∀ (a₁' : P.last.A) (g₁' : P.last.B a₁' → P.last.M)
  (e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁' g₁'),
  ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
Tactic: rcases e₁' : he₁' with ⟨a₁', g₁'⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' = ff
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff)
he₁' : (↑P.last : (α : Type u) → Type u) P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁' g₁'
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
have e₂ : dest' P (α := α) e₁' f₁ = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff
Tactic: rw [M.dest_eq_dest' _ e₁'] at e₁
Cleared hypotheses: e₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' = ff
he₁' : (↑P.last : (α : Type u) → Type u) P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁' g₁'
e₁ : dest' P (α := α) e₁' f₁ = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
have refl : ∀ (g₁' : P.last.B a' → P.last.M) (e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁')
  (ef :
    splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' =
      splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := (α ::: P.M α).drop) e₁' f₁)
        fun (x : (P.B a').last) ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)),
  ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
Tactic: cases e₁
Cleared hypotheses: ff, ef, a₁', g₁', e₁', e₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
        (P.B a).last → (α ::: P.M α).last),
        dest P (α := α) x =
            Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁) ∧
          dest P (α := α) y =
              Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂) ∧
            ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
x y : P.M α
r : R x y
⊢ x = y
have obtain : ∀ (a₁ : P.mp.A) (f₁ : P.mp.B a₁ ⟹ α) (r : R (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁) y),
  Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁ = y
Tactic: obtain ⟨a₁, f₁⟩ := x
Cleared hypotheses: x, r
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
        (P.B a).last → (α ::: P.M α).last),
        dest P (α := α) x =
            Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁) ∧
          dest P (α := α) y =
              Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂) ∧
            ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
y : P.M α
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
r : R (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁) y
⊢ Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁ = y
have obtain : ∀ (a₂ : P.mp.A) (f₂ : P.mp.B a₂ ⟹ α)
  (r :
    R (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₂ f₂)),
  Eq (α := P.M α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁)
    (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₂ f₂)
Tactic: obtain ⟨a₂, f₂⟩ := y
Cleared hypotheses: y, r
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
        (P.B a).last → (α ::: P.M α).last),
        dest P (α := α) x =
            Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁) ∧
          dest P (α := α) y =
              Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂) ∧
            ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r :
  R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₁) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₂ f₂)
⊢ a₁ = a₂
have a₃ : ∀ (x y : P.last.M),
  (fun (a₁ a₂ : P.last.M) ↦
        ∃ (x : P.M α) (y : P.M α),
          R x y ∧ x.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) = a₁ ∧ y.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) = a₂)
      x y →
    ∃ (a : P.last.A) (f : P.last.B a → P.last.M) (f' : P.last.B a → P.last.M),
      x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f ∧
        y.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f' ∧
          ∀ (i : P.last.B a),
            (fun (a₁ a₂ : P.last.M) ↦
                ∃ (x : P.M α) (y : P.M α),
                  R x y ∧
                    x.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) = a₁ ∧
                      y.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) = a₂)
              (f i) (f' i)
Tactic: refine
      PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) ?_ _ _
        ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩