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
h : IsUniform (F := F)
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
mp :
  (∃ (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
mpr :
  (∀ (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_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 f))
          (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a_2 f_1)) ∧
        ∀ (i : Fin2 n) (j : (P F).B a_2 i), p i (f_1 i j)
⊢ (∃ (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

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

Tactic:
rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]

Premises used: MvQPF.supp_eq_of_isUniform
-- 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
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq :
  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'))
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left : Membership.mem (γ := Set ((P F).B a' u)) univ i
hi : f' u i = b
mp : p u (f' u i)
⊢ p u b

Tactic:
rw [← hi]
-- 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
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq :
  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'))
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left : Membership.mem (γ := Set ((P F).B a' u)) univ i
hi : f' u i = b
⊢ p u (f' u i)

Tactic:
apply hf
-- 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
a : (P F).A
f : (P F).B a ⟹ α
h' :
  ∀ (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_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)

Tactic:
⟨a, f, rfl, fun _ i => h' _ _ ?_⟩

Premises used: And.intro, Exists.intro, 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
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' :
  ∀ (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
mpr :
  ∀ (x : Fin2 n) (i : (P F).B a x),
    Membership.mem (γ := Set (α x))
      (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x) (f x i)
⊢ ∃ (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)

Tactic:
refine ⟨a, f, rfl, fun _ i => 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
a : (P F).A
f : (P F).B a ⟹ α
h' :
  ∀ (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
x_1 : Fin2 n
i : (P F).B a x_1
mpr : f x_1 i ∈ f x_1 '' univ
⊢ Membership.mem (γ := Set (α x_1))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x_1)
    (f x_1 i)

Tactic:
rw [supp_eq_of_isUniform h]

Premises used: MvQPF.supp_eq_of_isUniform
-- 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
a : (P F).A
f : (P F).B a ⟹ α
h' :
  ∀ (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
x_1 : Fin2 n
i : (P F).B a x_1
⊢ f x_1 i ∈ f x_1 '' univ

Tactic:
⟨i, mem_univ i, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.mem_univ, Set.image, 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
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' :
  ∀ (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
x_1 : Fin2 n
i : (P F).B a x_1
⊢ f x_1 i ∈ f x_1 '' univ

Tactic:
exact ⟨i, mem_univ i, 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
g : α ⟹ β
x : F α
i : Fin2 n
rw :
  supp (F := F) (α := β) (map (F := F) (α := α) (β := β) g (abs (F := F) (α := α) (repr (F := F) (α := α) x))) i =
    g i '' supp (F := F) (α := α) (abs (F := F) (α := α) (repr (F := F) (α := α) x)) i
⊢ supp (F := F) (α := β) (map (F := F) (α := α) (β := β) g x) i = g i '' supp (F := F) (α := α) x i

Tactic:
rw [← abs_repr x]

Premises used: MvQPF.abs_repr
-- 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
g : α ⟹ β
x : F α
i : Fin2 n
obtain :
  ∀ (a : (P F).A) (f : (P F).B a ⟹ α),
    supp (F := F) (α := β)
        (map (F := F) (α := α) (β := β) g
          (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)))
        i =
      g i '' supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i
⊢ supp (F := F) (α := β) (map (F := F) (α := α) (β := β) g (abs (F := F) (α := α) (repr (F := F) (α := α) x))) i =
    g i '' supp (F := F) (α := α) (abs (F := F) (α := α) (repr (F := F) (α := α) x)) i

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

Premises used: MvQPF.repr
-- 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
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
rw :
  supp (F := F) (α := β)
      (abs (F := F) (α := β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ β) a (TypeVec.comp (α := (P F).B a) (β := α) (γ := β) g f)))
      i =
    g i '' supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i
⊢ supp (F := F) (α := β)
      (map (F := F) (α := α) (β := β) g (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)))
      i =
    g i '' supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i

Tactic:
rw [← abs_map, MvPFunctor.map_eq]

Premises used: MvPFunctor.map_eq, MvQPF.abs_map
-- 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
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
rw : TypeVec.comp (α := (P F).B a) (β := α) (γ := β) g f i '' univ = g i ∘ f i '' univ
⊢ supp (F := F) (α := β)
      (abs (F := F) (α := β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ β) a (TypeVec.comp (α := (P F).B a) (β := α) (γ := β) g f)))
      i =
    g i '' supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i

Tactic:
rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, ← image_comp]

Premises used: Set.image_comp, MvQPF.supp_eq_of_isUniform
-- 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
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ TypeVec.comp (α := (P F).B a) (β := α) (γ := β) g f i '' univ = g i ∘ f i '' univ

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
mp : SuppPreservation (F := F) → IsUniform (F := F)
mpr : IsUniform (F := F) → SuppPreservation (F := F)
⊢ SuppPreservation (F := F) ↔ IsUniform (F := F)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation (F := F)
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' :
  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'))
i : Fin2 n
mp :
  supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)
      i =
    f' i '' univ
mp₁ :
  Eq.{u + 1} (α := Set (α i))
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) i)
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
mp₂ :
  Eq (α := Set (α i))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i)
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
mp₃ :
  Eq (α := Set (α i))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f')) i)
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
mp₄ mp₅ :
  Eq.{u + 1} (α := Set (α i))
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a' f') i)
⊢ f i '' univ = f' i '' univ

