awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
mp :
  Liftp p x →
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)
⊢ Liftp p x ↔
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)
have mpr : (∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)) →
  Liftp p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
⊢ ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)
have mp : ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → Subtype p)
  (h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a f),
  ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)
Tactic: rcases h : repr y with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a f
⊢ ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)
have 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) : α)) ∧
  ∀ (i : (P F).B a), p ((fun (i : (P F).B a) ↦ (↑(f i) : α)) i)
Tactic: use a, fun i => (f i).val
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a f
⊢ 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) : α)) ∧
    ∀ (i : (P F).B a), p ((fun (i : (P F).B a) ↦ (↑(f i) : α)) i)
have 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) : α))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) 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) : α))
⊢ 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) : α)) ∧
    ∀ (i : (P F).B a), p ((fun (i : (P F).B a) ↦ (↑(f i) : α)) i)
have h₂ : ∀ (i : (P F).B a), p (↑(f i) : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a f
⊢ 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) : α))
have h₁ : Eq (α := F α)
  (abs
    ((P F).map (α := Subtype p) (Subtype.val (p := p))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) 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) : α)))
Tactic: rw [← hy, ← abs_repr y, h, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h₀ : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Liftp p x
have h : map (α := Subtype p) (Subtype.val (p := p))
    (abs
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a fun (i : (P F).B a) ↦
        Subtype.mk (p := p) (f i) sorry)) =
  x
Tactic: use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h₀ : x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ map (α := Subtype p) (Subtype.val (p := p))
      (abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a fun (i : (P F).B a) ↦
          Subtype.mk (p := p) (f i) ⋯)) =
    x
have h : Eq (α := F α)
  (abs
    ((P F).map (α := Subtype p) (Subtype.val (p := p))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a fun (i : (P F).B a) ↦
        Subtype.mk (p := p) (f i) sorry)))
  (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
Tactic: rw [← abs_map, h₀]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x ↔
    ∃ (u : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
      abs u = x ∧
        ∀ (i : (P F).B (u.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α))),
          p (u.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) i)
have mp : Liftp p x →
  ∃ (u : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
    abs u = x ∧
      ∀ (i : (P F).B (u.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α))),
        p (u.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
mp :
  Liftp p x →
    ∃ (u : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
      abs u = x ∧
        ∀ (i : (P F).B (u.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α))),
          p (u.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) i)
⊢ Liftp p x ↔
    ∃ (u : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
      abs u = x ∧
        ∀ (i : (P F).B (u.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α))),
          p (u.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) i)
have mpr : (∃ (u : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
    abs u = x ∧
      ∀ (i : (P F).B (u.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α))),
        p (u.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) i)) →
  Liftp p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
⊢ ∃ (u : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
    abs u = x ∧
      ∀ (i : (P F).B (u.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α))),
        p (u.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) i)
have mp : ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → Subtype p)
  (h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a f),
  ∃ (u : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
    abs u = x ∧
      ∀ (i : (P F).B (u.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α))),
        p (u.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) i)
Tactic: rcases h : repr y with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a f
⊢ ∃ (u : (↑(P F) : (α : Type u) → Type (max u u_1)) α),
    abs u = x ∧
      ∀ (i : (P F).B (u.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α))),
        p (u.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) i)
have h₁ : 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) : α)) = x ∧
  ∀
    (i :
      (P F).B
        (Sigma.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α)
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α)))),
    p
      (Sigma.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α)
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α)) i)
Tactic: use ⟨a, fun i => (f i).val⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) 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) : α)) = x ∧
    ∀
      (i :
        (P F).B
          (Sigma.fst (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α)
            (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦
              (↑(f i) : α)))),
      p
        (Sigma.snd (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α)
          (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a fun (i : (P F).B a) ↦ (↑(f i) : α)) i)
have h₁ : 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) : α)) = x ∧
  ∀ (i : (P F).B a), p (↑(f i) : α)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) 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) : α)) = x ∧
    ∀ (i : (P F).B a), p (↑(f i) : α)
have h₁ : 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) : α)) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a f
h₁ : 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) : α)) = 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) : α)) = x ∧
    ∀ (i : (P F).B a), p (↑(f i) : α)
have h₂ : ∀ (i : (P F).B a), p (↑(f i) : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val (p := p) <$> y = x
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → Subtype p
h : repr y = Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) 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) : α)) = x
have h₁ : Eq (α := 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) : α)))
  (abs
    ((P F).map (α := Subtype p) (Subtype.val (p := p))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a f)))
Tactic: rw [← hy, ← abs_repr y, h, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h₀ : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Liftp p x
have h : map (α := Subtype p) (Subtype.val (p := p))
    (abs
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a fun (i : (P F).B a) ↦
        Subtype.mk (p := p) (f i) sorry)) =
  x
Tactic: use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
h₀ : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ map (α := Subtype p) (Subtype.val (p := p))
      (abs
        (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a fun (i : (P F).B a) ↦
          Subtype.mk (p := p) (f i) ⋯)) =
    x
have h : Eq (α := F α)
  (abs
    ((P F).map (α := Subtype p) (Subtype.val (p := p))
      (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → Subtype p) a fun (i : (P F).B a) ↦
        Subtype.mk (p := p) (f i) sorry)))
  (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
Tactic: rw [← abs_map, ← h₀]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
r : α → α → Prop
x y : F α
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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 → α) (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)
have 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)
Tactic: rcases h : repr u with ⟨a, f⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use a, fun i => (f i).val.fst, fun i => (f i).val.snd
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ 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)
have 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))
Tactic: rw [← xeq, ← abs_repr u, h, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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
⊢ 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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
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)
⊢ 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
have h₂ : ∀ (i : (P F).B a), r (↑(f i) : α × α).1 (↑(f i) : α × α).2
Tactic: constructor