awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ :
  y =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).2)
h₂ : ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
⊢ y =
      abs (F := F) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
          (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ :
  Eq (α := F α)
    (abs (F := F) (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β :=
        α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f)))
    (abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).2))
⊢ y =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).2)

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

Premises used: MvQPF.abs_repr, MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ Eq (α := F α)
    (abs (F := F) (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β :=
        α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f)))
    (abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).2))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
i : Fin2 n
j : (P F).B a i
⊢ r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2

Tactic:
(f i j).property

Premises used: Subtype.property
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
i : Fin2 n
j : (P F).B a i
⊢ r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2

Tactic:
exact (f i j).property

Premises used: Subtype.property
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀)
yeq : y = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₁)
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
h₁ :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
        (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1)
        (abs (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
            fun (i : Fin2 n) (j : (P F).B a i) ↦
            Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)) =
      x ∧
    map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
        (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
        (abs (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
            fun (i : Fin2 n) (j : (P F).B a i) ↦
            Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)) =
      y
⊢ LiftR (F := F) (α := α) r x y

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

Premises used: Sigma.mk, MvQPF.abs
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀)
yeq : y = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₁)
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
h₁ :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1)
      (abs (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
          fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)) =
    x
h₂ :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
      (abs (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
          fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)) =
    y
⊢ map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
        (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1)
        (abs (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
            fun (i : Fin2 n) (j : (P F).B a i) ↦
            Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)) =
      x ∧
    map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
        (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
        (abs (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
            fun (i : Fin2 n) (j : (P F).B a i) ↦
            Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)) =
      y

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀)
yeq : y = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₁)
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
h₁ :
  Eq (α := F α)
    (abs (F := F) (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β :=
        α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
          fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)))
    (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀))
⊢ map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1)
      (abs (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
          fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)) =
    x

Tactic:
rw [xeq, ← abs_map]

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

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀)
yeq : y = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₁)
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
h₁ :
  Eq (α := F α)
    (abs (F := F) (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β :=
        α) (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
          fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)))
    (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₁))
⊢ map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2)
      (abs (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a
          fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := fun (p : α i × α i) ↦ r p.1 p.2) (f₀ i j, f₁ i j) ⋯)) =
    y

Tactic:
rw [yeq, ← abs_map]

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

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
mp :
  (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u) →
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α),
      abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x → u ∈ f i '' univ
mpr :
  (∀ (a : (P F).A) (f : (P F).B a ⟹ α),
      abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x → u ∈ f i '' univ) →
    ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u) ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α),
      abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x → u ∈ f i '' univ

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
rw :
  ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : (P F).B a_1 i), f_1 i j ∈ f i '' univ
⊢ LiftP (F := F) (α := α) (fun (i : Fin2 n) (u : α i) ↦ u ∈ f i '' univ) x

Tactic:
rw [liftP_iff]

Premises used: MvQPF.liftP_iff
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
⊢ ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : (P F).B a_1 i), f_1 i j ∈ f i '' univ

Tactic:
⟨a, f, haf.symm, ?_⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
refine : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ f i '' univ
⊢ ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a_1 f_1) ∧
      ∀ (i : Fin2 n) (j : (P F).B a_1 i), f_1 i j ∈ f i '' univ

Tactic:
refine ⟨a, f, haf.symm, ?_⟩
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i_1 : Fin2 n
u_1 : α i_1
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i_1 u_1
a : (P F).A
f : (P F).B a ⟹ α
haf : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
i : Fin2 n
u : (P F).B a i
⊢ f i u ∈ f i '' univ

Tactic:
mem_image_of_mem _ (mem_univ _)

Premises used: Set.mem_image_of_mem, Set.mem_univ
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i_1 : Fin2 n
u_1 : α i_1
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i_1 u_1
a : (P F).A
f : (P F).B a ⟹ α
haf : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
i : Fin2 n
u : (P F).B a i
⊢ f i u ∈ f i '' univ

Tactic:
exact mem_image_of_mem _ (mem_univ _)

Premises used: Set.mem_image_of_mem, Set.mem_univ
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
⊢ LiftP (F := F) (α := α) (fun (i : Fin2 n) (u : α i) ↦ u ∈ f i '' univ) x

Tactic:
have : LiftP (fun i u => u ∈ f i '' univ) x := by
      rw [liftP_iff]
      refine ⟨a, f, haf.symm, ?_⟩
      intro i u
      exact mem_image_of_mem _ (mem_univ _)
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
this : LiftP (F := F) (α := α) (fun (i : Fin2 n) (u : α i) ↦ u ∈ f i '' univ) x
⊢ u ∈ f i '' univ

Tactic:
h this
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u
a : (P F).A
f : (P F).B a ⟹ α
haf : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
this : LiftP (F := F) (α := α) (fun (i : Fin2 n) (u : α i) ↦ u ∈ f i '' univ) x
⊢ u ∈ f i '' univ

Tactic:
exact h this
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ (∀ (a : (P F).A) (f : (P F).B a ⟹ α),
      abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x → u ∈ f i '' univ) →
    ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP (F := F) (α := α) P x → P i u

Tactic:
grind [liftP_iff]

Premises used: MvQPF.liftP_iff
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
i : Fin2 n
x : F α
h :
  ∀ (x_1 : α i),
    x_1 ∈ supp (F := F) (α := α) x i ↔
      Membership.mem (γ := Set (α i))
        {u : α i |
          ∀ (a : (P F).A) (f : (P F).B a ⟹ α),
            abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x → u ∈ f i '' univ}
        x_1
⊢ supp (F := F) (α := α) x i =
    {u : α i |
      ∀ (a : (P F).A) (f : (P F).B a ⟹ α),
        abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x → u ∈ f i '' univ}

Tactic:
ext
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
i : Fin2 n
x : F α
x_1 : α i
⊢ x_1 ∈ supp (F := F) (α := α) x i ↔
    Membership.mem (γ := Set (α i))
      {u : α i |
        ∀ (a : (P F).A) (f : (P F).B a ⟹ α),
          abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x → u ∈ f i '' univ}
      x_1

Tactic:
apply mem_supp

Premises used: MvQPF.mem_supp
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
mp :
  (∀ (p : (i : Fin2 n) → α i → Prop),
      LiftP (F := F) (α := α) p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u) →
    ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α),
          abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') = x →
            f i '' univ ⊆ f' i '' univ
mpr :
  (∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α),
          abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') = x →
            f i '' univ ⊆ f' i '' univ) →
    ∀ (p : (i : Fin2 n) → α i → Prop),
      LiftP (F := F) (α := α) p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
⊢ (∀ (p : (i : Fin2 n) → α i → Prop),
      LiftP (F := F) (α := α) p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u) ↔
    ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α),
          abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') = x →
            f i '' univ ⊆ f' i '' univ

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h :
  ∀ (p : (i : Fin2 n) → α i → Prop),
    LiftP (F := F) (α := α) p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
rw : ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, supp (F := F) (α := α) x i u
⊢ LiftP (F := F) (α := α) (supp (F := F) (α := α) x) x

Tactic:
rw [h]