Tactic:
rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]

Premises used: MvPFunctor.supp_eq
-- 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 ⟹ α
mpr :
  ∀ (x : Fin2 n) (x_1 : α x),
    Membership.mem (γ := Set (α x))
        (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x) x_1 ↔
      Membership.mem (γ := Set (α x))
        (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
        x_1
⊢ Eq (α := (i : Fin2 n) → Set (α i))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)))
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))

Tactic:
ext
-- 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 ⟹ α
x : Fin2 n
x_1 : α x
mpr :
  x_1 ∈ f x '' univ ↔
    Membership.mem (γ := Set (α x))
      (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
      x_1
mpr₁ : IsUniform (F := F)
mpr₂ : x_1 ∈ f x '' univ ↔ x_1 ∈ f x '' univ
mpr₃ : IsUniform (F := F)
mpr₄ : x_1 ∈ f x '' univ ↔ x_1 ∈ f x '' univ
mpr₅ mpr₆ mpr₇ : IsUniform (F := F)
⊢ Membership.mem (γ := Set (α x))
      (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x) x_1 ↔
    Membership.mem (γ := Set (α x))
      (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
      x_1

Tactic:
rwa [supp_eq_of_isUniform, MvPFunctor.supp_eq]

Premises used: MvPFunctor.supp_eq, MvQPF.supp_eq_of_isUniform
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
mp : SuppPreservation (F := F) → LiftPPreservation (F := F)
mpr : LiftPPreservation (F := F) → SuppPreservation (F := F)
⊢ SuppPreservation (F := F) ↔ LiftPPreservation (F := F)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation (F := F)
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ SuppPreservation (F := F)

Tactic:
have h' := h
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation (F := F)
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : SuppPreservation (F := F)
⊢ IsUniform (F := F)

Tactic:
rw [suppPreservation_iff_isUniform] at h'

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

Tactic:
simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h',
      image_univ, mem_range, exists_imp]

Premises used: Set.image_univ, Set.mem_range, MvPFunctor.liftP_iff', MvQPF.supp_eq_of_isUniform, exists_imp, MvQPF.liftP_iff_of_isUniform
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    supp (F := F) (α := α) (abs (F := F) (α := α) x) = supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform (F := F)
mp : (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) → ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
mp₁ : (∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)) → ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    supp (F := F) (α := α) (abs (F := F) (α := α) x) = supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform (F := F)
h_1 : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i : Fin2 n
u : α i
x : (P F).B a i
h_2 : f i x = u
mp : p (f i x)
⊢ p u

Tactic:
subst_vars
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    supp (F := F) (α := α) (abs (F := F) (α := α) x) = supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform (F := F)
h_1 : ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
i : Fin2 n
x : (P F).B a i
⊢ p (f i x)

Tactic:
solve_by_elim
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    supp (F := F) (α := α) (abs (F := F) (α := α) x) = supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform (F := F)
h_1 : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i : Fin2 n
x : (P F).B a i
⊢ p (f i x)

