-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) :
    (gcd a b).factorization = a.factorization ⊓ b.factorization

Proof state:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
p : ℕ
hp : p ∈ dfac.support
⊢ p ∈ a.primeFactorsList ∧ p ∈ b.primeFactorsList

Tactic:
simpa [dfac] using hp

Result:
no goals

Proof state:
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
⊢ e ∣ d

Tactic:
have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb

Result:
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
heb' : e.factorization ≤ b.factorization
⊢ e ∣ d

Proof state:
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ b.factorization

Tactic:
exact inf_le_right

Result:
no goals

Proof state:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
have h1 : d.factorization = dfac := prod_pow_factorization_eq_self dfac_prime

Result:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Proof state:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
p : ℕ
hp : p ∈ dfac.support
⊢ Prime p

Tactic:
have : p ∈ a.primeFactorsList ∧ p ∈ b.primeFactorsList := by simpa [dfac] using hp

Result:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
p : ℕ
hp : p ∈ dfac.support
this : p ∈ a.primeFactorsList ∧ p ∈ b.primeFactorsList
⊢ Prime p

Proof state:
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ a.factorization

Tactic:
exact inf_le_left

Result:
no goals

Proof state:
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
⊢ d ∣ b

Tactic:
rw [← factorization_le_iff_dvd hd_pos hb_pos, h1]

Result:
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ b.factorization

Proof state:
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d

Tactic:
intro e hea heb

Result:
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
d : ℕ := dfac.prod fun x1 x2 => x1 ^ x2
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
⊢ e ∣ d