Porting note: need dsimp only

[pitmonticone]

Classifies porting notes claiming:

need dsimp only.

Examples

mathlib4/Mathlib/Algebra/GCDMonoid/Basic.lean

Lines 1040 to 1069 in 89415b3

	/-- Define `GCDMonoid` on a structure just from the `gcd` and its properties. -/
	noncomputable def gcdMonoidOfGCD [DecidableEq α] (gcd : α → α → α)
	(gcd_dvd_left : ∀ a b, gcd a b ∣ a) (gcd_dvd_right : ∀ a b, gcd a b ∣ b)
	(dvd_gcd : ∀ {a b c}, a ∣ c → a ∣ b → a ∣ gcd c b) : GCDMonoid α :=
	{ gcd
	gcd_dvd_left
	gcd_dvd_right
	dvd_gcd := fun {a b c} => dvd_gcd
	lcm := fun a b =>
	if a = 0 then 0 else Classical.choose ((gcd_dvd_left a b).trans (Dvd.intro b rfl))
	gcd_mul_lcm := fun a b => by
	-- Porting note: need `dsimp only` before `split_ifs`
	dsimp only
	split_ifs with a0
	· rw [mul_zero, a0, zero_mul]
	· rw [← Classical.choose_spec ((gcd_dvd_left a b).trans (Dvd.intro b rfl))]
	lcm_zero_left := fun a => if_pos rfl
	lcm_zero_right := fun a => by
	-- Porting note: need `dsimp only` before `split_ifs`
	dsimp only
	split_ifs with a0
	· rfl
	have h := (Classical.choose_spec ((gcd_dvd_left a 0).trans (Dvd.intro 0 rfl))).symm
	have a0' : gcd a 0 ≠ 0 := by
	contrapose! a0
	rw [← associated_zero_iff_eq_zero, ← a0]
	exact associated_of_dvd_dvd (dvd_gcd (dvd_refl a) (dvd_zero a)) (gcd_dvd_left _ _)
	apply Or.resolve_left (mul_eq_zero.1 _) a0'
	rw [h, mul_zero] }
	#align gcd_monoid_of_gcd gcdMonoidOfGCD

[grunweg]

Some of these are just about beta-reduction; I'm re-classifying these as #12129 in #12130.