apply le_trans _ this
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) p

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y