-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem suppPreservation_iff_liftpPreservation : q.SuppPreservation ↔ q.LiftPPreservation

Proof state:
case mp.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)

Tactic:
constructor <;> intros <;> subst_vars <;> solve_by_elim

Result:
no goals

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

Tactic:
ext

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

Proof state:
case mp.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩

Tactic:
dsimp only [SuppPreservation, supp] at h

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

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

Tactic:
simp only [supp, h, mem_setOf_eq]

Result:
no goals

Proof state:
case mp.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : SuppPreservation
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩

Tactic:
rw [suppPreservation_iff_isUniform] at h'

Result:
case mp.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩

Proof state:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : LiftPPreservation
⊢ SuppPreservation

Tactic:
rintro α ⟨a, f⟩

Result:
case mpr.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : LiftPPreservation
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Proof state:
case mp.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩

Tactic:
have h' := h

Result:
case mp.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : SuppPreservation
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩

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

Tactic:
simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h',
  image_univ, mem_range, exists_imp]

Result:
case mp.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation ↔ LiftPPreservation

Tactic:
constructor <;> intro h

Result:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
⊢ LiftPPreservation

case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : LiftPPreservation
⊢ SuppPreservation

Proof state:
case mpr.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : LiftPPreservation
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Tactic:
simp only [LiftPPreservation] at h

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

Proof state:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
⊢ LiftPPreservation

Tactic:
rintro α p ⟨a, f⟩

Result:
case mp.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