awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Quot
Goal:
n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (α := α) (FG_repr (α := α) x) = x
FG_abs_map :
  ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α),
    FG_abs (α := β) (map (F := F) (α := α) (β := β) f x) = map (F := G) (α := α) (β := β) f (FG_abs (α := α) x)
α β : TypeVec.{u} n
f : α ⟹ β
p : (↑(P F) : (α : TypeVec.{u} n) → Type u) α
rw :
  FG_abs (α := β) (map (F := F) (α := α) (β := β) f (abs (F := F) (α := α) p)) =
    map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p))
rw₁ rw₂ :
  map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p)) =
    map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p))
⊢ FG_abs (α := β) (abs (F := F) (α := β) (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f p)) =
    map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p))

Tactic:
rw [abs_map, FG_abs_map]

Premises used: MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma
Goal:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst_1 : (α : A) → MvQPF (F α)
α : TypeVec.{u} n
x : A
f : F x α
⊢ Eq (α := Sigma F α) (Sigma.abs F (α := α) (Sigma.repr F (α := α) (Sigma.mk (β := fun (α_1 : A) ↦ F α_1 α) x f)))
    (Sigma.mk (β := fun (α_1 : A) ↦ F α_1 α) x f)

Tactic:
simp only [Sigma.abs, Sigma.repr, Sigma.eta, abs_repr]

Premises used: MvQPF.Sigma.abs, MvQPF.Sigma.repr, Sigma.eta, MvQPF.abs_repr
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma
Goal:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst_1 : (α : A) → MvQPF (F α)
α β : TypeVec.{u} n
f : α ⟹ β
x : (Sigma.P F).A
g : (Sigma.P F).B x ⟹ α
⊢ Eq (α := Sigma F β)
    (Sigma.mk (β := fun (α : A) ↦ F α β) (x.fst (β := fun (a : A) ↦ (P (F a)).A))
      (abs (F := F (x.fst (β := fun (a : A) ↦ (P (F a)).A))) (α := β)
        (Sigma.mk (β := fun (a : (P (F (x.fst (β := fun (a : A) ↦ (P (F a)).A)))).A) ↦
          (P (F (x.fst (β := fun (a : A) ↦ (P (F a)).A)))).B a ⟹ β) (x.snd (β := fun (a : A) ↦ (P (F a)).A))
          (TypeVec.comp (α := (Sigma.P F).B x) (β := α) (γ := β) f g))))
    (map (F := Sigma F) (α := α) (β := β) f
      (Sigma.mk (β := fun (α_1 : A) ↦ F α_1 α) (x.fst (β := fun (a : A) ↦ (P (F a)).A))
        (abs (F := F (x.fst (β := fun (a : A) ↦ (P (F a)).A))) (α := α)
          (Sigma.mk (β := fun (a : (P (F (x.fst (β := fun (a : A) ↦ (P (F a)).A)))).A) ↦
            (P (F (x.fst (β := fun (a : A) ↦ (P (F a)).A)))).B a ⟹ α) (x.snd (β := fun (a : A) ↦ (P (F a)).A)) g))))

Tactic:
simp only [(· <$$> ·), ← abs_map, ← MvPFunctor.map_eq]

Premises used: MvPFunctor.map_eq, MvQPF.abs_map, MvFunctor.map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma
Goal:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst_1 : (α : A) → MvQPF (F α)
α : TypeVec.{u} n
f : Pi F α
⊢ Pi.abs F (α := α) (Pi.repr F (α := α) f) = f

Tactic:
simp +instances only [Pi.abs, Pi.repr, Sigma.eta, abs_repr]

Premises used: Sigma.eta, MvQPF.abs_repr, MvQPF.Pi.repr, MvQPF.Pi.abs
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma
Goal:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst_1 : (α : A) → MvQPF (F α)
α β : TypeVec.{u} n
f : α ⟹ β
x : (Pi.P F).A
g : (Pi.P F).B x ⟹ α
simp :
  Eq (α := Pi F β)
    (match (motive := (↑(Pi.P F) : (α : TypeVec.{u} n) → Type u) β → Pi F β)
        (Pi.P F).map (α := α) (β := β) f (Sigma.mk (β := fun (a : (Pi.P F).A) ↦ (Pi.P F).B a ⟹ α) x g) with
      | ⟨a, f⟩ => fun (x : A) ↦
        abs (F := F x) (α := β)
          (Sigma.mk (β := fun (a : (P (F x)).A) ↦ (P (F x)).B a ⟹ β) (a x) fun (i : Fin2 n) (y : (P (F x)).B (a x) i) ↦
            f i (Sigma.mk (β := fun (a_1 : A) ↦ (P (F a_1)).B (a a_1) i) x y)) :
      Pi F β)
    fun (a : A) ↦
    abs (F := F a) (α := β)
      ((P (F a)).map (α := α) (β := β) f
        (Sigma.mk (β := fun (a_1 : (P (F a)).A) ↦ (P (F a)).B a_1 ⟹ α) (x a)
          fun (i : Fin2 n) (y : (P (F a)).B (x a) i) ↦ g i (Sigma.mk (β := fun (a : A) ↦ (P (F a)).B (x a) i) a y)))
