Porting note: broken dot notation

[pitmonticone]

Classifies porting notes claiming anything equivalent to

• "broken dot notation"
• "dot notation no longer works"

Examples

mathlib4/Mathlib/Algebra/Category/ModuleCat/Kernels.lean

Lines 91 to 98 in f5e8fa1

	/-- The categorical kernel of a morphism in `ModuleCat`
	agrees with the usual module-theoretical kernel.
	-/
	noncomputable def kernelIsoKer {G H : ModuleCat.{v} R} (f : G ⟶ H) :
	-- Porting note: broken dot notation
	kernel f ≅ ModuleCat.of R (LinearMap.ker f) :=
	limit.isoLimitCone ⟨_, kernelIsLimit f⟩
	#align Module.kernel_iso_ker ModuleCat.kernelIsoKer

mathlib4/Mathlib/LinearAlgebra/Dual.lean

Lines 1173 to 1178 in f5e8fa1

	/-- The natural isomorphism from the dual of a subspace `W` to `W.dualLift.range`. -/
	-- Porting note: broken dot notation lean4#1910 LinearMap.range
	noncomputable def dualEquivDual (W : Subspace K V) :
	Module.Dual K W ≃ₗ[K] LinearMap.range W.dualLift :=
	LinearEquiv.ofInjective _ dualLift_injective
	#align subspace.dual_equiv_dual Subspace.dualEquivDual

mathlib4/Mathlib/Data/Set/Semiring.lean

Lines 58 to 91 in 16cc6aa

	-- Porting note: dot notation no longer works
	@[simp]
	protected theorem down_up (s : Set α) : SetSemiring.down (Set.up s) = s :=
	rfl
	#align set_semiring.down_up SetSemiring.down_up
	-- Porting note: dot notation no longer works
	@[simp]
	protected theorem up_down (s : SetSemiring α) : Set.up (SetSemiring.down s) = s :=
	rfl
	#align set_semiring.up_down SetSemiring.up_down
	-- TODO: These lemmas are not tagged `simp` because `Set.le_eq_subset` simplifies the LHS
	-- Porting note: dot notation no longer works
	theorem up_le_up {s t : Set α} : Set.up s ≤ Set.up t ↔ s ⊆ t :=
	Iff.rfl
	#align set_semiring.up_le_up SetSemiring.up_le_up
	-- Porting note: dot notation no longer works
	theorem up_lt_up {s t : Set α} : Set.up s < Set.up t ↔ s ⊂ t :=
	Iff.rfl
	#align set_semiring.up_lt_up SetSemiring.up_lt_up
	-- Porting note: dot notation no longer works
	@[simp]
	theorem down_subset_down {s t : SetSemiring α} : SetSemiring.down s ⊆ SetSemiring.down t ↔ s ≤ t :=
	Iff.rfl
	#align set_semiring.down_subset_down SetSemiring.down_subset_down
	-- Porting note: dot notation no longer works
	@[simp]
	theorem down_ssubset_down {s t : SetSemiring α} : SetSemiring.down s ⊂ SetSemiring.down t ↔ s < t :=
	Iff.rfl
	#align set_semiring.down_ssubset_down SetSemiring.down_ssubset_down