a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
let dfac := a.factorization ⊓ b.factorization
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
let d := dfac.prod Nat.pow
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
have dfac_prime : ∀ p : ℕ, p ∈ dfac.support → Prime p := by
  intro p hp
  have : p ∈ a.factors ∧ p ∈ b.factors := by simpa using hp
  exact prime_of_mem_factors this.1
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
have h1 : d.factorization = dfac := prod_pow_factorization_eq_self dfac_prime
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
have hd_pos : d ≠ 0 := (factorizationEquiv.invFun ⟨dfac, dfac_prime⟩).2.ne'
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d = gcd a b
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
suffices d = gcd a b by rwa [← this]
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d ∣ a

case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d ∣ b

case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d = gcd a b
apply gcd_greatest
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
p : ℕ
hp : p ∈ dfac.support
⊢ Prime p
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
⊢ ∀ (p : ℕ), p ∈ dfac.support → Prime p
intro p hp
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
p : ℕ
hp : p ∈ dfac.support
this : p ∈ factors a ∧ p ∈ factors b
⊢ Prime p
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
p : ℕ
hp : p ∈ dfac.support
⊢ Prime p
have : p ∈ a.factors ∧ p ∈ b.factors := by simpa using hp
no goals
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
p : ℕ
hp : p ∈ dfac.support
this : p ∈ factors a ∧ p ∈ factors b
⊢ Prime p
exact prime_of_mem_factors this.1
no goals
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
p : ℕ
hp : p ∈ dfac.support
⊢ p ∈ factors a ∧ p ∈ factors b
simpa using hp
no goals
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
this : d = gcd a b
⊢ factorization (gcd a b) = factorization a ⊓ factorization b
rwa [← this]
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ factorization a
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d ∣ a
rw [← factorization_le_iff_dvd hd_pos ha_pos, h1]
no goals
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ factorization a
exact inf_le_left
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ factorization b
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ d ∣ b
rw [← factorization_le_iff_dvd hd_pos hb_pos, h1]
no goals
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ dfac ≤ factorization b
exact inf_le_right
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
⊢ e ∣ d
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d
intro e hea heb
case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = 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 : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ d
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
⊢ e ∣ d
rcases Decidable.eq_or_ne e 0 with (rfl | he_pos)
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : factorization e ≤ factorization a
⊢ e ∣ d
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ d
have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : factorization e ≤ factorization a
heb' : factorization e ≤ factorization b
⊢ e ∣ d
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : factorization e ≤ factorization a
⊢ e ∣ d
have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb
no goals
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : factorization e ≤ factorization a
heb' : factorization e ≤ factorization b
⊢ e ∣ d
simp [← factorization_le_iff_dvd he_pos hd_pos, h1, hea', heb']
case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
heb : 0 ∣ b
hea : a = 0
⊢ 0 ∣ d
case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ d
simp only [zero_dvd_iff] at hea
no goals
case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
dfac : ℕ →₀ ℕ := factorization a ⊓ factorization b
d : ℕ := Finsupp.prod dfac Nat.pow
dfac_prime : ∀ (p : ℕ), p ∈ dfac.support → Prime p
h1 : factorization d = dfac
hd_pos : d ≠ 0
heb : 0 ∣ b
hea : a = 0
⊢ 0 ∣ d
contradiction