Porting note: was simp

[pitmonticone]

Classifies porting notes claiming was simp.

Examples

mathlib4/Mathlib/Algebra/Lie/Engel.lean

Lines 175 to 186 in 2147266

	theorem Function.Surjective.isEngelian {f : L →ₗ⁅R⁆ L₂} (hf : Function.Surjective f)
	(h : LieAlgebra.IsEngelian.{u₁, u₂, u₄} R L) : LieAlgebra.IsEngelian.{u₁, u₃, u₄} R L₂ := by
	intro M _i1 _i2 _i3 _i4 h'
	letI : LieRingModule L M := LieRingModule.compLieHom M f
	letI : LieModule R L M := compLieHom M f
	have hnp : ∀ x, IsNilpotent (toEndomorphism R L M x) := fun x => h' (f x)
	have surj_id : Function.Surjective (LinearMap.id : M →ₗ[R] M) := Function.surjective_id
	haveI : LieModule.IsNilpotent R L M := h M hnp
	apply hf.lieModuleIsNilpotent surj_id
	-- Porting note: was `simp`
	intros; simp only [LinearMap.id_coe, id_eq]; rfl
	#align function.surjective.is_engelian Function.Surjective.isEngelian

mathlib4/Mathlib/Data/IsROrC/Basic.lean

Lines 589 to 592 in 2147266

	@[isROrC_simps] -- porting note: was `simp`
	theorem conj_inv (x : K) : conj x⁻¹ = (conj x)⁻¹ :=
	star_inv' _
	#align is_R_or_C.conj_inv IsROrC.conj_inv

mathlib4/Mathlib/LinearAlgebra/Isomorphisms.lean

Lines 135 to 141 in 2147266

	-- @[simp] -- Porting note: simp can prove this
	theorem quotientInfEquivSupQuotient_symm_apply_eq_zero_iff {p p' : Submodule R M} {x : ↥(p ⊔ p')} :
	(quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ (x : M) ∈ p' :=
	(LinearEquiv.symm_apply_eq _).trans <| by
	-- Porting note: Was `simp`.
	rw [_root_.map_zero, Quotient.mk_eq_zero, mem_comap, Submodule.coeSubtype]
	#align linear_map.quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff

mathlib4/Mathlib/SetTheory/Cardinal/Basic.lean

Lines 1358 to 1363 in 2147266

	-- Porting note: was `simp`. LHS is not normal form.
	-- @[simp, norm_cast]
	@[norm_cast]
	theorem natCast_pow {m n : ℕ} : (↑(m ^ n) : Cardinal) = (↑m : Cardinal) ^ (↑n : Cardinal) := by
	induction n <;> simp [pow_succ', power_add, *, Pow.pow]
	#align cardinal.nat_cast_pow Cardinal.natCast_pow

[grunweg]

Some of these are resolved in #12128.