-- 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:
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

Tactic:
rcases Decidable.eq_or_ne e 0 with (rfl | he_pos)

Result:
case hd.inl
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
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ d

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
⊢ e ∣ d

Proof state:
case hd.inl
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
heb : 0 ∣ b
hea : a = 0
⊢ 0 ∣ d

Tactic:
contradiction

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
⊢ e ∣ d

Tactic:
have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea

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
⊢ e ∣ d

Proof state:
case hd.inl
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
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ d

Tactic:
simp only [zero_dvd_iff] at hea

Result:
case hd.inl
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
heb : 0 ∣ b
hea : a = 0
⊢ 0 ∣ d

Proof state:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
let dfac := a.factorization ⊓ b.factorization

Result:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := a.factorization ⊓ b.factorization
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

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
⊢ d ∣ a

Tactic:
rw [← factorization_le_iff_dvd hd_pos ha_pos, h1]

Result:
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

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
this : p ∈ a.primeFactorsList ∧ p ∈ b.primeFactorsList
⊢ Prime p

Tactic:
exact prime_of_mem_primeFactorsList this.1

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
⊢ ∀ p ∈ dfac.support, Prime p

Tactic:
intro p 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
⊢ Prime p

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
h1 : d.factorization = dfac
hd_pos : d ≠ 0
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
suffices d = gcd a b by rwa [← this]

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
hd_pos : d ≠ 0
⊢ d = a.gcd b

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
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
have dfac_prime : ∀ p : ℕ, p ∈ dfac.support → Prime p := by
  intro p hp
  have : p ∈ a.primeFactorsList ∧ p ∈ b.primeFactorsList := by simpa [dfac] using hp
  exact prime_of_mem_primeFactorsList this.1

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
⊢ (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
dfac_prime : ∀ p ∈ dfac.support, Prime p
h1 : d.factorization = dfac
hd_pos : d ≠ 0
⊢ d = a.gcd b

Tactic:
apply gcd_greatest

Result:
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
⊢ d ∣ a

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

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

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
heb' : e.factorization ≤ b.factorization
⊢ e ∣ d

Tactic:
simp [dfac, ← factorization_le_iff_dvd he_pos hd_pos, h1, hea', heb']

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
h1 : d.factorization = dfac
hd_pos : d ≠ 0
this : d = a.gcd b
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
rwa [← this]

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
h1 : d.factorization = dfac
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
have hd_pos : d ≠ 0 := (factorizationEquiv.invFun ⟨dfac, dfac_prime⟩).2.ne'

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
hd_pos : d ≠ 0
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization