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
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)
⊢ 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
have 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) sorry)) =
  x
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
α : 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).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
have 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) sorry)) =
  y
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
α : 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)
⊢ 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
have 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) sorry)))
  (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀))
Tactic: rw [xeq, ← abs_map]
-- 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
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)
⊢ 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
have 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) sorry)))
  (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₁))
Tactic: rw [yeq, ← abs_map]
-- 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 α
i : Fin2 n
u : α i
⊢ (∀ ⦃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
have 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
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
α : 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
⊢ (∀ ⦃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
have 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
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
α : 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
have 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
Tactic: rw [liftP_iff]
-- 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 α
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
have refine : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ f i '' univ
Tactic: refine ⟨a, f, haf.symm, ?_⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (hypothesis)
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
⊢ u ∈ f i '' univ
have this : 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 _)
-- 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
i : Fin2 n
x : F α
⊢ 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}
have 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
Tactic: ext
-- 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 α
⊢ (∀ (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
have 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
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
α : 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
⊢ (∀ (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
have 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
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
α : 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
have rw : ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, supp (F := F) (α := α) x i u
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (hypothesis)
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 ⟹ α),
    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
have this : LiftP (F := F) (α := α) (supp (F := F) (α := α) x) x
Tactic: have : LiftP (supp x) x := by rw [h]; introv; exact id
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (hypothesis)
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 ⟹ α),
    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
have 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)
Tactic: rw [liftP_iff] at this
Cleared hypotheses: this
-- 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 α
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)
⊢ ∃ (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
have 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
Tactic: rcases this with ⟨a, f, xeq, h'⟩
Cleared hypotheses: this
-- 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 α
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
have 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
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 α
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'
have rw : f a' j ∈ supp (F := F) (α := α) x a'
Tactic: rw [← hfi]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Basic (hypothesis)
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 ∈ h'' a' '' univ
have hh : u ∈ supp (F := F) (α := α) x a'
Tactic: have hh : u ∈ supp x a' := by rw [← hfi]; 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
⊢ LiftP (F := F) (α := α) p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp (F := F) (α := α) x i, p i u
have 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
Tactic: rw [liftP_iff]
-- 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 ⟹ α),
      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
have 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
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
α : 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
⊢ (∃ (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
have 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)
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
α : 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
⊢ p i u
have 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
Tactic: rcases (mem_supp x _ u).mp (@usuppx) a' f' xeq'.symm with ⟨i, _, f'ieq⟩