Porting note: TODO

[pitmonticone]

Classifies porting notes claiming "TODO".

We might need some subclassification at a later stage.

Examples

mathlib4/Mathlib/Analysis/Normed/Group/Quotient.lean

Lines 407 to 412 in 7e0bc5a

	-- Porting note: todo: deprecate?
	theorem lift_norm_le {N : Type*} [SeminormedAddCommGroup N] (S : AddSubgroup M)
	(f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) {c : ℝ≥0} (fb : ‖f‖ ≤ c) :
	‖lift S f hf‖ ≤ c :=
	(norm_lift_le S f hf).trans fb
	#align normed_add_group_hom.lift_norm_le NormedAddGroupHom.lift_norm_le

mathlib4/Mathlib/Data/Analysis/Filter.lean

Lines 25 to 35 in 7e0bc5a

	-- Porting note: TODO write doc strings
	/-- A `CFilter α σ` is a realization of a filter (base) on `α`,
	represented by a type `σ` together with operations for the top element and
	the binary `inf` operation. -/
	structure CFilter (α σ : Type*) [PartialOrder α] where
	f : σ → α
	pt : σ
	inf : σ → σ → σ
	inf_le_left : ∀ a b : σ, f (inf a b) ≤ f a
	inf_le_right : ∀ a b : σ, f (inf a b) ≤ f b
	#align cfilter CFilter

mathlib4/Mathlib/Data/ENNReal/Operations.lean

Lines 70 to 78 in 7e0bc5a

	-- Porting note: todo: generalize to `WithTop`
	theorem mul_left_strictMono (h0 : a ≠ 0) (hinf : a ≠ ∞) : StrictMono (a * ·) := by
	lift a to ℝ≥0 using hinf
	rw [coe_ne_zero] at h0
	intro x y h
	contrapose! h
	simpa only [← mul_assoc, ← coe_mul, inv_mul_cancel h0, coe_one, one_mul]
	using mul_le_mul_left' h (↑a⁻¹)
	#align ennreal.mul_left_strict_mono ENNReal.mul_left_strictMono

mathlib4/Mathlib/Geometry/Manifold/Diffeomorph.lean

Lines 473 to 478 in 7e0bc5a

	@[simp]
	-- Porting note: TODO: should use `E ≃ₘ^n[𝕜] F` notation
	theorem uniqueDiffOn_preimage (h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F) (hn : 1 ≤ n) {s : Set F} :
	UniqueDiffOn 𝕜 (h ⁻¹' s) ↔ UniqueDiffOn 𝕜 s :=
	h.symm_image_eq_preimage s ▸ h.symm.uniqueDiffOn_image hn
	#align diffeomorph.unique_diff_on_preimage Diffeomorph.uniqueDiffOn_preimage

[grunweg]

A few notes classified here are actually instances of #5171.