⊢ Pi.abs F (α := β)
      (map (F := (↑(Pi.P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f
        (Sigma.mk (β := fun (a : (Pi.P F).A) ↦ (Pi.P F).B a ⟹ α) x g)) =
    map (F := Pi F) (α := α) (β := β) f
      (Pi.abs F (α := α) (Sigma.mk (β := fun (a : (Pi.P F).A) ↦ (Pi.P F).B a ⟹ α) x g))

Tactic:
simp only [Pi.abs, (· <$$> ·), ← abs_map]

Premises used: MvQPF.abs_map, MvQPF.Pi.abs, MvFunctor.map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma
Goal:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst_1 : (α : A) → MvQPF (F α)
α β : TypeVec.{u} n
f : α ⟹ β
x : (Pi.P F).A
g : (Pi.P F).B x ⟹ α
⊢ Eq (α := Pi F β)
    (match (motive := (↑(Pi.P F) : (α : TypeVec.{u} n) → Type u) β → Pi F β)
        (Pi.P F).map (α := α) (β := β) f (Sigma.mk (β := fun (a : (Pi.P F).A) ↦ (Pi.P F).B a ⟹ α) x g) with
      | ⟨a, f⟩ => fun (x : A) ↦
        abs (F := F x) (α := β)
          (Sigma.mk (β := fun (a : (P (F x)).A) ↦ (P (F x)).B a ⟹ β) (a x) fun (i : Fin2 n) (y : (P (F x)).B (a x) i) ↦
            f i (Sigma.mk (β := fun (a_1 : A) ↦ (P (F a_1)).B (a a_1) i) x y)) :
      Pi F β)
    fun (a : A) ↦
    abs (F := F a) (α := β)
      ((P (F a)).map (α := α) (β := β) f
        (Sigma.mk (β := fun (a_1 : (P (F a)).A) ↦ (P (F a)).B a_1 ⟹ α) (x a)
          fun (i : Fin2 n) (y : (P (F a)).B (x a) i) ↦ g i (Sigma.mk (β := fun (a : A) ↦ (P (F a)).B (x a) i) a y)))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
x : F α
rw : id <$> abs.{u, u_1, v} (repr x) = abs.{u, u_1, v} (repr x)
⊢ id <$> x = x

Tactic:
rw [← abs_repr x]

Premises used: QPF.abs_repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
x : F α
obtain :
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    Eq (α := F α) (id <$> abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
      (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
⊢ id <$> abs.{u, u_1, v} (repr x) = abs.{u, u_1, v} (repr x)

Tactic:
obtain ⟨a, f⟩ := repr x

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
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
rw :
  Eq (α := F α) (abs ((P F).map id (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
⊢ Eq (α := F α) (id <$> abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))

Tactic:
rw [← 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
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
⊢ Eq (α := F α) (abs ((P F).map id (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
    (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
f : α → β
g : β → γ
x : F α
rw : (g ∘ f) <$> abs.{u, u_1, v} (repr x) = g <$> f <$> abs.{u, u_1, v} (repr x)
⊢ (g ∘ f) <$> x = g <$> f <$> x

Tactic:
rw [← abs_repr x]

Premises used: QPF.abs_repr
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α β γ : Type u
f : α → β
g : β → γ
x : F α
rw : abs.{u, u_1, v} ((P F).map (g ∘ f) (repr x)) = abs.{u, u_1, v} ((P F).map g ((P F).map f (repr x)))
⊢ (g ∘ f) <$> abs.{u, u_1, v} (repr x) = g <$> f <$> abs.{u, u_1, v} (repr x)

Tactic:
rw [← abs_map, ← abs_map, ← 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
f : α → β
g : β → γ
x : F α
⊢ abs.{u, u_1, v} ((P F).map (g ∘ f) (repr x)) = abs.{u, u_1, v} ((P F).map g ((P F).map f (repr x)))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
h : ∀ (α β : Type u), Eq (α := α → F β → F α) Functor.mapConst (Functor.map ∘ Function.const β)
⊢ LawfulFunctor F

Tactic:
{ map_const := @h
    id_map := @id_map F _
    comp_map := @comp_map F _ }

Premises used: LawfulFunctor.mk, QPF.comp_map, QPF.id_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
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)
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
⊢ 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)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
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
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)
⊢ ∃ (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⟩

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
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) : α)) ∧
    ∀ (i : (P F).B a), p ((fun (i : (P F).B a) ↦ (↑(f i) : α)) i)
⊢ ∃ (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:
use a, fun i => (f i).val

Premises used: Subtype.val
-- Module: Mathlib.Data.QPF.Univariate.Basic
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) : α))
h₂ : ∀ (i : (P F).B a), p (↑(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)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
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₁ :
  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) : α)))
⊢ 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:
rw [← hy, ← abs_repr y, 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
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
⊢ 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:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
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
i : (P F).B a
⊢ p (↑(f i) : α)

Tactic:
apply (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
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)
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) ⋯)) =
    x
⊢ Liftp p x

Tactic:
use abs ⟨a, fun 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
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)
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) ⋯)))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
⊢ 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

Tactic:
rw [← abs_map, h₀]

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
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)
⊢ 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) ⋯)))
    (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
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)
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
⊢ 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
-- Module: Mathlib.Data.QPF.Univariate.Basic
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
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)
⊢ ∃ (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⟩

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
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 ∧
    ∀
      (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)
⊢ ∃ (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:
use ⟨a, fun i => (f i).val⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
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 ∧
    ∀ (i : (P F).B a), p (↑(f i) : α)
⊢ 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:
dsimp
-- Module: Mathlib.Data.QPF.Univariate.Basic
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
h₂ : ∀ (i : (P F).B a), p (↑(f i) : α)
⊢ 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:
constructor
-- Module: Mathlib.Data.QPF.Univariate.Basic
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₁ :
  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)))
⊢ 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:
rw [← hy, ← abs_repr y, 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
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
⊢ 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:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
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)
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) ⋯)) =
    x
⊢ Liftp p x

Tactic:
use abs ⟨a, fun 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
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)
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) ⋯)))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
⊢ 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

Tactic:
rw [← abs_map, ← h₀]

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
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)
⊢ 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) ⋯)))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))

Tactic:
rfl