-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem liftP_iff_of_isUniform (h : q.IsUniform) {α : TypeVec n} (x : F α) (p : ∀ i, α i → Prop) :
    LiftP p x ↔ ∀ (i), ∀ u ∈ supp x i, p i u

Proof state:
case mk.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)) →
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u

Tactic:
rintro ⟨a', f', abseq, hf⟩ u

Result:
case mk.mp.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
⊢ ∀ u_1 ∈ supp (abs ⟨a, f⟩) u, p u u_1

Proof state:
case mk.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u (f' u i)

Tactic:
apply hf

Result:
no goals

Proof state:
case mk.mp.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
⊢ ∀ u_1 ∈ supp (abs ⟨a, f⟩) u, p u u_1

Tactic:
rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]

Result:
case mk.mp.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
⊢ ∀ u_1 ∈ f' u '' univ, p u u_1

Proof state:
case mk.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
x✝ : Fin2 n
i : (P F).B a x✝
⊢ f x✝ i ∈ f x✝ '' univ

Tactic:
exact ⟨i, mem_univ i, rfl⟩

Result:
no goals

Proof state:
case mk.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u) →
    ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_2 i), p i (f_1 i j)

Tactic:
intro h'

Result:
case mk.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
⊢ ∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)

Proof state:
case mk.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
x✝ : Fin2 n
i : (P F).B a x✝
⊢ f x✝ i ∈ supp (abs ⟨a, f⟩) x✝

Tactic:
rw [supp_eq_of_isUniform h]

Result:
case mk.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
x✝ : Fin2 n
i : (P F).B a x✝
⊢ f x✝ i ∈ f x✝ '' univ

Proof state:
case mk.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u b

Tactic:
rw [← hi]

Result:
case mk.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u (f' u i)

Proof state:
case mk.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
⊢ ∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)

Tactic:
refine ⟨a, f, rfl, fun _ i => h' _ _ ?_⟩

Result:
case mk.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
x✝ : Fin2 n
i : (P F).B a x✝
⊢ f x✝ i ∈ supp (abs ⟨a, f⟩) x✝

Proof state:
case mk.mp.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
⊢ ∀ u_1 ∈ f' u '' univ, p u u_1

Tactic:
rintro b ⟨i, _, hi⟩

Result:
case mk.mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u b

Proof state:
case mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u

Tactic:
constructor

Result:
case mk.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)) →
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u

case mk.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u) →
    ∃ a_2 f_1, abs ⟨a, f⟩ = abs ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_2 i), p i (f_1 i j)

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

Tactic:
obtain ⟨a, f⟩ := repr x

Result:
case mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u