Lean4
/-- If `𝒰` is a directed cover of `X`, this is the cover of `𝒰ᵢ ×[X] 𝒰ⱼ` by `{𝒰ₖ}` where
`k ≤ i` and `k ≤ j`. -/
@[simps f]
def intersectionOfLocallyDirected [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] (i j : 𝒰.I₀) :
(pullback (𝒰.f i) (𝒰.f j)).Cover (precoverage P)
where
I₀ := Σ (k : 𝒰.I₀), (k ⟶ i) × (k ⟶ j)
X k := 𝒰.X k.1
f k := pullback.lift (𝒰.trans k.2.1) (𝒰.trans k.2.2) (by simp)
mem₀ := by
rw [presieve₀_mem_precoverage_iff]
refine ⟨fun x ↦ ?_, fun k ↦ ?_⟩
· use
⟨(𝒰.exists_lift_trans_eq x).choose, (𝒰.exists_lift_trans_eq x).choose_spec.choose,
(𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose⟩
exact (𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose_spec
· apply P.of_postcomp (W' := P) _ (pullback.fst _ _) (P.pullback_fst _ _ (𝒰.map_prop _))
rw [pullback.lift_fst]
exact 𝒰.property_trans _