Lean4
/-- Define `GCDMonoid` on a structure just from the `lcm` and its properties. -/
noncomputable def gcdMonoidOfLCM [DecidableEq α] (lcm : α → α → α) (dvd_lcm_left : ∀ a b, a ∣ lcm a b)
(dvd_lcm_right : ∀ a b, b ∣ lcm a b) (lcm_dvd : ∀ {a b c}, c ∣ a → b ∣ a → lcm c b ∣ a) : GCDMonoid α :=
let exists_gcd a b := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
{ lcm
gcd := fun a b => if a = 0 then b else if b = 0 then a else Classical.choose (exists_gcd a b)
gcd_mul_lcm := fun a b => by
split_ifs with h h_1
· rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
· rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _)]
rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]
lcm_zero_left := fun _ => eq_zero_of_zero_dvd (dvd_lcm_left _ _)
lcm_zero_right := fun _ => eq_zero_of_zero_dvd (dvd_lcm_right _ _)
gcd_dvd_left := fun a b => by
split_ifs with h h_1
· rw [h]
apply dvd_zero
· exact dvd_rfl
have h0 : lcm a b ≠ 0 := by
intro con
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
rw [con, zero_dvd_iff, mul_eq_zero] at h
cases h
· exact absurd ‹a = 0› h
· exact absurd ‹b = 0› h_1
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), mul_comm, mul_dvd_mul_iff_right h]
apply dvd_lcm_right
gcd_dvd_right := fun a b => by
split_ifs with h h_1
· exact dvd_rfl
· rw [h_1]
apply dvd_zero
have h0 : lcm a b ≠ 0 := by
intro con
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
rw [con, zero_dvd_iff, mul_eq_zero] at h
cases h
· exact absurd ‹a = 0› h
· exact absurd ‹b = 0› h_1
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), mul_dvd_mul_iff_right h_1]
apply dvd_lcm_left
dvd_gcd := fun {a b c} ac ab => by
split_ifs with h h_1
· exact ab
· exact ac
have h0 : lcm c b ≠ 0 := by
intro con
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
rw [con, zero_dvd_iff, mul_eq_zero] at h
cases h
· exact absurd ‹c = 0› h
· exact absurd ‹b = 0› h_1
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd c b)]
rcases ab with ⟨d, rfl⟩
rw [mul_eq_zero] at ‹a * d ≠ 0›
push_neg at h_1
rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]
apply lcm_dvd (Dvd.intro d rfl)
rw [mul_comm, mul_dvd_mul_iff_right h_1.2]
apply ac }
