-- Mathlib/Data/Nat/Factorization/Basic.lean
lemma factorizationLCMLeft_dvd_left : factorizationLCMLeft a b ∣ a

Proof state:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.factorization ⊔ b.factorization) p ∣ p ^ a.factorization p

Tactic:
apply pow_dvd_pow

Result:
case pos.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ (a.factorization ⊔ b.factorization) p ≤ a.factorization p

Proof state:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ a_1 ∈ (a.lcm b).factorization.support,
    (fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1) a_1 ((a.lcm b).factorization a_1) ∣
      a_1 ^ a.factorization a_1

Tactic:
rintro p -

Result:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p) ∣
    p ^ a.factorization p

Proof state:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization.support ⊆ (a.lcm b).factorization.support

Tactic:
intro p hp

Result:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.factorization.support
⊢ p ∈ (a.lcm b).factorization.support

Proof state:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ a.factorization p

Tactic:
rw [factorization_lcm ha hb]

Result:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.factorization ⊔ b.factorization) p ∣ p ^ a.factorization p

Proof state:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ a.factorization x

Tactic:
apply prod_dvd_prod_of_dvd

Result:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ a_1 ∈ (a.lcm b).factorization.support,
    (fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1) a_1 ((a.lcm b).factorization a_1) ∣
      a_1 ^ a.factorization a_1

Proof state:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) ∣ p ^ a.factorization p

Tactic:
split_ifs with le

Result:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ a.factorization p

case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ a.factorization p

Proof state:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
intros

Result:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
i✝ : ℕ
a✝ : i✝ ∈ (a.lcm b).factorization.support
⊢ i✝ ^ 0 = 1

Proof state:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.factorization.support
⊢ p ∈ (a.lcm b).factorization.support

Tactic:
rw [mem_support_iff] at hp ⊢

Result:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.lcm b).factorization p ≠ 0

Proof state:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
nth_rewrite 2 [← factorization_prod_pow_eq_self ha]

Result:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a.factorization.prod fun x1 x2 => x1 ^ x2

Proof state:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0

Tactic:
exact (lt_sup_iff.mpr <| .inl <| Nat.pos_of_ne_zero hp).ne'

Result:
no goals

Proof state:
case inl
b : ℕ
⊢ factorizationLCMLeft 0 b ∣ 0

Tactic:
simp only [dvd_zero]

Result:
no goals

Proof state:
case inr.inl
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft 0 ∣ a

Tactic:
simp [factorizationLCMLeft]

Result:
no goals

Proof state:
case pos.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ (a.factorization ⊔ b.factorization) p ≤ a.factorization p

Tactic:
exact sup_le le_rfl le

Result:
no goals

Proof state:
a b : ℕ
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Result:
case inl
b : ℕ
⊢ factorizationLCMLeft 0 b ∣ 0

case inr
a b : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft b ∣ a

Proof state:
case inr
a b : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Result:
case inr.inl
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft 0 ∣ a

case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a

Proof state:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p) ∣
    p ^ a.factorization p

Tactic:
dsimp only

Result:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) ∣ p ^ a.factorization p

Proof state:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ a.factorization p

Tactic:
apply one_dvd

Result:
no goals

Proof state:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a.factorization.prod fun x1 x2 => x1 ^ x2

Tactic:
rw [prod_of_support_subset (s := (lcm a b).factorization.support)]

Result:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ a.factorization x

case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization.support ⊆ (a.lcm b).factorization.support

case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Proof state:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
i✝ : ℕ
a✝ : i✝ ∈ (a.lcm b).factorization.support
⊢ i✝ ^ 0 = 1

Tactic:
rw [pow_zero]

Result:
no goals

Proof state:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.lcm b).factorization p ≠ 0

Tactic:
rw [factorization_lcm ha hb]

Result:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0