-- Mathlib/Data/Nat/Factorization/Basic.lean
lemma coprime_factorizationLCMLeft_factorizationLCMRight :
    (factorizationLCMLeft a b).Coprime (factorizationLCMRight a b)

Proof state:
a b : ℕ
⊢ ((a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1).Coprime
    ((a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n)

Tactic:
refine coprime_prod_left_iff.mpr fun p hp ↦ coprime_prod_right_iff.mpr fun q hq ↦ ?_

Result:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ ((fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p)).Coprime
    ((fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n) q ((a.lcm b).factorization q))

Proof state:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : p = q
⊢ b.factorization q ≤ a.factorization q

Tactic:
rwa [← h']

Result:
no goals

Proof state:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : ¬b.factorization q ≤ a.factorization q
⊢ Coprime 1 (q ^ (a.lcm b).factorization q)

Tactic:
simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

Result:
no goals

Proof state:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ ((fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p)).Coprime
    ((fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n) q ((a.lcm b).factorization q))

Tactic:
dsimp only

Result:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1).Coprime
    (if b.factorization q ≤ a.factorization q then 1 else q ^ (a.lcm b).factorization q)

Proof state:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
⊢ (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1).Coprime
    (if b.factorization q ≤ a.factorization q then 1 else q ^ (a.lcm b).factorization q)

Tactic:
split_ifs with h h'

Result:
case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime 1

case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)

case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : b.factorization q ≤ a.factorization q
⊢ Coprime 1 1

case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : ¬b.factorization q ≤ a.factorization q
⊢ Coprime 1 (q ^ (a.lcm b).factorization q)

Proof state:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ p ≠ q

Tactic:
contrapose! h'

Result:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : p = q
⊢ b.factorization q ≤ a.factorization q

Proof state:
case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime 1

case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)

case pos
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : b.factorization q ≤ a.factorization q
⊢ Coprime 1 1

case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬b.factorization p ≤ a.factorization p
h✝ : ¬b.factorization q ≤ a.factorization q
⊢ Coprime 1 (q ^ (a.lcm b).factorization q)

Tactic:
any_goals simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

Result:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)

Proof state:
a b : ℕ
⊢ (a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)

Tactic:
rw [factorizationLCMLeft, factorizationLCMRight]

Result:
a b : ℕ
⊢ ((a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1).Coprime
    ((a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n)

Proof state:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ (p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)

Tactic:
refine coprime_pow_primes _ _ (prime_of_mem_primeFactors hp) (prime_of_mem_primeFactors hq) ?_

Result:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : ¬b.factorization q ≤ a.factorization q
⊢ p ≠ q