awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
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₂)
⊢ Eq (α := P.M α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₁)
    (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₂ f₂)
have this : a₁ = a₂
Tactic: have : a₁ = a₂ := by
    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⟩
    rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
    rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩
    rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
    rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩
    rw [e₁', e₂']
    exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩
-- 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₂)
this : a₁ = a₂
⊢ Eq (α := P.M α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₁)
    (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₂ f₂)
have subst : ∀ (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₂)),
  Eq (α := P.M α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₁)
    (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₂)
Tactic: subst this
Cleared hypotheses: a₂, f₂, r, this
-- 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₁ 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₂)
⊢ Eq (α := P.M α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₁)
    (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) a₁ f₂)
have e_snd : ∀ (i : Fin2 n) (p : P.mp.B a₁ i), f₁ i p = f₂ i p
Tactic: congr with (i p)
-- 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
i_1 : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
have e_snd : ∀ (a' : P.A) (f' : (P.B a').drop ⟹ (α ::: P.M α).drop) (f₁' f₂' : (P.B a').last → (α ::: P.M α).last)
  (e₁ :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' (splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁')))
  (e₂ :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' (splitFun (α := P.B a') (α' := α ::: P.M α) f' f₂')))
  (h'' : ∀ (i : (P.B a').last), R (f₁' i) (f₂' i)), f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
Tactic: obtain ⟨a', f', f₁', f₂', e₁, e₂, h''⟩ := h _ _ 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
i_1 : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂)
a' : P.A
f' : (P.B a').drop ⟹ (α ::: P.M α).drop
f₁' f₂' : (P.B a').last → (α ::: P.M α).last
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' (splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁'))
e₂ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' (splitFun (α := P.B a') (α' := α ::: P.M α) f' f₂'))
h'' : ∀ (i : (P.B a').last), R (f₁' i) (f₂' i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
have e_snd : ∀ (g₁' : P.last.B a' → P.last.M) (e₁' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁')
  (e₂ :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a'
        (splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) f₂')))
  (h'' :
    ∀ (i : (P.B a').last),
      R
        ((fun (x_1 : P.last.B a') ↦
            (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x_1) (pathDestRight P (α := α) e₁' f₁ x_1) :
              (a : P.mp.A) × P.mp.B a ⟹ α))
          i)
        (f₂' i))
  (e₁ :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a'
        (splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) fun (x_1 : P.last.B a') ↦
          Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x_1) (pathDestRight P (α := α) e₁' f₁ x_1)))),
  f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
Tactic: obtain ⟨g₁', e₁', rfl, rfl⟩ := M.bisim_lemma P e₁
Cleared hypotheses: f', f₁', e₁, e₂, h''
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
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
i_1 : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂)
g₂' : P.last.B a → P.last.M
e₂' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a g₂'
e₁' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) fun (x_1 : P.last.B a) ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (f x_1) (pathDestRight P (α := α) e₁' f₁ x_1)))
e₃ : pathDestLeft P (α := α) e₁' f₁ = pathDestLeft P (α := α) e₂' f₂
e₂ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) fun (x_1 : P.last.B a) ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₂' x_1) (pathDestRight P (α := α) e₂' f₂ x_1)))
h'' :
  ∀ (i : (P.B a).last),
    R
      ((fun (x_1 : P.last.B a) ↦
          (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (f x_1) (pathDestRight P (α := α) e₁' f₁ x_1) :
            (a : P.mp.A) × P.mp.B a ⟹ α))
        i)
      ((fun (x_1 : P.last.B a) ↦
          (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₂' x_1) (pathDestRight P (α := α) e₂' f₂ x_1) :
            (a : P.mp.A) × P.mp.B a ⟹ α))
        i)
e₂'₁ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
have e₄ : pathDestLeft P (α := α) e₁' f₁ = pathDestLeft P (α := α) e₂'₁ f₂
Tactic: cases h'.symm.trans e₂'
Cleared hypotheses: g₂', e₂', e₃, e₂, h''
-- 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
i_1 : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
i : P.last.B a
c : Fin2 n
p : Path P (f i) c
IH :
  ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α)
    (r :
      R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) (f i) f₁)
        (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) (f i) f₂)),
    f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
