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
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
i : Fin2 n
u : α i
⊢ u ∈ supp (F := F) (α := α) x i → supp (F := F) (α := α) x i u

Tactic:
id

Premises used: Set.Mem, setOf, MvFunctor.supp, id
-- 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
i : Fin2 n
u : α i
⊢ u ∈ supp (F := F) (α := α) x i → supp (F := F) (α := α) x i u

Tactic:
exact id

Premises used: id
-- 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
⊢ LiftP (F := F) (α := α) (supp (F := F) (α := α) x) x

Tactic:
have : LiftP (supp x) x := by rw [h]; introv; exact id
-- 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
this : LiftP (F := F) (α := α) (supp (F := F) (α := α) x) x
⊢ ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
      ∀ (i : Fin2 n) (j : (P F).B a i), supp (F := F) (α := α) x i (f i j)

Tactic:
rw [liftP_iff] at this

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 α
h :
  ∀ (p : (i : Fin2 n) → α i → Prop),
    LiftP (F := F) (α := α) p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
this :
  ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
      ∀ (i : Fin2 n) (j : (P F).B a i), supp (F := F) (α := α) x i (f i j)
mp :
  ∀ (a : (P F).A) (f : (P F).B a ⟹ α)
    (xeq : x = 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), supp (F := F) (α := α) x i (f i j)),
    ∃ (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
⊢ ∃ (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:
rcases this with ⟨a, f, xeq, h'⟩
-- 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
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = 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), supp (F := F) (α := α) x i (f i j)
⊢ ∃ (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:
⟨a, f, xeq.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 α
h :
  ∀ (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 ⟹ α
xeq : x = 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), supp (F := F) (α := α) x i (f i j)
mp :
  ∀ (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
⊢ ∃ (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:
refine ⟨a, f, xeq.symm, ?_⟩
-- 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
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = 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), supp (F := F) (α := α) x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) f' h'') = x
u : α a'
j : (P F).B a a'
_h₂ : Membership.mem (γ := Set ((P F).B a a')) univ j
hfi : f a' j = u
rw : f a' j ∈ supp (F := F) (α := α) x a'
⊢ u ∈ supp (F := F) (α := α) x a'

Tactic:
rw [← hfi]
-- 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
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = 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), supp (F := F) (α := α) x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) f' h'') = x
u : α a'
j : (P F).B a a'
_h₂ : Membership.mem (γ := Set ((P F).B a a')) univ j
hfi : f a' j = u
⊢ f a' j ∈ supp (F := F) (α := α) x a'

Tactic:
apply h'
-- 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
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = 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), supp (F := F) (α := α) x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) f' h'') = x
u : α a'
j : (P F).B a a'
_h₂ : Membership.mem (γ := Set ((P F).B a a')) univ j
hfi : f a' j = u
⊢ u ∈ supp (F := F) (α := α) x a'

Tactic:
have hh : u ∈ supp x a' := by rw [← hfi]; apply h'
-- 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
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = 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), supp (F := F) (α := α) x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) f' h'') = x
u : α a'
j : (P F).B a a'
_h₂ : Membership.mem (γ := Set ((P F).B a a')) univ j
hfi : f a' j = u
hh : u ∈ supp (F := F) (α := α) x a'
⊢ u ∈ h'' a' '' univ

Tactic:
(mem_supp x _ u).mp hh _ _ hu

Premises used: MvQPF.mem_supp, Iff.mp
-- 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
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = 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), supp (F := F) (α := α) x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) f' h'') = x
u : α a'
j : (P F).B a a'
_h₂ : Membership.mem (γ := Set ((P F).B a a')) univ j
hfi : f a' j = u
hh : u ∈ supp (F := F) (α := α) x a'
⊢ u ∈ h'' a' '' univ

Tactic:
exact (mem_supp x _ u).mp hh _ _ hu

Premises used: MvQPF.mem_supp, Iff.mp
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
mpr :
  (∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
        ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
⊢ LiftP (F := F) (α := α) p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u

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 α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
mpr :
  (∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
        ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) →
    ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
mpr₁ :
  (∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u) →
    ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
        ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
⊢ (∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
        ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u

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 α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : x = 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), p i (f' i j)
i : Fin2 n
u : α i
usuppx : u ∈ supp (F := F) (α := α) x i
mpr : ∀ (i_1 : (P F).B a' i), Membership.mem (γ := Set ((P F).B a' i)) univ i_1 → ∀ (f'ieq : f' i i_1 = u), p i u
⊢ p i u

Tactic:
rcases (mem_supp x _ u).mp (@usuppx) a' f' xeq'.symm with ⟨i, _, f'ieq⟩

Premises used: MvQPF.mem_supp, Iff.mp, 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 α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : x = 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), p i (f' i j)
i_1 : Fin2 n
u : α i_1
usuppx : u ∈ supp (F := F) (α := α) x i_1
i : (P F).B a' i_1
left : Membership.mem (γ := Set ((P F).B a' i_1)) univ i
f'ieq : f' i_1 i = u
mpr : p i_1 (f' i_1 i)
⊢ p i_1 u

Tactic:
rw [← f'ieq]
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : x = 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), p i (f' i j)
i_1 : Fin2 n
u : α i_1
usuppx : u ∈ supp (F := F) (α := α) x i_1
i : (P F).B a' i_1
left : Membership.mem (γ := Set ((P F).B a' i_1)) univ i
f'ieq : f' i_1 i = u
⊢ p i_1 (f' i_1 i)

Tactic:
apply h'
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
⊢ ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
      ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)

Tactic:
⟨a, f, xeq.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 α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
mpr : ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
⊢ ∃ (a : (P F).A) (f : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
      ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)

Tactic:
refine ⟨a, f, xeq.symm, ?_⟩
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
j : Fin2 n
y : (P F).B a j
mpr : f j y ∈ supp (F := F) (α := α) x j
⊢ p j (f j y)

Tactic:
apply h'
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
j : Fin2 n
y : (P F).B a j
mpr :
  ∀ (a : (P F).A) (f_1 : (P F).B a ⟹ α),
    abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f_1) = x → f j y ∈ f_1 j '' univ
⊢ f j y ∈ supp (F := F) (α := α) x j

Tactic:
rw [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 α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
j : Fin2 n
y : (P F).B a j
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') = x
mpr : f j y ∈ f j '' univ
⊢ f j y ∈ f' j '' univ

Tactic:
apply h _ a' f' xeq'
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) = x
h :
  ∀ (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
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
j : Fin2 n
y : (P F).B a j
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') = x
⊢ f j y ∈ f j '' univ

Tactic:
apply 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
h : IsUniform (F := F)
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i : Fin2 n
h₁ :
  ∀ (u : α i),
    Membership.mem (γ := Set (α i))
        (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i) u ↔
      u ∈ f i '' univ
⊢ supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i = f i '' univ

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

Tactic:
rw [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
h : IsUniform (F := F)
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i : Fin2 n
u : α i
h₁ :
  (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α),
      Eq (α := F α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a_1 f_1))
          (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) →
        u ∈ f_1 i '' univ) →
    u ∈ f i '' univ
h₂ :
  u ∈ f i '' univ →
    ∀ (a_2 : (P F).A) (f_1 : (P F).B a_2 ⟹ α),
      Eq (α := F α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a_2 f_1))
          (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) →
        u ∈ f_1 i '' univ
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α),
      Eq (α := F α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a_1 f_1))
          (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) →
        u ∈ f_1 i '' univ) ↔
    u ∈ f i '' univ

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

Tactic:
apply h' _ _ rfl

Premises used: rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform (F := F)
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i : Fin2 n
u : α i
h' : u ∈ f i '' univ
a' : (P F).A
f' : (P F).B a' ⟹ α
e :
  Eq (α := F α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f'))
    (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))
h₁ : u ∈ f i '' univ
⊢ u ∈ f' i '' univ

Tactic:
rw [← h _ _ _ _ e.symm]

Premises used: Eq.symm
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform (F := F)
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i : Fin2 n
u : α i
h' : u ∈ f i '' univ
a' : (P F).A
f' : (P F).B a' ⟹ α
e :
  Eq (α := F α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f'))
    (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))
⊢ u ∈ f i '' univ

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

Tactic:
rw [liftP_iff, ← abs_repr x]

Premises used: MvQPF.abs_repr, MvQPF.liftP_iff
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform (F := F)
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
obtain :
  ∀ (a : (P F).A) (f : (P F).B a ⟹ α),
    (∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α),
        Eq (α := F α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))
            (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), p i (f_1 i j)) ↔
      ∀ (i : Fin2 n) (u : α i),
        Membership.mem (γ := Set (α i))
            (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i)
            u →
          p i u
⊢ (∃ (a : (P F).A) (f : (P F).B a ⟹ α),
      abs (F := F) (α := α) (repr (F := F) (α := α) x) =
          abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) ∧
        ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) (abs (F := F) (α := α) (repr (F := F) (α := α) x)) i, p i u

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

Premises used: MvQPF.repr