-- Mathlib/Data/Nat/Factorization/Basic.lean
lemma factorizationLCMRight_dvd_right : factorizationLCMRight a b ∣ b

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

Tactic:
apply one_dvd

Result:
no goals

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

Tactic:
exact sup_le (not_le.1 le).le le_rfl

Result:
no goals

Proof state:
case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) ∣ p ^ b.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
⊢ 1 ∣ p ^ b.factorization p

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

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

Tactic:
rcases eq_or_ne b 0 with rfl | hb

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

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

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

Tactic:
rcases eq_or_ne a 0 with rfl | ha

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

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

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

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

Result:
no goals

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

Tactic:
apply Finset.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 1 else p ^ n) a_1 ((a.lcm b).factorization a_1) ∣
      a_1 ^ b.factorization a_1

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

Tactic:
apply pow_dvd_pow

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

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

Tactic:
simp only [dvd_zero]

Result:
no goals

Proof state:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ b.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.factorizationLCMRight b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ b.factorization x

case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.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
p : ℕ
⊢ (fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n) p ((a.lcm b).factorization p) ∣
    p ^ b.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 1 else p ^ (a.lcm b).factorization p) ∣ p ^ b.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 : b.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 : b.factorization p ≠ 0
⊢ (a.factorization ⊔ b.factorization) p ≠ 0

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

Tactic:
simp [factorizationLCMRight]

Result:
no goals

Proof state:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ b.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 : b.factorization p ≠ 0
⊢ (a.lcm b).factorization p ≠ 0

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 1 else p ^ n) a_1 ((a.lcm b).factorization a_1) ∣
      a_1 ^ b.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 1 else p ^ n) p ((a.lcm b).factorization p) ∣
    p ^ b.factorization p

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

Tactic:
rw [factorization_lcm ha hb]

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

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

Tactic:
nth_rewrite 2 [← factorization_prod_pow_eq_self hb]

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

Proof state:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.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 ∈ b.factorization.support
⊢ p ∈ (a.lcm b).factorization.support

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