awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
coprime :
  1 < a →
    1 < b →
      a.Coprime b →
        (a ≠ 0 → f a = a.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
          (b ≠ 0 → f b = b.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
            a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
⊢ 1 < a →
    1 < b →
      a.Coprime b →
        (a ≠ 0 → f a = a.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
          (b ≠ 0 → f b = b.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
            a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
_
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
h : 1 < a
coprime :
  1 < b →
    a.Coprime b →
      (a ≠ 0 → f a = a.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
        (b ≠ 0 → f b = b.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
          a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
⊢ 1 < b →
    a.Coprime b →
      (a ≠ 0 → f a = a.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
        (b ≠ 0 → f b = b.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)) →
          a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
_
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
h : 1 < a
h_1 : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
hab_pos : a * b ≠ 0
coprime : _root_.Disjoint a.factorization.support b.factorization.support
⊢ f (a * b) = (a * b).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
rw [h_mult a b hab, ha (left_ne_zero_of_mul hab_pos), hb (right_ne_zero_of_mul hab_pos),
      factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]

Premises used: Finsupp.prod_add_index_of_disjoint, right_ne_zero_of_mul, left_ne_zero_of_mul, Nat.factorization_mul_of_coprime
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
h : 1 < a
h_1 : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ _root_.Disjoint a.factorization.support b.factorization.support

Tactic:
hab.disjoint_primeFactors

Premises used: Multiset.toFinset, List.toFinset, Nat.Coprime.disjoint_primeFactors, Nat.primeFactors
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
h : 1 < a
h_1 : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ _root_.Disjoint a.factorization.support b.factorization.support

Tactic:
exact hab.disjoint_primeFactors

Premises used: Nat.Coprime.disjoint_primeFactors
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
n : ℕ
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
inl : f 0 = (factorization 0).prod fun (p k : ℕ) ↦ f (p ^ k)
inr : ∀ (hn : n ≠ 0), f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
⊢ f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 0 = (factorization 0).prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
n : ℕ
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
hn : n ≠ 0
⊢ f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
multiplicative_factorization _ h_mult hf1 hn

Premises used: Nat.multiplicative_factorization
-- Module: Mathlib.Data.Nat.Factorization.Induction
Goal:
n : ℕ
β : Type u_1
inst : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
hn : n ≠ 0
⊢ f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)

Tactic:
exact multiplicative_factorization _ h_mult hf1 hn

Premises used: Nat.multiplicative_factorization
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
b : ℕ
⊢ factorizationLCMLeft 0 b = 1

Tactic:
simp [factorizationLCMLeft]

Premises used: Nat.factorizationLCMLeft
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a : ℕ
⊢ a.factorizationLCMLeft 0 = 1

Tactic:
simp [factorizationLCMLeft]

Premises used: Nat.factorizationLCMLeft
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
b : ℕ
⊢ factorizationLCMRight 0 b = 1

Tactic:
simp [factorizationLCMRight]

Premises used: Nat.factorizationLCMRight
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a : ℕ
⊢ a.factorizationLCMRight 0 = 1

Tactic:
simp [factorizationLCMRight]

Premises used: Nat.factorizationLCMRight
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
a₁ : a.factorizationLCMLeft b ≠ 0
⊢ 0 < a.factorizationLCMLeft b

Tactic:
apply Nat.pos_of_ne_zero

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
a₁ :
  ∀ i ∈ (a.lcm b).factorization.support,
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) i : ℕ) ((a.factorization : (a : ℕ) → ℕ) i : ℕ) then
        HPow.hPow (β := ℕ) i (((a.lcm b).factorization : (a : ℕ) → ℕ) i : ℕ)
      else 1) ≠
      0
⊢ a.factorizationLCMLeft b ≠ 0

Tactic:
rw [factorizationLCMLeft, Finsupp.prod_ne_zero_iff]

Premises used: Finsupp.prod_ne_zero_iff, Nat.factorizationLCMLeft
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
a₁ :
  p ∈ (a.lcm b).factorization.support →
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
        HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
      else 1) ≠
      0
⊢ p ∈ (a.lcm b).factorization.support →
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
        HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
      else 1) ≠
      0

Tactic:
_
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
h : p ∈ (a.lcm b).factorization.support
H :
  (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
      HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
    else 1) =
    0
pos : ∀ (h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)), False
neg : ∀ (h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)), False
⊢ False

Tactic:
by_cases h : b.factorization p ≤ a.factorization p

