awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
a' : P.A
f' : P.B a' → α
heq :
  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')
h' : ∀ (i : P.B a'), p (f' i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
cases heq
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h' : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
assumption
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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₁ : P.A
⊢ ∃ (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)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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₁ : P.A
⊢ ∃ (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)

Tactic:
first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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 :
  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)
mpr₁ : P.B a → α
⊢ ∃ (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:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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 :
  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)
mpr₁ : P.B a → α
⊢ ∃ (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
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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 :
  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)
mpr₁ : ∀ (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)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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 :
  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)
mpr₁ : ∀ (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)

Tactic:
first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)

Tactic:
first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
assumption
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
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)
mpr₃ : ∀ (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)

Tactic:
repeat' first | constructor | assumption
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
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
⊢ 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
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
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)
⊢ ∃ (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⟩
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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) ∧
    (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)
⊢ ∃ (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:
use a, fun i => (f i).val.fst, fun i => (f i).val.snd

Premises used: Prod.fst, Subtype.val, Prod.snd
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
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
⊢ (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:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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₁ :
  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)
⊢ x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).1

Tactic:
rw [← xeq, h]
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
⊢ 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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
h₂ : ∀ (i : P.B a), r (↑(f i) : α × α).1 (↑(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

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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₁ :
  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)
⊢ y = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a fun (i : P.B a) ↦ (↑(f i) : α × α).2

Tactic:
rw [← yeq, h]
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
⊢ 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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
i : P.B a
⊢ r (↑(f i) : α × α).1 (↑(f i) : α × α).2

Tactic:
(f i).property

Premises used: Subtype.property
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
i : P.B a
⊢ r (↑(f i) : α × α).1 (↑(f i) : α × α).2

Tactic:
exact (f i).property

Premises used: Subtype.property
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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 : α × α).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
⊢ Liftr r x y

Tactic:
use ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
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) ⋯) =
    y
⊢ ((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

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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₁ :
  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) ⋯)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀)
⊢ ((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

Tactic:
rw [xeq]
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
⊢ 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) ⋯)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₀)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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₁ :
  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) ⋯)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁)
⊢ ((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

Tactic:
rw [yeq]
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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)
⊢ 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) ⋯)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f₁)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
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
⊢ supp (F := (↑P : (α : Type u) → Type (max u uA uB))) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) = f '' univ

Tactic:
ext x
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
⊢ 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:
simp only [supp, image_univ, mem_range, mem_setOf_eq]

Premises used: Set.image_univ, Set.mem_range, Set.mem_setOf_eq, Functor.supp
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
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
⊢ (∀ ⦃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
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
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)
⊢ ∃ (y : P.B a), f y = x

Tactic:
apply @h fun x => ∃ y : P.B a, f y = x
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
h₁ : ∀ (i : P.B a), ∃ (y : P.B a), f y = f i
⊢ 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:
rw [liftp_iff']

Premises used: PFunctor.liftp_iff'
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
i : P.B a
⊢ ∃ (y : P.B a), f y = f i

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
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
i : P.B a
⊢ ∃ (y : P.B a), f y = f i

Tactic:
exact ⟨_, rfl⟩