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

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

Tactic:
constructor

Result:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)) → LiftP p x

Proof state:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)) → LiftP p x

Tactic:
rintro ⟨a, f, h₀, h₁⟩

Result:
case mpr.intro.intro.intro
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 ⟨a, f⟩
h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ LiftP p x

Proof state:
case h
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 ⟨a, f⟩
h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ abs ((fun i => Subtype.val) <$$> ⟨a, fun i j => ⟨f i j, ⋯⟩⟩) = abs ⟨a, f⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mpr.intro.intro.intro
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 ⟨a, f⟩
h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ LiftP p x

Tactic:
use abs ⟨a, fun 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
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
a : (P F).A
f : (P F).B a ⟹ α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> abs ⟨a, fun i j => ⟨f i j, ⋯⟩⟩ = x

Proof state:
case h.left
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((fun i => Subtype.val) <$$> ⟨a, f⟩) = abs ⟨a, fun i j => ↑(f i j)⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h.left
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j => ↑(f i j)⟩

Tactic:
rw [← hy, ← abs_repr y, h, ← abs_map]

Result:
case h.left
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((fun i => Subtype.val) <$$> ⟨a, f⟩) = abs ⟨a, fun i j => ↑(f i j)⟩

Proof state:
case h
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j => ↑(f i j)⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p ((fun i j => ↑(f i j)) i j)

Tactic:
constructor

Result:
case h.left
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j => ↑(f i j)⟩

case h.right
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), p ↑(f i j)

Proof state:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

Tactic:
rintro ⟨y, hy⟩

Result:
case mp.intro
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

Proof state:
case mp.intro
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

Tactic:
rcases h : repr y with ⟨a, f⟩

Result:
case mp.intro.mk
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

Proof state:
case h
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 ⟨a, f⟩
h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ (fun i => Subtype.val) <$$> abs ⟨a, fun i j => ⟨f i j, ⋯⟩⟩ = x

Tactic:
rw [← abs_map, h₀]

Result:
case h
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 ⟨a, f⟩
h₁ : ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)
⊢ abs ((fun i => Subtype.val) <$$> ⟨a, fun i j => ⟨f i j, ⋯⟩⟩) = abs ⟨a, f⟩

Proof state:
case h.right
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), p ↑(f i j)

Tactic:
intro i j

Result:
case h.right
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
i : Fin2 n
j : (P F).B a i
⊢ p ↑(f i j)

Proof state:
case h.right
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
i : Fin2 n
j : (P F).B a i
⊢ p ↑(f i j)

Tactic:
apply (f i j).property

Result:
no goals

Proof state:
case mp.intro.mk
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ a f, x = abs ⟨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

Result:
case h
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 => Subtype p
hy : (fun i => Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i => Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i j => ↑(f i j)⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p ((fun i j => ↑(f i j)) i j)