awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
      ∀ (i : P.B a_1), p (f_1 i)
have mpr : ∃ (f_1 : P.B a → α),
  Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f_1) ∧
    ∀ (i : P.B a), p (f_1 i)
Tactic: first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ (f_1 : P.B a → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f_1) ∧
      ∀ (i : P.B a), p (f_1 i)
have mpr : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) ∧
  ∀ (i : P.B a), p (f i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ (f_1 : P.B a → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f_1) ∧
      ∀ (i : P.B a), p (f_1 i)
have mpr : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) ∧
  ∀ (i : P.B a), p (f i)
Tactic: first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) ∧
    ∀ (i : P.B a), p (f i)
have mpr : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) ∧
    ∀ (i : P.B a), p (f i)
have mpr : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
Tactic: first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
      ∀ (i : P.B a_1), p (f_1 i)
have mpr : ∃ (f_1 : P.B a → α),
  Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f_1) ∧
    ∀ (i : P.B a), p (f_1 i)
Tactic: repeat' first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
mpr :
  ∃ (f_1 : P.B a → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f_1) ∧
      ∀ (i : P.B a), p (f_1 i)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
      ∀ (i : P.B a_1), p (f_1 i)
have mpr₁ : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) ∧
  ∀ (i : P.B a), p (f i)
Tactic: repeat' first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
mpr :
  ∃ (f_1 : P.B a → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f_1) ∧
      ∀ (i : P.B a), p (f_1 i)
mpr₁ :
  Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) ∧
    ∀ (i : P.B a), p (f i)
⊢ ∃ (a_1 : P.A) (f_1 : P.B a_1 → α),
    Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a_1 f_1) ∧
      ∀ (i : P.B a_1), p (f_1 i)
have mpr₂ : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
Tactic: repeat' first | constructor | assumption
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
⊢ Liftr r x y ↔
    ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α),
      x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀ ∧
        y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
have mp : Liftr r x y →
  ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α),
    x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀ ∧
      y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
mp :
  Liftr r x y →
    ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α),
      x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀ ∧
        y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ Liftr r x y ↔
    ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α),
      x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀ ∧
        y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
have mpr : (∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α),
    x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀ ∧
      y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)) →
  Liftr r x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
u : (↑P : (α : Type u) → Type (max u uA uB)) { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
⊢ ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α),
    x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀ ∧
      y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
have mp : ∀ (a : P.A) (f : P.B a → { p : α × α // r p.1 p.2 })
  (h : u = Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f),
  ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α),
    x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀ ∧
      y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
Tactic: rcases h : u with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
u : (↑P : (α : Type u) → Type (max u uA uB)) { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
a : P.A
f : P.B a → { p : α × α // r p.1 p.2 }
h : u = Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f
⊢ ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α),
    x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀ ∧
      y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
have h₁ : (x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).1) ∧
  (y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2) ∧
    ∀ (i : P.B a), r (↑(f i) : α × α).1 ((fun (i : P.B a) ↦ (↑(f i) : α × α).2) i)
Tactic: use a, fun i => (f i).val.fst, fun i => (f i).val.snd
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
u : (↑P : (α : Type u) → Type (max u uA uB)) { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
a : P.A
f : P.B a → { p : α × α // r p.1 p.2 }
h : u = Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f
⊢ (x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).1) ∧
    (y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2) ∧
      ∀ (i : P.B a), r (↑(f i) : α × α).1 ((fun (i : P.B a) ↦ (↑(f i) : α × α).2) i)
have h₁ : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
u : (↑P : (α : Type u) → Type (max u uA uB)) { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
a : P.A
f : P.B a → { p : α × α // r p.1 p.2 }
h : u = Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f
h₁ : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).1
⊢ (x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).1) ∧
    (y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2) ∧
      ∀ (i : P.B a), r (↑(f i) : α × α).1 ((fun (i : P.B a) ↦ (↑(f i) : α × α).2) i)
have h₂ : (y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2) ∧
  ∀ (i : P.B a), r (↑(f i) : α × α).1 (↑(f i) : α × α).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
u : (↑P : (α : Type u) → Type (max u uA uB)) { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
a : P.A
f : P.B a → { p : α × α // r p.1 p.2 }
h : u = Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f
⊢ x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).1
have h₁ : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α)
  ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
    Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).1)
