-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem liftR_iff {α : TypeVec n} (r : ∀ /- ⦃i⦄ -/ {i}, α i → α i → Prop) (x y : F α) :
    LiftR r x y ↔ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ i j, r (f₀ i j) (f₁ i j)

Proof state:
case h.right
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 ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t => (↑t).2) <$$> ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h.right.right
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i => { p // (fun {i} => r) p.1 p.2 }
h : repr u = ⟨a, f⟩
i : Fin2 n
j : (P F).B a i
⊢ r (↑(f i j)).1 (↑(f i j)).2

Tactic:
exact (f i j).property

Result:
no goals

Proof state:
case h.left
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 ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).1) <$$> abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = x

Tactic:
rw [xeq, ← abs_map]

Result:
case h.left
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 ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t => (↑t).1) <$$> ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₀⟩

Proof state:
case h.right.left
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i => { p // (fun {i} => r) p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t => (↑t).2) <$$> ⟨a, f⟩) = abs ⟨a, fun i j => (↑(f i j)).2⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h.left
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i => { p // (fun {i} => r) p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((fun i t => (↑t).1) <$$> ⟨a, f⟩) = abs ⟨a, fun i j => (↑(f i j)).1⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h.right.right
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i => { p // (fun {i} => r) p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j)).1 (↑(f i j)).2

Tactic:
intro i j

Result:
case h.right.right
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i => { p // (fun {i} => r) p.1 p.2 }
h : repr u = ⟨a, f⟩
i : Fin2 n
j : (P F).B a i
⊢ r (↑(f i j)).1 (↑(f i j)).2

Proof state:
case mpr.intro.intro.intro.intro.intro
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 ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ LiftR (fun {i} => r) x y

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

Result:
case h
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 ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t => (↑t).1) <$$> abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = x ∧
    (fun i t => (↑t).2) <$$> abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = y

Proof state:
case h.right
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i => { p // (fun {i} => r) p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i j => (↑(f i j)).2⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j)).1 (↑(f i j)).2

Tactic:
constructor

Result:
case h.right.left
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i => { p // (fun {i} => r) p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i j => (↑(f i j)).2⟩

case h.right.right
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
a : (P F).A
f : (P F).B a ⟹ fun i => { p // (fun {i} => r) p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), r (↑(f i j)).1 (↑(f i j)).2

Proof state:
case mp
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 (fun {i} => r) x y →
    ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)

Tactic:
rintro ⟨u, xeq, yeq⟩

Result:
case mp.intro.intro
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 => { p // (fun {i} => r) p.1 p.2 }
xeq : (fun i t => (↑t).1) <$$> u = x
yeq : (fun i t => (↑t).2) <$$> u = y
⊢ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)

Proof state:
case h.left
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 ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t => (↑t).1) <$$> ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₀⟩

Tactic:
rfl

Result:
no goals

Proof state:
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 (fun {i} => r) x y ↔
    ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)

Tactic:
constructor

Result:
case mp
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 (fun {i} => r) x y →
    ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)

case mpr
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 f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)) →
    LiftR (fun {i} => r) x y