a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization a + factorization b = factorization a ⊓ factorization b + factorization a ⊔ factorization b
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization (lcm a b) = factorization a ⊔ factorization b
rw [← add_right_inj (a.gcd b).factorization, ←
  factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm,
  factorization_gcd ha hb, factorization_mul ha hb]
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ ↑(factorization a + factorization b) a✝ = ↑(factorization a ⊓ factorization b + factorization a ⊔ factorization b) a✝
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization a + factorization b = factorization a ⊓ factorization b + factorization a ⊔ factorization b
ext1
no goals
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ ↑(factorization a + factorization b) a✝ = ↑(factorization a ⊓ factorization b + factorization a ⊔ factorization b) a✝
exact (min_add_max _ _).symm