awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
mp :
  Liftr r x y →
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f₀ : (P F).B a → α) (f₁ : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀) ∧
        y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁) ∧
          ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
mpr :
  (∃ (a : PFunctor.A.{u, u_1} (P F)) (f₀ : (P F).B a → α) (f₁ : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀) ∧
        y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁) ∧
          ∀ (i : (P F).B a), r (f₀ i) (f₁ i)) →
    Liftr r x y
⊢ Liftr r x y ↔
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f₀ : (P F).B a → α) (f₁ : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀) ∧
        y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁) ∧
          ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → { p : α × α // r p.1 p.2 })
    (h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f),
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f₀ : (P F).B a → α) (f₁ : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀) ∧
        y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁) ∧
          ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ ∃ (a : PFunctor.A.{u, u_1} (P F)) (f₀ : (P F).B a → α) (f₁ : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀) ∧
      y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁) ∧
        ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
rcases h : repr u with ⟨a, f⟩

Premises used: QPF.repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
h₁ :
  x =
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦
          (↑(f i) : α × α).1) ∧
    y =
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦
            (↑(f i) : α × α).2) ∧
      ∀ (i : (P F).B a), r (↑(f i) : α × α).1 ((fun (i : (P F).B a) ↦ (↑(f i) : α × α).2) i)
⊢ ∃ (a : PFunctor.A.{u, u_1} (P F)) (f₀ : (P F).B a → α) (f₁ : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀) ∧
      y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁) ∧
        ∀ (i : (P F).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.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
h₁ :
  x =
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).1)
h₂ :
  y =
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦
          (↑(f i) : α × α).2) ∧
    ∀ (i : (P F).B a), r (↑(f i) : α × α).1 (↑(f i) : α × α).2
⊢ x =
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦
          (↑(f i) : α × α).1) ∧
    y =
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦
            (↑(f i) : α × α).2) ∧
      ∀ (i : (P F).B a), r (↑(f i) : α × α).1 ((fun (i : (P F).B a) ↦ (↑(f i) : α × α).2) i)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
h₁ :
  Eq (α := F α)
    (abs
      ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f)))
    (abs
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).1))
⊢ x =
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).1)

Tactic:
rw [← xeq, ← abs_repr u, h, ← abs_map]

Premises used: QPF.abs_repr, QPF.abs_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
⊢ Eq (α := F α)
    (abs
      ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f)))
    (abs
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).1))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
h₁ :
  y =
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).2)
h₂ : ∀ (i : (P F).B a), r (↑(f i) : α × α).1 (↑(f i) : α × α).2
⊢ y =
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦
          (↑(f i) : α × α).2) ∧
    ∀ (i : (P F).B a), r (↑(f i) : α × α).1 (↑(f i) : α × α).2

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
h₁ :
  Eq (α := F α)
    (abs
      ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f)))
    (abs
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).2))
⊢ y =
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).2)

Tactic:
rw [← yeq, ← abs_repr u, h, ← abs_map]

Premises used: QPF.abs_repr, QPF.abs_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
⊢ Eq (α := F α)
    (abs
      ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f)))
    (abs
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α × α).2))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
i : (P F).B a
⊢ r (↑(f i) : α × α).1 (↑(f i) : α × α).2

Tactic:
(f i).property

Premises used: Subtype.property
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
u : F { 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 : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → { p : α × α // r p.1 p.2 }
h : repr u = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a f
i : (P F).B a
⊢ r (↑(f i) : α × α).1 (↑(f i) : α × α).2

Tactic:
exact (f i).property

Premises used: Subtype.property
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
h₁ :
  (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
            fun (i : (P F).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) <$>
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
            fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      y
⊢ Liftr r x y

Tactic:
use abs ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩

Premises used: QPF.abs, Sigma.mk
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
h₁ :
  (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).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) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).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) <$>
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
            fun (i : (P F).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) <$>
        abs
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
            fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
      y

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
h₁ :
  Eq (α := F α)
    (abs
      ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯)))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀))
⊢ (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
    x

Tactic:
rw [xeq, ← abs_map]

Premises used: QPF.abs_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Eq (α := F α)
    (abs
      ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).1)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯)))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
h₁ :
  Eq (α := F α)
    (abs
      ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯)))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁))
⊢ (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2) <$>
      abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯) =
    y

Tactic:
rw [yeq, ← abs_map]

Premises used: QPF.abs_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
a : PFunctor.A.{u, u_1} (P F)
f₀ f₁ : (P F).B a → α
xeq : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₀)
yeq : y = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁)
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Eq (α := F α)
    (abs
      ((P F).map (fun (t : { p : α × α // r p.1 p.2 }) ↦ (↑t : α × α).2)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → { p : α × α // r p.1 p.2 }) a
          fun (i : (P F).B a) ↦ Subtype.mk (p := fun (p : α × α) ↦ r p.1 p.2) (f₀ i, f₁ i) ⋯)))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f₁))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
g : F α → α
x : PFunctor.W.{u, u_1} (P F)
mk :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → WType.{u, u_1} (α := PFunctor.A.{u, u_1} (P F)) (P F).B),
    recF g (WType.mk (β := (P F).B) a f) = g (abs ((P F).map (recF g) (PFunctor.W.dest (WType.mk (β := (P F).B) a f))))
⊢ recF g x = g (abs ((P F).map (recF g) x.dest))

Tactic:
cases x
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
g : F α → α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → WType.{u, u_1} (α := PFunctor.A.{u, u_1} (P F)) (P F).B
⊢ recF g (WType.mk (β := (P F).B) a f) = g (abs ((P F).map (recF g) (PFunctor.W.dest (WType.mk (β := (P F).B) a f))))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
g : F α → α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → PFunctor.W.{u, u_1} (P F)
⊢ recF g (WType.mk (β := (P F).B) a f) =
    g
      (abs
        ((P F).map (α := PFunctor.W.{u, u_1} (P F)) (recF g)
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → PFunctor.W.{u, u_1} (P F)) a f)))

