-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem suppPreservation_iff_liftpPreservation : q.SuppPreservation ↔ q.LiftpPreservation

Proof state:
case mp.mk
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → 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
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → 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
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → 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_uniform] at h'

Result:
case mp.mk
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩

Proof state:
F : Type u → Type u
q : QPF F
⊢ SuppPreservation ↔ LiftpPreservation

Tactic:
constructor <;> intro h

Result:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
⊢ LiftpPreservation

case mpr
F : Type u → Type u
q : QPF F
h : LiftpPreservation
⊢ SuppPreservation

Proof state:
case mp.mk
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ (∀ (u : α) (x : (P F).B a), f x = u → p u) ↔ ∀ (i : (P F).B a), p (f i)

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

Result:
no goals

Proof state:
case mpr.mk
F : Type u → Type u
q : QPF F
h : ∀ ⦃α : Type u⦄ (p : α → Prop) (x : ↑(P F) α), Liftp p (abs x) ↔ Liftp p x
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Tactic:
simp only [supp, h]

Result:
no goals

Proof state:
case mpr
F : Type u → Type u
q : QPF F
h : LiftpPreservation
⊢ SuppPreservation

Tactic:
rintro α ⟨a, f⟩

Result:
case mpr.mk
F : Type u → Type u
q : QPF F
h : LiftpPreservation
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Proof state:
case mpr.mk
F : Type u → Type u
q : QPF F
h : LiftpPreservation
α : Type u
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
F : Type u → Type u
q : QPF F
h : ∀ ⦃α : Type u⦄ (p : α → Prop) (x : ↑(P F) α), Liftp p (abs x) ↔ Liftp p x
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Proof state:
case mp.mk
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)

Tactic:
simp only [image_univ, mem_range, exists_imp]

Result:
case mp.mk
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ (∀ (u : α) (x : (P F).B a), f x = u → p u) ↔ ∀ (i : (P F).B a), p (f i)

Proof state:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
⊢ LiftpPreservation

Tactic:
rintro α p ⟨a, f⟩

Result:
case mp.mk
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩

Proof state:
case mp.mk
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → 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
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩

Proof state:
case mp.mk
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩

Tactic:
rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']

Result:
case mp.mk
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)