awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1
h₂ :
  (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
⊢ (x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1) ∧
    (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
      ∀ (i : Fin2 n) (j : P.B a i),
        r (↑(f i j) : α i × α i).1 ((fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) i j)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ :
  Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1)
⊢ x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1

Tactic:
rw [← xeq, h]
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).1)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2
h₂ : ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
⊢ (y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ :
  Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2)
⊢ y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2

Tactic:
rw [← yeq, h]
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i × α i).2)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
i : Fin2 n
j : P.B a i
⊢ r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2

Tactic:
(f i j).property

Premises used: Subtype.property
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
u : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
      (β := α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h : u = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
i : Fin2 n
j : P.B a i
⊢ r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2

Tactic:
exact (f i j).property

Premises used: Subtype.property
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
a : P.A
f₀ f₁ : P.B a ⟹ α
xeq : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀
yeq : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁
h : ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
⊢ LiftR (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) r x y

Tactic:
⟨⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩, xeq.symm, yeq.symm⟩

Premises used: Prod.mk, Subtype.mk, And.intro, Exists.intro, MvFunctor.LiftR, Sigma.mk, Eq.symm
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
a : P.A
f₀ f₁ : P.B a ⟹ α
xeq : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀
yeq : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁
h : ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
⊢ LiftR (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) r x y

Tactic:
exact ⟨⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩, xeq.symm, yeq.symm⟩
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
h :
  ∀ (x : α i),
    Membership.mem (γ := Set (α i))
        (supp (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) i) x ↔
      x ∈ f i '' univ
⊢ supp (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) i =
    f i '' univ

Tactic:
ext x
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
      LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
        P_1 i x) ↔
    ∃ (y : P.B a i), f i y = x
⊢ Membership.mem (γ := Set (α i))
      (supp (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) i) x ↔
    x ∈ f i '' univ

Tactic:
simp only [supp, image_univ, mem_range, mem_setOf_eq]

Premises used: Set.image_univ, Set.mem_range, MvFunctor.supp, Set.mem_setOf_eq
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
      LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
        P_1 i x) →
    ∃ (y : P.B a i), f i y = x
h₁ :
  (∃ (y : P.B a i), f i y = x) →
    ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
      LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
        P_1 i x
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
      LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
        P_1 i x) ↔
    ∃ (y : P.B a i), f i y = x

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x
h₁ :
  LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (fun (i : Fin2 n) (x : α i) ↦ ∃ (y : P.B a i), f i y = x)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
⊢ ∃ (y : P.B a i), f i y = x

Tactic:
apply @h fun i x => ∃ y : P.B a i, f i y = x
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x
h₁ : ∀ (i : Fin2 n) (x : P.B a i), ∃ (y : P.B a i), f i y = f i x
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) (fun (i : Fin2 n) (x : α i) ↦ ∃ (y : P.B a i), f i y = x)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)

Tactic:
rw [liftP_iff']

Premises used: MvPFunctor.liftP_iff'
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x
i_1 : Fin2 n
x_1 : P.B a i_1
⊢ ∃ (y : P.B a i_1), f i_1 y = f i_1 x_1

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h :
  ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x
i_1 : Fin2 n
x_1 : P.B a i_1
⊢ ∃ (y : P.B a i_1), f i_1 y = f i_1 x_1

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ (y : P.B a i), f i y = x
h₁ : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄,
    LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) P_1 (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) →
      P_1 i x

Tactic:
simp only [liftP_iff']

Premises used: MvPFunctor.liftP_iff'
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ (y : P.B a i), f i y = x
h₁ :
  ∀ (w : P.B a i),
    f i w = x → ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i x

Tactic:
cases h
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
w : P.B a i
h_1 : f i w = x
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i (f i w)
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i x

Tactic:
subst x
-- Module: Mathlib.Data.PFunctor.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
w : P.B a i
h h₁ h₂ h₃ h₄ h₅ h₆ h₇ :
  ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i (f i w)
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, (∀ (i : Fin2 n) (x : P.B a i), P_1 i (f i x)) → P_1 i (f i w)

Tactic:
tauto
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
x : P.last.M
i : Fin2 n
inst : Inhabited (P.drop.B x.head i)
a : P.last.A := x.head
f : (i : P.last.B x.head) → P.last.M := x.children
a_1 : P.last.A
f_1 : P.last.B a_1 → P.last.M
simp : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) x.head f
⊢ x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f

Tactic:
simp [a]
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
x : P.last.M
i : Fin2 n
inst : Inhabited (P.drop.B x.head i)
a : P.last.A := x.head
f : (i : P.last.B x.head) → P.last.M := x.children
a_1 : P.last.A
f_1 : P.last.B a_1 → P.last.M
⊢ x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) x.head f

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
⊢ MvFunctor (n := n) fun (α : TypeVec.{u} n) ↦ (↑P.mp : (α : TypeVec.{u} n) → Type u) α

Tactic:
infer_instance
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
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
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
rw :
  ∀
    (h' :
      Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
        (PFunctor.map.{u, u, v, u} P.last (α := β)
          (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
          (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
        (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f))
    (c : P.drop.B a i) (h : x = corecShape P g₀ g₂ b), a = g₀ b
⊢ a = g₀ b

Tactic:
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'

Premises used: MvPFunctor.M.corecShape, PFunctor.M.dest_corec
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' :
  Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
    (PFunctor.map.{u, u, v, u} P.last (α := β)
      (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
    (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f)
c : P.drop.B a i
h : x = corecShape P g₀ g₂ b
refl : ∀ (c : P.drop.B (g₀ b) i), g₀ b = g₀ b
⊢ a = g₀ b

Tactic:
cases h'
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
h : x = corecShape P g₀ g₂ b
c : P.drop.B (g₀ b) i
⊢ g₀ b = g₀ b

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
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
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
rw :
  ∀
    (h' :
      Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
        (PFunctor.map.{u, u, v, u} P.last (α := β)
          (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
          (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
        (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f))
    (j : P.last.B a) (c : Path P (f j) i) (h : x = corecShape P g₀ g₂ b), a = g₀ b
⊢ a = g₀ b

Tactic:
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'

Premises used: MvPFunctor.M.corecShape, PFunctor.M.dest_corec
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' :
  Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
    (PFunctor.map.{u, u, v, u} P.last (α := β)
      (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
    (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f)
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
refl :
  ∀ (j : P.last.B (g₀ b))
    (c :
      Path P
        (((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j)
        i),
    g₀ b = g₀ b
⊢ a = g₀ b

Tactic:
cases h'
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
h : x = corecShape P g₀ g₂ b
j : P.last.B (g₀ b)
c :
  Path P (((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j)
    i
⊢ g₀ b = g₀ b

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
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
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
rw :
  ∀
    (h' :
      Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
        (PFunctor.map.{u, u, v, u} P.last (α := β)
          (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
          (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
        (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f))
    (j : P.last.B a) (c : Path P (f j) i) (h : x = corecShape P g₀ g₂ b) (h₀ : a = g₀ b),
    f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))

Tactic:
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'

Premises used: MvPFunctor.M.corecShape, PFunctor.M.dest_corec