Porting note: added proof

[pitmonticone]

Classifies porting notes claiming added proof.

Examples

mathlib4/Mathlib/Topology/Compactness/Paracompact.lean

Lines 97 to 113 in f5e69ec

	/-- In a paracompact space, every open covering of a closed set admits a locally finite refinement
	indexed by the same type. -/
	theorem precise_refinement_set [ParacompactSpace X] {s : Set X} (hs : IsClosed s) (u : ι → Set X)
	(uo : ∀ i, IsOpen (u i)) (us : s ⊆ ⋃ i, u i) :
	∃ v : ι → Set X, (∀ i, IsOpen (v i)) ∧ (s ⊆ ⋃ i, v i) ∧ LocallyFinite v ∧ ∀ i, v i ⊆ u i := by
	-- Porting note: Added proof of uc
	have uc : (iUnion fun i => Option.elim' sᶜ u i) = univ := by
	apply Subset.antisymm (subset_univ _)
	· simp_rw [← compl_union_self s, Option.elim', iUnion_option]
	apply union_subset_union_right sᶜ us
	rcases precise_refinement (Option.elim' sᶜ u) (Option.forall.2 ⟨isOpen_compl_iff.2 hs, uo⟩)
	uc with
	⟨v, vo, vc, vf, vu⟩
	refine' ⟨v ∘ some, fun i ↦ vo _, _, vf.comp_injective (Option.some_injective _), fun i ↦ vu _⟩
	· simp only [iUnion_option, ← compl_subset_iff_union] at vc
	exact Subset.trans (subset_compl_comm.1 <| vu Option.none) vc
	#align precise_refinement_set precise_refinement_set

mathlib4/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

Lines 80 to 89 in f5e69ec

	/-- (Impl) A preliminary definition to avoid timeouts. -/
	@[simps]
	def conesEquivFunctor (B : C) {J : Type w} (F : Discrete J ⥤ Over B) :
	Cone (widePullbackDiagramOfDiagramOver B F) ⥤ Cone F where
	obj c :=
	{ pt := Over.mk (c.π.app none)
	π :=
	{ app := fun ⟨j⟩ => Over.homMk (c.π.app (some j)) (c.w (WidePullbackShape.Hom.term j))
	-- Porting note: Added a proof for `naturality`
	naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨f⟩⟩ => by dsimp at f ⊢; aesop_cat } }