Tactic:
solve_by_elim
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h :
  ∀ ⦃α : TypeVec.{u} n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : (↑(P F) : (α : TypeVec.{u} n) → Type u) α),
    LiftP (F := F) (α := α) p (abs (F := F) (α := α) x) ↔
      LiftP (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) p x
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
mpr :
  ∀ (x : Fin2 n) (x_1 : α x),
    Membership.mem (γ := Set (α x))
        (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) x) x_1 ↔
      Membership.mem (γ := Set (α x))
        (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f) x)
        x_1
⊢ Eq (α := (i : Fin2 n) → Set (α i))
    (supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)))
    (supp (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))

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

Tactic:
simp only [supp, h, mem_setOf_eq]

Premises used: MvFunctor.supp, Set.mem_setOf_eq
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
rw : SuppPreservation (F := F) ↔ IsUniform (F := F)
rw₁ rw₂ : IsUniform (F := F) ↔ IsUniform (F := F)
⊢ LiftPPreservation (F := F) ↔ IsUniform (F := F)

Tactic:
rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform]

Premises used: MvQPF.suppPreservation_iff_liftpPreservation, MvQPF.suppPreservation_iff_isUniform
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F_1 : TypeVec.{u} n → Type u_1
q_1 : MvQPF F_1
F : TypeVec.{u} n → Type u_2
F' : TypeVec.{u} n → Type u_3
q : MvQPF F'
inst : MvFunctor F
eqv : (α : TypeVec.{u} n) → Equiv.{u_2 + 1, u_3 + 1} (F α) (F' α)
map_eq :
  ∀ (α β : TypeVec.{u} n) (f : α ⟹ β) (a : F α),
    map (F := F) (α := α) (β := β) f a =
      ((eqv β).symm : (a : F' β) → F β) (map (F := F') (α := α) (β := β) f ((eqv α : (a : F α) → F' α) a))
⊢ ∀ {α : TypeVec.{u} n} (x : F α),
    ((eqv α).symm : (a : F' α) → F α)
        (abs (F := F') (α := α) (repr (F := F') (α := α) ((eqv α : (a : F α) → F' α) x))) =
      x

Tactic:
simp [q.abs_repr]

Premises used: MvQPF.abs_repr
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F_1 : TypeVec.{u} n → Type u_1
q_1 : MvQPF F_1
F : TypeVec.{u} n → Type u_2
F' : TypeVec.{u} n → Type u_3
q : MvQPF F'
inst : MvFunctor F
eqv : (α : TypeVec.{u} n) → Equiv.{u_2 + 1, u_3 + 1} (F α) (F' α)
map_eq :
  ∀ (α β : TypeVec.{u} n) (f : α ⟹ β) (a : F α),
    map (F := F) (α := α) (β := β) f a =
      ((eqv β).symm : (a : F' β) → F β) (map (F := F') (α := α) (β := β) f ((eqv α : (a : F α) → F' α) a))
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : (↑(P F') : (α : TypeVec.{u} n) → Type u) α),
    Eq.{u_2 + 1} (α := F β)
      (((eqv β).symm : (a : F' β) → F β)
          (abs (F := F') (α := β) (map (F := (↑(P F') : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f p)) :
        F β)
      (map (F := F) (α := α) (β := β) f (((eqv α).symm : (a : F' α) → F α) (abs (F := F') (α := α) p)) : F β)

Tactic:
simp [q.abs_map, map_eq]

Premises used: MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u_1} n
α : TypeVec.{u_1} n
x : (↑P : (α : TypeVec.{u_1} n) → Type u_1) α
⊢ id (id x) = x

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
P : MvPFunctor.{u_1} n
α β : TypeVec.{u_1} n
f : α ⟹ β
p : (↑P : (α : TypeVec.{u_1} n) → Type u_1) α
⊢ id (MvFunctor.map (F := (↑P : (α : TypeVec.{u_1} n) → Type u_1)) (α := α) (β := β) f p) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u_1} n) → Type u_1)) (α := α) (β := β) f (id p)

Tactic:
rfl