Premises used: DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
h_1 : p ∈ (a.lcm b).factorization.support
H :
  (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
      HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
    else 1) =
    0
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p = 0 ∧ ¬Eq (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp only [h, reduceIte, pow_eq_zero_iff', ne_eq] at H

Premises used: pow_eq_zero_iff', ne_eq, reduceIte
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
h_1 : p ∈ (a.lcm b).factorization.support
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
H : p = 0 ∧ ¬Eq (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ False

Tactic:
simpa [H.1] using H.2

Premises used: And.right, And.left
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
h_1 : p ∈ (a.lcm b).factorization.support
H :
  (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
      HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
    else 1) =
    0
h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ False

Tactic:
simp only [h, reduceIte, one_ne_zero] at H

Premises used: reduceIte, one_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
a₁ : a.factorizationLCMRight b ≠ 0
⊢ 0 < a.factorizationLCMRight b

Tactic:
apply Nat.pos_of_ne_zero

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
a₁ :
  ∀ i ∈ (a.lcm b).factorization.support,
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) i : ℕ) ((a.factorization : (a : ℕ) → ℕ) i : ℕ) then 1
      else HPow.hPow (β := ℕ) i (((a.lcm b).factorization : (a : ℕ) → ℕ) i : ℕ)) ≠
      0
⊢ a.factorizationLCMRight b ≠ 0

Tactic:
rw [factorizationLCMRight, Finsupp.prod_ne_zero_iff]

Premises used: Nat.factorizationLCMRight, Finsupp.prod_ne_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
a₁ :
  p ∈ (a.lcm b).factorization.support →
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
      else HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)) ≠
      0
⊢ p ∈ (a.lcm b).factorization.support →
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
      else HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)) ≠
      0

Tactic:
_
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
h : p ∈ (a.lcm b).factorization.support
H :
  (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
    else HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)) =
    0
pos : ∀ (h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)), False
neg : ∀ (h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)), False
⊢ False

Tactic:
by_cases h : b.factorization p ≤ a.factorization p

Premises used: DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
h_1 : p ∈ (a.lcm b).factorization.support
H :
  (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
    else HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)) =
    0
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ False

Tactic:
simp only [h, reduceIte, reduceCtorEq] at H

Premises used: reduceCtorEq, reduceIte
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
h_1 : p ∈ (a.lcm b).factorization.support
H :
  (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
    else HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)) =
    0
h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p = 0 ∧ ¬Eq (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
simp only [h, ↓reduceIte, pow_eq_zero_iff', ne_eq] at H

Premises used: pow_eq_zero_iff', ne_eq, reduceIte
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
h_1 : p ∈ (a.lcm b).factorization.support
h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
H : p = 0 ∧ ¬Eq (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ False

Tactic:
simpa [H.1] using H.2

Premises used: And.right, And.left
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
⊢ Coprime
    ((a.lcm b).factorization.prod fun (p n : ℕ) ↦
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
      else 1)
    ((a.lcm b).factorization.prod fun (p n : ℕ) ↦
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
      else p ^ n)

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

Premises used: Iff.mpr, Nat.coprime_prod_left_iff, Finsupp.prod, Nat.coprime_prod_right_iff
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
refine :
  ∀ (p : ℕ) (hp : p ∈ (a.lcm b).factorization.support) (q : ℕ) (hq : q ∈ (a.lcm b).factorization.support),
    Coprime
      ((fun (p n : ℕ) ↦
          if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
          else 1)
        p (((a.lcm b).factorization : (a : ℕ) → ℕ) p))
      ((fun (p n : ℕ) ↦
          if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
          else p ^ n)
        q (((a.lcm b).factorization : (a : ℕ) → ℕ) q))
⊢ Coprime
    ((a.lcm b).factorization.prod fun (p n : ℕ) ↦
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
      else 1)
    ((a.lcm b).factorization.prod fun (p n : ℕ) ↦
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
      else p ^ n)

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

Premises used: Iff.mpr, Nat.coprime_prod_left_iff, Nat.coprime_prod_right_iff
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
pos :
  ∀ (h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ))
    (h' : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)),
    (HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)).Coprime 1
neg :
  ∀ (h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ))
    (h' : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)),
    (HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)).Coprime
      (HPow.hPow (β := ℕ) q (((a.lcm b).factorization : (a : ℕ) → ℕ) q : ℕ))
pos₁ :
  ∀ (h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) → Coprime 1 1
neg₁ :
  ∀ (h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) →
      Coprime 1 (HPow.hPow (β := ℕ) q (((a.lcm b).factorization : (a : ℕ) → ℕ) q : ℕ))
⊢ (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
        HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
      else 1).Coprime
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) then 1
    else HPow.hPow (β := ℕ) q (((a.lcm b).factorization : (a : ℕ) → ℕ) q : ℕ))