Tactic: rw [← xeq, h]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
u : (↑P : (α : Type u) → Type (max u uA uB)) { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
a : P.A
f : P.B a → { p : α × α // r p.1 p.2 }
h : u = Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f
⊢ (y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2) ∧
    ∀ (i : P.B a), r (↑(f i) : α × α).1 (↑(f i) : α × α).2
have h₁ : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
u : (↑P : (α : Type u) → Type (max u uA uB)) { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
a : P.A
f : P.B a → { p : α × α // r p.1 p.2 }
h : u = Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f
h₁ : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2
⊢ (y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2) ∧
    ∀ (i : P.B a), r (↑(f i) : α × α).1 (↑(f i) : α × α).2
have h₂ : ∀ (i : P.B a), r (↑(f i) : α × α).1 (↑(f i) : α × α).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
u : (↑P : (α : Type u) → Type (max u uA uB)) { p : α × α // r p.1 p.2 }
xeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$> u = x
yeq : (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$> u = y
a : P.A
f : P.B a → { p : α × α // r p.1 p.2 }
h : u = Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f
⊢ y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2
have h₁ : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α)
  ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
    Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a f)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2)
Tactic: rw [← yeq, h]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀
yeq : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ Liftr r x y
have h₁ : ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
      Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
        Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry) =
    x ∧
  ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
      Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
        Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry) =
    y
Tactic: use ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀
yeq : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
        Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
          Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      x ∧
    ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
        Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
          Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      y
have h₁ : ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
    Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
      Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry) =
  x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀
yeq : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
h₁ :
  ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
      Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
        Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
    x
⊢ ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
        Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
          Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      x ∧
    ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
        Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
          Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      y
have h₂ : ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
    Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
      Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry) =
  y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀
yeq : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
      Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
        Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
    x
have h₁ : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α)
  ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
    Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
      Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀)
Tactic: rw [xeq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : (↑P : (α : Type u) → Type (max u uA uB)) α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀
yeq : y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
      Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
        Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
    y
have h₁ : Eq (α := (↑P : (α : Type u) → Type (max u uA uB)) α)
  ((fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
    Sigma.mk (β := fun (x : P.A) ↦ P.B x → { p : α × α // r p.1 p.2 }) a fun (i : P.B a) ↦
      Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) sorry)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁)
Tactic: rw [yeq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
⊢ supp (F := (↑P : (α : Type u) → Type (max u uA uB))) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) = f '' univ
have h : ∀ (x : α),
  Membership.mem (γ := Set α)
      (supp (F := (↑P : (α : Type u) → Type (max u uA uB))) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)) x ↔
    x ∈ f '' univ
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ Membership.mem (γ := Set α)
      (supp (F := (↑P : (α : Type u) → Type (max u uA uB))) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)) x ↔
    x ∈ f '' univ
have h : (∀ ⦃p : α → Prop⦄,
    Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x) ↔
  ∃ (y : P.B a), f y = x
Tactic: simp only [supp, image_univ, mem_range, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄,
      Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x) ↔
    ∃ (y : P.B a), f y = x
have h : (∀ ⦃p : α → Prop⦄,
    Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x) →
  ∃ (y : P.B a), f y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h :
  (∀ ⦃p : α → Prop⦄,
      Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x) →
    ∃ (y : P.B a), f y = x
⊢ (∀ ⦃p : α → Prop⦄,
      Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x) ↔
    ∃ (y : P.B a), f y = x
have h₁ : (∃ (y : P.B a), f y = x) →
  ∀ ⦃p : α → Prop⦄,
    Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h :
  ∀ ⦃p : α → Prop⦄,
    Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x
⊢ ∃ (y : P.B a), f y = x
have h₁ : Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) (fun (x : α) ↦ ∃ (y : P.B a), f y = x)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
Tactic: apply @h fun x => ∃ y : P.B a, f y = x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h :
  ∀ ⦃p : α → Prop⦄,
    Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x
⊢ Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) (fun (x : α) ↦ ∃ (y : P.B a), f y = x)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f)
have h₁ : ∀ (i : P.B a), ∃ (y : P.B a), f y = f i
Tactic: rw [liftp_iff']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ (y : P.B a), f y = x
⊢ ∀ ⦃p : α → Prop⦄,
    Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x
have h₁ : ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x
Tactic: simp only [liftp_iff']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ (y : P.B a), f y = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x
have h₁ : ∀ (w : P.B a), f w = x → ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.Basic (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
w : P.B a
h : f w = x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x
have h : ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p (f w)
Tactic: subst x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F (n + 1)
⊢ x = CofixA.intro (head' x) (children' x)
have intro : ∀ (a : F.A) (a_1 : F.B a → CofixA F n),
  CofixA.intro a a_1 = CofixA.intro (head' (CofixA.intro a a_1)) (children' (CofixA.intro a a_1))
Tactic: cases x
Cleared hypotheses: x