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
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α) (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y = 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), p (f i j)
have mp : ∀ (a : (P F).A) (f : (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p)
  (h :
    repr (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) y =
      Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f),
  ∃ (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 (f i j)
Tactic: rcases h : repr y with ⟨a, f⟩
-- 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
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α) (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y = x
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) y =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
⊢ ∃ (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 (f i j)
have h₁ : x =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i)) ∧
  ∀ (i : Fin2 n) (j : (P F).B a i), p (i := i) ((fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i)) i j)
Tactic: use a, fun i j => (f i j).val
-- 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
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α) (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y = x
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) y =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
⊢ x =
      abs (F := F) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i)) ∧
    ∀ (i : Fin2 n) (j : (P F).B a i), p (i := i) ((fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i)) i j)
have h₁ : x =
  abs (F := F) (α := α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i))
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
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α) (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y = x
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) y =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
h₁ :
  x =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i))
⊢ x =
      abs (F := F) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i)) ∧
    ∀ (i : Fin2 n) (j : (P F).B a i), p (i := i) ((fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i)) i j)
have h₂ : ∀ (i : Fin2 n) (j : (P F).B a i), p (↑(f i j) : α i)
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
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun (i : Fin2 n) ↦ Subtype (α := α i) p
hy :
  map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α) (fun (i : Fin2 n) ↦ Subtype.val (p := p)) y = x
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) y =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f
⊢ x =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i))
have h₁ : Eq (α := F α)
  (abs (F := F) (α := α)
    (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p))
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a f)))
  (abs (F := F) (α := α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i)))
Tactic: rw [← hy, ← abs_repr y, h, ← 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
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : (P F).B a ⟹ α
h₀ : 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 (f i j)
⊢ LiftP (F := F) (α := α) p x
have h : map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α) (fun (i : Fin2 n) ↦ Subtype.val (p := p))
    (abs (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a
        fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := p) (f i j) sorry)) =
  x
Tactic: use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩
-- 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
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : (P F).B a ⟹ α
h₀ : 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 (f i j)
⊢ map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α) (fun (i : Fin2 n) ↦ Subtype.val (p := p))
      (abs (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a
          fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := p) (f i j) ⋯)) =
    x
have h : Eq (α := F α)
  (abs (F := F) (α := α)
    (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) p) (β := α)
      (fun (i : Fin2 n) ↦ Subtype.val (p := p))
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ Subtype (α := α i) p) a
        fun (i : Fin2 n) (j : (P F).B a i) ↦ Subtype.mk (p := p) (f i j) sorry)))
  (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))
Tactic: rw [← abs_map, 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
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
⊢ LiftR (F := F) (α := α) r x y ↔
    ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α) (f₁ : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀) ∧
        y = 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), r (f₀ i j) (f₁ i j)
have mp : LiftR (F := F) (α := α) r x y →
  ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α) (f₁ : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀) ∧
      y = 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), r (f₀ i j) (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
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
mp :
  LiftR (F := F) (α := α) r x y →
    ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α) (f₁ : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀) ∧
        y = 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), r (f₀ i j) (f₁ i j)
⊢ LiftR (F := F) (α := α) r x y ↔
    ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α) (f₁ : (P F).B a ⟹ α),
      x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀) ∧
        y = 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), r (f₀ i j) (f₁ i j)
have mpr : (∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α) (f₁ : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀) ∧
      y = 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), r (f₀ i j) (f₁ i j)) →
  LiftR (F := F) (α := α) r x 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 α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
⊢ ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α) (f₁ : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀) ∧
      y = 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), r (f₀ i j) (f₁ i j)
have mp : ∀ (a : (P F).A) (f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 })
  (h :
    repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
      Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f),
  ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α) (f₁ : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀) ∧
      y = 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), r (f₀ i j) (f₁ i j)
Tactic: rcases h : repr u with ⟨a, f⟩
-- 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 α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α) (f₁ : (P F).B a ⟹ α),
    x = abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f₀) ∧
      y = 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), r (f₀ i j) (f₁ i j)
have h₁ : x =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).1) ∧
  y =
      abs (F := F) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
          (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : (P F).B a i),
      r (↑(f i j) : α i × α i).1 ((fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i × α i).2) i j)
Tactic: use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd
-- 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 α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ x =
      abs (F := F) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
          (↑(f i j) : α i × α i).1) ∧
    y =
        abs (F := F) (α := α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
            (↑(f i j) : α i × α i).2) ∧
      ∀ (i : Fin2 n) (j : (P F).B a i),
        r (↑(f i j) : α i × α i).1 ((fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i × α i).2) i j)
have h₁ : x =
  abs (F := F) (α := α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i × α i).1)
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 α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ :
  x =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).1)
⊢ x =
      abs (F := F) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
          (↑(f i j) : α i × α i).1) ∧
    y =
        abs (F := F) (α := α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
            (↑(f i j) : α i × α i).2) ∧
      ∀ (i : Fin2 n) (j : (P F).B a i),
        r (↑(f i j) : α i × α i).1 ((fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i × α i).2) i j)
have h₂ : y =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).2) ∧
  ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
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 α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ x =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).1)
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 f)))
  (abs (F := F) (α := α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i × α i).1))
Tactic: rw [← xeq, ← abs_repr u, h, ← 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 α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ y =
      abs (F := F) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
          (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
have h₁ : y =
  abs (F := F) (α := α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i × α i).2)
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 α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
h₁ :
  y =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).2)
⊢ y =
      abs (F := F) (α := α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
          (↑(f i j) : α i × α i).2) ∧
    ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
have h₂ : ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j) : α i × α i).1 (↑(f i j) : α i × α i).2
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 α
u : F fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
xeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).1) u =
    x
yeq :
  map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) (β := α)
      (fun (i : Fin2 n) (t : { p : α i × α i // r p.1 p.2 }) ↦ (↑t : α i × α i).2) u =
    y
a : (P F).A
f : (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }
h :
  repr (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) u =
    Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ fun (i : Fin2 n) ↦ { p : α i × α i // r p.1 p.2 }) a f
⊢ y =
    abs (F := F) (α := α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦
        (↑(f i j) : α i × α i).2)
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 f)))
  (abs (F := F) (α := α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a fun (i : Fin2 n) (j : (P F).B a i) ↦ (↑(f i j) : α i × α i).2))
Tactic: rw [← yeq, ← abs_repr u, h, ← 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)
⊢ LiftR (F := F) (α := α) r x 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 ∧
  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: use abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