Tactic:
split_ifs with h h'
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h' : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ (HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)).Coprime 1

Tactic:
simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

Premises used: Nat.coprime_one_right_eq_true, Nat.coprime_one_left_eq_true
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h_1 : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ Coprime 1 1

Tactic:
simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

Premises used: Nat.coprime_one_right_eq_true, Nat.coprime_one_left_eq_true
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h_1 : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ Coprime 1 (HPow.hPow (β := ℕ) q (((a.lcm b).factorization : (a : ℕ) → ℕ) q : ℕ))

Tactic:
simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]

Premises used: Nat.coprime_one_right_eq_true, Nat.coprime_one_left_eq_true
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h' : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ (HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)).Coprime
    (HPow.hPow (β := ℕ) q (((a.lcm b).factorization : (a : ℕ) → ℕ) q : ℕ))

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

Premises used: Nat.prime_of_mem_primeFactors, Nat.coprime_pow_primes
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h' : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
neg : p ≠ q
⊢ (HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)).Coprime
    (HPow.hPow (β := ℕ) q (((a.lcm b).factorization : (a : ℕ) → ℕ) q : ℕ))

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

Premises used: Nat.prime_of_mem_primeFactors, Nat.coprime_pow_primes
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h' : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
neg : ∀ (h' : p = q), LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ p ≠ q

Tactic:
contrapose h'
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h' : p = q
neg neg₁ neg₂ neg₃ : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)

Tactic:
rwa [← h']
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
rw :
  Eq (α := ℕ)
    ((a.lcm b).factorization.prod fun (a_1 b_1 : ℕ) ↦
      (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then
          a_1 ^ b_1
        else 1) *
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then 1
        else a_1 ^ b_1)
    ((a.lcm b).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
⊢ a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b

Tactic:
rw [← prod_factorization_pow_eq_self (lcm_ne_zero ha hb), factorizationLCMLeft,
    factorizationLCMRight, ← prod_mul]

Premises used: Nat.factorizationLCMRight, Finsupp.prod_mul, Nat.lcm_ne_zero, Nat.factorizationLCMLeft, Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
e_g :
  Eq (α := ℕ → ℕ → ℕ)
    (fun (a_1 b_1 : ℕ) ↦
      (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then
          a_1 ^ b_1
        else 1) *
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then 1
        else a_1 ^ b_1)
    fun (x1 x2 : ℕ) ↦ x1 ^ x2
⊢ Eq (α := ℕ)
    ((a.lcm b).factorization.prod fun (a_1 b_1 : ℕ) ↦
      (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then
          a_1 ^ b_1
        else 1) *
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then 1
        else a_1 ^ b_1)
    ((a.lcm b).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
congr
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
e_g :
  ∀ (p n : ℕ),
    ((if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
        else 1) *
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
        else p ^ n) =
      p ^ n
⊢ Eq (α := ℕ → ℕ → ℕ)
    (fun (a_1 b_1 : ℕ) ↦
      (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then
          a_1 ^ b_1
        else 1) *
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then 1
        else a_1 ^ b_1)
    fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
ext p n
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
pos : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) → p ^ n * 1 = p ^ n
neg :
  ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) → 1 * p ^ n = p ^ n
⊢ ((if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
      else 1) *
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
      else p ^ n) =
    p ^ n

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p ^ n * 1 = p ^ n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ 1 * p ^ n = p ^ n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
inl : factorizationLCMLeft 0 b ∣ 0
inr : ∀ (ha : a ≠ 0), a.factorizationLCMLeft b ∣ a
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
b : ℕ
⊢ factorizationLCMLeft 0 b ∣ 0

Tactic:
simp only [dvd_zero]

Premises used: dvd_zero
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a b : ℕ
ha : a ≠ 0
inr : a.factorizationLCMLeft 0 ∣ a
inr₁ : ∀ (hb : b ≠ 0), a.factorizationLCMLeft b ∣ a
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.LCM
Goal:
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft 0 ∣ a

Tactic:
simp [factorizationLCMLeft]

Premises used: Nat.factorizationLCMLeft