have e_snd : ∀ (a' : P.A) (f' : (P.B a').drop ⟹ (α ::: P.M α).drop) (f₁' f₂' : (P.B a').last → (α ::: P.M α).last)
  (e₁ :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' (splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁')))
  (e₂ :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' (splitFun (α := P.B a') (α' := α ::: P.M α) f' f₂')))
  (h'' : ∀ (i : (P.B a').last), R (f₁' i) (f₂' i)), f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
Tactic: obtain ⟨a', f', f₁', f₂', e₁, e₂, h''⟩ := h _ _ r
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
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
i_1 : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
i : P.last.B a
c : Fin2 n
p : Path P (f i) c
IH :
  ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α)
    (r :
      R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) (f i) f₁)
        (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) (f i) f₂)),
    f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂)
g₂' : P.last.B a → P.last.M
e₂' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a g₂'
e₁' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) fun (x_1 : P.last.B a) ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (f x_1) (pathDestRight P (α := α) e₁' f₁ x_1)))
e₃ : pathDestLeft P (α := α) e₁' f₁ = pathDestLeft P (α := α) e₂' f₂
e₂ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (pathDestLeft P (α := α) e₁' f₁) fun (x_1 : P.last.B a) ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₂' x_1) (pathDestRight P (α := α) e₂' f₂ x_1)))
h'' :
  ∀ (i : (P.B a).last),
    R
      ((fun (x_1 : P.last.B a) ↦
          (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (f x_1) (pathDestRight P (α := α) e₁' f₁ x_1) :
            (a : P.mp.A) × P.mp.B a ⟹ α))
        i)
      ((fun (x_1 : P.last.B a) ↦
          (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₂' x_1) (pathDestRight P (α := α) e₂' f₂ x_1) :
            (a : P.mp.A) × P.mp.B a ⟹ α))
        i)
e₂'₁ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
have e₄ : pathDestLeft P (α := α) e₁' f₁ = pathDestLeft P (α := α) e₂'₁ f₂
Tactic: cases h'.symm.trans e₂'
Cleared hypotheses: g₂', e₂', e₃, e₂, h''
-- 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₁ 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₂)
i : Fin2 n
p : P.mp.B a₁ i
⊢ f₁ i p = f₂ i p
have e_snd : ∀ (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M)
  (h' : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f) (i : Fin2 n) (c : P.drop.B a i)
  (f₁ f₂ : P.mp.B x ⟹ α)
  (r :
    R (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₁)
      (Sigma.mk (β := fun (a : P.last.M) ↦ Path P a ⟹ α) x f₂)),
  f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
Tactic: induction p with (
    obtain ⟨a', f', f₁', f₂', e₁, e₂, h''⟩ := h _ _ r
    obtain ⟨g₁', e₁', rfl, rfl⟩ := M.bisim_lemma P e₁
    obtain ⟨g₂', e₂', e₃, rfl⟩ := M.bisim_lemma P e₂
    cases h'.symm.trans e₁'
    cases h'.symm.trans e₂')
  | root x a f h' i c =>
    exact congr_fun (congr_fun e₃ i) c
  | child x a f h' i c p IH =>
    exact IH _ _ (h'' _)
Cleared hypotheses: f₁, f₂, r, p
-- 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₀ : Equivalence R
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
r : R x y
⊢ x = y
have apply : ∀ (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)
Tactic: apply M.bisim P R _ _ _ r
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
Hr : 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)
have h₁ : MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
Tactic: specialize h _ _ Hr
Cleared hypotheses: h
-- 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₀ : Equivalence R
x y : P.M α
h :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) 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)
have revert : ∀
  (h :
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) 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)
Tactic: revert h
Cleared hypotheses: h