awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i → (TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (a : ι), a ∈ l → f a ∈ t a)

Tactic:
fun _ => h
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i → (TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (a : ι), a ∈ l → f a ∈ t a)

Tactic:
exact fun _ => h
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h₁ : ∀ (i : ι), Membership.mem (γ := Set ι) {i : ι | i ∈ l} i ↔ Membership.mem (γ := Set ι) univ i
⊢ Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ

Tactic:
ext i
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
i : ι
⊢ Membership.mem (γ := Set ι) {i : ι | i ∈ l} i ↔ Membership.mem (γ := Set ι) univ i

Tactic:
simp [h]
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ

Tactic:
have h2 : { i | i ∈ l } = univ := by
    ext i
    simp [h]
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ
rw :
  (fun (x : TProd α l) ↦ TProd.mk (α := α) l (TProd.elim' (α := α) h x)) ⁻¹' Set.tprod (α := α) l t =
    Set.tprod (α := α) l t
⊢ TProd.elim' (α := α) h ⁻¹' pi (α := α) univ t = Set.tprod (α := α) l t

Tactic:
rw [← h2, ← mk_preimage_tprod, preimage_preimage]

Premises used: Set.preimage_preimage, Set.mk_preimage_tprod
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ
simp : (fun (x : TProd α l) ↦ x) ⁻¹' Set.tprod (α := α) l t = Set.tprod (α := α) l t
⊢ (fun (x : TProd α l) ↦ TProd.mk (α := α) l (TProd.elim' (α := α) h x)) ⁻¹' Set.tprod (α := α) l t =
    Set.tprod (α := α) l t

Tactic:
simp only [TProd.mk_elim hnd h]

Premises used: List.TProd.mk_elim
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : Eq.{u + 1} (α := Set ι) {i : ι | i ∈ l} univ
⊢ (fun (x : TProd α l) ↦ x) ⁻¹' Set.tprod (α := α) l t = Set.tprod (α := α) l t

Tactic:
dsimp
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
rw :
  abs (F := F) (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := α) (TypeVec.id (α := α))
        (repr (F := F) (α := α) x)) =
    abs (F := F) (α := α) (repr (F := F) (α := α) x)
⊢ map (F := F) (α := α) (β := α) (TypeVec.id (α := α)) x = x

Tactic:
rw [← abs_repr x, ← abs_map]

Premises used: MvQPF.abs_repr, MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ abs (F := F) (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := α) (TypeVec.id (α := α))
        (repr (F := F) (α := α) x)) =
    abs (F := F) (α := α) (repr (F := F) (α := α) x)

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
rw :
  abs (F := F) (α := γ)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := γ)
        (TypeVec.comp (α := α) (β := β) (γ := γ) g f) (repr (F := F) (α := α) x)) =
    abs (F := F) (α := γ)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := β) (β := γ) g
        (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f (repr (F := F) (α := α) x)))
⊢ map (F := F) (α := α) (β := γ) (TypeVec.comp (α := α) (β := β) (γ := γ) g f) x =
    map (F := F) (α := β) (β := γ) g (map (F := F) (α := α) (β := β) f x)

Tactic:
rw [← abs_repr x, ← abs_map, ← abs_map, ← abs_map]

Premises used: MvQPF.abs_repr, MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α β γ : TypeVec.{u} n
f : α ⟹ β
g : β ⟹ γ
x : F α
⊢ abs (F := F) (α := γ)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := γ)
        (TypeVec.comp (α := α) (β := β) (γ := γ) g f) (repr (F := F) (α := α) x)) =
    abs (F := F) (α := γ)
      (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := β) (β := γ) g
        (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f (repr (F := F) (α := α) x)))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
Goal:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
mp :
  LiftP (F := F) (α := α) p 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)
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 (f i j)) →
    LiftP (F := F) (α := α) p x
⊢ LiftP (F := F) (α := α) p 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)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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
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)
⊢ ∃ (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⟩

Premises used: MvQPF.repr
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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)) ∧
    ∀ (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)
⊢ ∃ (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:
use a, fun i j => (f i j).val

Premises used: Subtype.val
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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))
h₂ : ∀ (i : Fin2 n) (j : (P F).B a i), p (↑(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)

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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₁ :
  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)))
⊢ 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:
rw [← hy, ← abs_repr y, h, ← abs_map]

Premises used: MvQPF.abs_repr, MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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
⊢ 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:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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
i : Fin2 n
j : (P F).B a i
⊢ p (↑(f i j) : α i)

Tactic:
apply (f i j).property

Premises used: Subtype.property
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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)
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) ⋯)) =
    x
⊢ LiftP (F := F) (α := α) p x

Tactic:
use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩

Premises used: Sigma.mk, MvQPF.abs
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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)
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) ⋯)))
    (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))
⊢ 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

Tactic:
rw [← abs_map, h₀]

Premises used: MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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)
⊢ 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) ⋯)))
    (abs (F := F) (α := α) (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α) a f))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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)
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
⊢ 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
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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
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)
⊢ ∃ (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⟩

Premises used: MvQPF.repr
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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) ∧
    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)
⊢ ∃ (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:
use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd

Premises used: Prod.fst, Subtype.val, Prod.snd
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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)
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
⊢ 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:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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₁ :
  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))
⊢ 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:
rw [← xeq, ← abs_repr u, h, ← abs_map]

Premises used: MvQPF.abs_repr, MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Basic
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
⊢ 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:
rfl