awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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 u
have mpr : p i_1 (f' i_1 i)
Tactic: rw [← f'ieq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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)
have mpr : ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
Tactic: refine ⟨a, f, xeq.symm, ?_⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ p j (f j y)
have mpr : f j y ∈ supp (F := F) (α := α) x j
Tactic: apply h'
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ f j y ∈ supp (F := F) (α := α) x j
have 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
Tactic: rw [mem_supp]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
have mpr : f j y ∈ f j '' univ
Tactic: apply h _ a' f' xeq'
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ supp (F := F) (α := α) (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f)) i = f i '' univ
have 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
Tactic: ext u
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ 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
have 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: rw [mem_supp]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ (∀ (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
have 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: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ LiftP (F := F) (α := α) p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
have 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
Tactic: rw [liftP_iff, ← abs_repr x]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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 ⟹ α),
      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
have 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
Tactic: obtain ⟨a, f⟩ := repr x
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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_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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ (∃ (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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ ∀ (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
have mp : ∀ u_1 ∈ f' u '' univ, p u u_1
Tactic: rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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 b
have mp : p u (f' u i)
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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)
have 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)
Tactic: refine ⟨a, f, rfl, fun _ i => h' _ _ ?_⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ 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)
have mpr : f x_1 i ∈ f x_1 '' univ
Tactic: rw [supp_eq_of_isUniform h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ supp (F := F) (α := β) (map (F := F) (α := α) (β := β) g x) i = g i '' supp (F := F) (α := α) x i
have 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
Tactic: rw [← abs_repr x]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨a, f⟩ := repr x
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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 ⟹ α
⊢ 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
have 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
Tactic: rw [← abs_map, MvPFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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 ⟹ α
⊢ 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
have rw : TypeVec.comp (α := (P F).B a) (β := α) (γ := β) g f i '' univ = g i ∘ f i '' univ
Tactic: rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, ← image_comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation (F := F) ↔ IsUniform (F := F)
have mp : SuppPreservation (F := F) → IsUniform (F := F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
mp : SuppPreservation (F := F) → IsUniform (F := F)
⊢ SuppPreservation (F := F) ↔ IsUniform (F := F)
have mpr : IsUniform (F := F) → SuppPreservation (F := F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ f i '' univ = f' i '' univ
have 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
Tactic: rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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
⊢ f i '' univ = f' i '' univ
have 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)
Tactic: rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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)
⊢ f i '' univ = f' i '' univ
have 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)
Tactic: rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (goal)
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)
⊢ f i '' univ = f' i '' univ
have 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)
Tactic: rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]