Lean4
/-- Define `NormalizedGCDMonoid` on a structure just from the `gcd` and its properties. -/
noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [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) (normalize_gcd : ∀ a b, normalize (gcd a b) = gcd a b) :
NormalizedGCDMonoid α :=
{ (inferInstance : NormalizationMonoid α) with
gcd
gcd_dvd_left
gcd_dvd_right
dvd_gcd := fun {_ _ _} => dvd_gcd
normalize_gcd
lcm := fun a b =>
if a = 0 then 0 else Classical.choose (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))
normalize_lcm := fun a b => by
dsimp [normalize]
split_ifs with a0
· exact @normalize_zero α _ _
· have := (Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))).symm
set l := Classical.choose (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))
obtain rfl | hb := eq_or_ne b 0
· rw [mul_zero a, normalize_zero, mul_eq_zero] at this
obtain ha | hl := this
· apply (a0 _).elim
rw [← zero_dvd_iff, ← ha]
exact gcd_dvd_left _ _
· rw [hl, zero_mul]
have h1 : gcd a b ≠ 0 := by
have hab : a * b ≠ 0 := mul_ne_zero a0 hb
contrapose! hab
rw [← normalize_eq_zero, ← this, hab, zero_mul]
have h2 : normalize (gcd a b * l) = gcd a b * l := by rw [this, normalize_idem]
rw [← normalize_gcd] at this
rwa [normalize.map_mul, normalize_gcd, mul_right_inj' h1] at h2
gcd_mul_lcm := fun a b => by
split_ifs with a0
· rw [mul_zero, a0, zero_mul]
· rw [← Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (.intro b rfl)))]
exact normalize_associated (a * b)
lcm_zero_left := fun _ => if_pos rfl
lcm_zero_right := fun a => by
split_ifs with a0
· rfl
rw [← normalize_eq_zero] at a0
have h := (Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a 0).trans (.intro 0 rfl)))).symm
have gcd0 : gcd a 0 = normalize a := by
rw [← normalize_gcd]
exact normalize_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_zero a))
rw [← gcd0] at a0
apply Or.resolve_left (mul_eq_zero.1 _) a0
rw [h, mul_zero, normalize_zero] }
