awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
rw : Membership.mem (γ := Part (Subtype p)) { Dom := p (f a), get := Subtype.mk (p := p) (f a) } b ↔ (↑b : β) = f a
rw₁ : (∃ (h : p (f a)), Subtype.mk (p := p) (f a) h = b) ↔ (↑b : β) = f a
⊢ b ∈ toSubtype p f a ↔ (↑b : β) = f a
have rw₂ : f a = (↑b : β) ↔ (↑b : β) = f a
Tactic: rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
rw : Membership.mem (γ := Part (Subtype p)) { Dom := p (f a), get := Subtype.mk (p := p) (f a) } b ↔ (↑b : β) = f a
rw₁ : (∃ (h : p (f a)), Subtype.mk (p := p) (f a) h = b) ↔ (↑b : β) = f a
rw₂ : f a = (↑b : β) ↔ (↑b : β) = f a
⊢ b ∈ toSubtype p f a ↔ (↑b : β) = f a
have rw₃ : (↑b : β) = f a ↔ (↑b : β) = f a
Tactic: rw [toSubtype_apply, Part.mem_mk_iff, exists_subtype_mk_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
⊢ (f.comp g).Dom = g.preimage f.Dom
have h : ∀ (x : α), x ∈ (f.comp g).Dom ↔ x ∈ g.preimage f.Dom
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x : α
⊢ x ∈ (f.comp g).Dom ↔ x ∈ g.preimage f.Dom
have h : (∃ (y : γ), ∃ (a : β), a ∈ g x ∧ y ∈ f a) ↔ ∃ (y : β), (∃ (y_1 : γ), y_1 ∈ f y) ∧ y ∈ g x
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
⊢ a.bind (f.comp g) = (a.bind g).bind f
have H : ∀ (a_1 : γ), a_1 ∈ a.bind (f.comp g) ↔ a_1 ∈ (a.bind g).bind f
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x
have trans : y ∈ f.prodLift g x ↔ ∃ (hp : (f x).Dom), ∃ (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2
Tactic: trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
trans : y ∈ f.prodLift g x ↔ ∃ (hp : (f x).Dom), ∃ (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2
⊢ y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x
have trans₁ : (∃ (hp : (f x).Dom), ∃ (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x
Tactic: trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2
have trans : y ∈ f.prodMap g x ↔ ∃ (hp : (f x.1).Dom), ∃ (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
Tactic: trans ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
trans : y ∈ f.prodMap g x ↔ ∃ (hp : (f x.1).Dom), ∃ (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
⊢ y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2
have trans₁ : (∃ (hp : (f x.1).Dom), ∃ (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2
Tactic: trans ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
x : (↑(const n A) : (α : TypeVec.{u} n) → Type u) α
⊢ get (α := β) (MvFunctor.map (F := (↑(const n A) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f x) =
    get (α := α) x
have mk : ∀ (fst : (const n A).A) (snd : (const n A).B fst ⟹ α),
  get (α := β)
      (MvFunctor.map (F := (↑(const n A) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f
        (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)) =
    get (α := α) (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
x : (↑(const n A) : (α : TypeVec.{u} n) → Type u) α
⊢ mk n (get (α := α) x) (α := α) = x
have mk : ∀ (fst : (const n A).A) (snd : (const n A).B fst ⟹ α),
  Eq (α := (↑(const n A) : (α : TypeVec.{u} n) → Type u) α)
    (mk n (get (α := α) (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)) (α := α))
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
fst : (const n A).A
snd : (const n A).B fst ⟹ α
⊢ Eq (α := (↑(const n A) : (α : TypeVec.{u} n) → Type u) α)
    (mk n (get (α := α) (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)) (α := α))
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)
have mk : Eq (α := (↑(const n A) : (α : TypeVec.{u} n) → Type u) α)
  (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst fun (x : Fin2 n) (a : (const n A).B fst x) ↦
    PEmpty.elim a)
  (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)
Tactic: dsimp [const.get, const.mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
fst : (const n A).A
snd : (const n A).B fst ⟹ α
⊢ Eq (α := (↑(const n A) : (α : TypeVec.{u} n) → Type u) α)
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst fun (x : Fin2 n) (a : (const n A).B fst x) ↦
      PEmpty.elim a)
    (Sigma.mk (β := fun (a : (const n A).A) ↦ (const n A).B a ⟹ α) fst snd)
have mk : (fun (x : Fin2 n) (a : (const n A).B fst x) ↦ PEmpty.elim a) = snd
Tactic: congr with (_⟨⟩)
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x ↔
    ∃ (a : P.A) (f : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
have mp : LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x →
  ∃ (a : P.A) (f : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
mp :
  LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x →
    ∃ (a : P.A) (f : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x ↔
    ∃ (a : P.A) (f : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
have mpr : (∃ (a : P.A) (f : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)) →
  LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
y : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y =
    x
⊢ ∃ (a : P.A) (f : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
have mp : ∀ (a : P.A) (f : P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p)
  (h : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f),
  ∃ (a : P.A) (f : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
Tactic: rcases h : y with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
y : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y =
    x
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
⊢ ∃ (a : P.A) (f : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
have mp : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i)
Tactic: refine ⟨a, fun i j => (f i j).val, ?_, fun i j => (f i j).property⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
y : (↑P : (α : TypeVec.{u} n) → Type u) fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y =
    x
a : P.A
f : P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h : y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
⊢ x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i)
have mp : Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a
    (TypeVec.comp (α := P.B a) (β := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (γ := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p)) f))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a fun (i : Fin2 n) (j : P.B a i) ↦ (↑(f i j) : α i))
Tactic: rw [← hy, h, map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
a : P.A
f : P.B a ⟹ α
xeq : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p x
have h : MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
    (fun (i : Fin2 n) ↦ Subtype.val (p := p))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a fun (i : Fin2 n) (j : P.B a i) ↦
      Subtype.mk (p := p) (f i j) sorry) =
  x
Tactic: use ⟨a, fun i j => ⟨f i j, pf i j⟩⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : (↑P : (α : TypeVec.{u} n) → Type u) α
a : P.A
f : P.B a ⟹ α
xeq : x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a
        fun (i : Fin2 n) (j : P.B a i) ↦ Subtype.mk (p := p) (f i j) ⋯) =
    x
have h : Eq.{u + 1} (α := (↑P : (α : TypeVec.{u} n) → Type u) α)
  (MvFunctor.map (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
    (fun (i : Fin2 n) ↦ Subtype.val (p := p))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a fun (i : Fin2 n) (j : P.B a i) ↦
      Subtype.mk (p := p) (f i j) sorry))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
Tactic: rw [xeq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ LiftP (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) p (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ↔
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
have simp : (∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) ↔
  ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
Tactic: simp only [liftP_iff]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
      Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
        ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) ↔
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
have mp : (∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) →
  ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
mp :
  (∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
      Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
        ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) →
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ (∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
      Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
        ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) ↔
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
have mpr : (∀ (i : Fin2 n) (x : P.B a i), p (f i x)) →
  ∃ (a_2 : P.A) (f_1 : P.B a_2 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_2 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_2 i), p (f_1 i j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)
have mpr : ∃ (f_1 : P.B a ⟹ α),
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)
have mpr : ∃ (f_1 : P.B a ⟹ α),
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
Tactic: first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
have mpr : Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
  ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
have mpr : Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
  ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
Tactic: first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
have mpr : Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
have mpr : Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
Tactic: first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)
have mpr : ∃ (f_1 : P.B a ⟹ α),
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
Tactic: repeat' first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)
have mpr₁ : Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
  ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
Tactic: repeat' first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
h : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
mpr :
  ∃ (f_1 : P.B a ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a i), p (f_1 i j)
mpr₁ :
  Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f) ∧
    ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 ⟹ α),
    Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)
have mpr₂ : Eq (α := (↑P : (α : TypeVec.{u} n) → Type u) α) (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f)
Tactic: repeat' first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
⊢ LiftR (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) r x y ↔
    ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
        y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
have mp : LiftR (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) r x y →
  ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
      y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.Basic (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : (↑P : (α : TypeVec.{u} n) → Type u) α
mp :
  LiftR (F := (↑P : (α : TypeVec.{u} n) → Type u)) (α := α) r x y →
    ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
        y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (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 ↔
    ∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
      x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
        y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
have mpr : (∃ (a : P.A) (f₀ : P.B a ⟹ α) (f₁ : P.B a ⟹ α),
    x = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₀ ∧
      y = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α) a f₁ ∧ ∀ (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: constructor