Tactic:
rfl

Premises used: QPF.recF, PFunctor.map, rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
a : (P F).A
f f' : (P F).B a → (P F).W
h : ∀ (x : (P F).B a), Wequiv (f x) (f' x)
ih : ∀ (x : (P F).B a), recF u (f x) = recF u (f' x)
⊢ recF u (WType.mk (β := (P F).B) a f) = recF u (WType.mk (β := (P F).B) a f')

Tactic:
simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]

Premises used: QPF.recF_eq', Function.comp_def, PFunctor.map_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
a : (P F).A
f : (P F).B a → (P F).W
a' : (P F).A
f' : (P F).B a' → (P F).W
h :
  Eq (α := F (P F).W) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))
    (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a' f'))
⊢ recF u (WType.mk (β := (P F).B) a f) = recF u (WType.mk (β := (P F).B) a' f')

Tactic:
simp only [recF_eq', abs_map, h]

Premises used: QPF.recF_eq', QPF.abs_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x_1 y_1 x y z : (P F).W
h : Wequiv x y
h_1 : Wequiv y z
ih₁ : recF u x = recF u y
ih₂ : recF u y = recF u z
⊢ recF u x = recF u z

Tactic:
Eq.trans ih₁ ih₂

Premises used: Eq.trans
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x_1 y_1 x y z : (P F).W
h : Wequiv x y
h_1 : Wequiv y z
ih₁ : recF u x = recF u y
ih₂ : recF u y = recF u z
⊢ recF u x = recF u z

Tactic:
exact Eq.trans ih₁ ih₂

Premises used: Eq.trans
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
h : Wequiv x y
ind :
  ∀ (a : (P F).A) (f f' : (P F).B a → (P F).W),
    (∀ (x : (P F).B a), Wequiv (f x) (f' x)) →
      ∀ (ih : ∀ (x : (P F).B a), recF u (f x) = recF u (f' x)),
        recF u (WType.mk (β := (P F).B) a f) = recF u (WType.mk (β := (P F).B) a f')
abs :
  ∀ (a : (P F).A) (f : (P F).B a → (P F).W) (a' : (P F).A) (f' : (P F).B a' → (P F).W)
    (h :
      Eq (α := F (P F).W) (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))
        (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a' f'))),
    recF u (WType.mk (β := (P F).B) a f) = recF u (WType.mk (β := (P F).B) a' f')
trans :
  ∀ (x y z : (P F).W),
    Wequiv x y → Wequiv y z → ∀ (ih₁ : recF u x = recF u y) (ih₂ : recF u y = recF u z), recF u x = recF u z
⊢ recF u x = recF u y

Tactic:
induction h with
  | ind a f f' _ ih => simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]
  | abs a f a' f' h => simp only [recF_eq', abs_map, h]
  | trans x y z _ _ ih₁ ih₂ => exact Eq.trans ih₁ ih₂

Premises used: QPF.recF_eq', QPF.abs_map, Function.comp_def, QPF.abs, PFunctor.map_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x y : (P F).W
h : QPF.abs x.dest = QPF.abs y.dest
mk :
  ∀ (a : (P F).A) (f : (P F).B a → WType (α := (P F).A) (P F).B)
    (h : QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) = QPF.abs y.dest),
    Wequiv (WType.mk (β := (P F).B) a f) y
⊢ Wequiv x y

Tactic:
cases x
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
y : (P F).W
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) = QPF.abs y.dest
mk :
  ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → WType (α := (P F).A) (P F).B)
    (h :
      QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) =
        QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a_1 f_1))),
    Wequiv (WType.mk (β := (P F).B) a f) (WType.mk (β := (P F).B) a_1 f_1)
⊢ Wequiv (WType.mk (β := (P F).B) a f) y

Tactic:
cases y
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
a_1 : (P F).A
f_1 : (P F).B a_1 → WType (α := (P F).A) (P F).B
h :
  QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) = QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a_1 f_1))
mk :
  Eq (α := F (P F).W) (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))
    (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a_1 f_1))
⊢ Wequiv (WType.mk (β := (P F).B) a f) (WType.mk (β := (P F).B) a_1 f_1)

Tactic:
apply Wequiv.abs

Premises used: QPF.Wequiv.abs
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
a_1 : (P F).A
f_1 : (P F).B a_1 → WType (α := (P F).A) (P F).B
h :
  QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a f)) = QPF.abs (PFunctor.W.dest (WType.mk (β := (P F).B) a_1 f_1))
⊢ Eq (α := F (P F).W) (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a f))
    (QPF.abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → (P F).W) a_1 f_1))

Tactic:
apply h
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
x : (P F).W
obtain :
  ∀ (a : (P F).A) (f : (P F).B a → WType (α := (P F).A) (P F).B),
    Wequiv (WType.mk (β := (P F).B) a f) (WType.mk (β := (P F).B) a f)
⊢ Wequiv x x

Tactic:
obtain ⟨a, f⟩ := x
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
⊢ Wequiv (WType.mk (β := (P F).B) a f) (WType.mk (β := (P F).B) a f)

Tactic:
Wequiv.abs a f a f rfl

Premises used: QPF.Wequiv.abs, rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
⊢ Wequiv (WType.mk (β := (P F).B) a f) (WType.mk (β := (P F).B) a f)

Tactic:
exact Wequiv.abs a f a f rfl

Premises used: QPF.Wequiv.abs, rfl