awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (hypothesis)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
⊢ motive (k + 2)
have htp : 0 < t
Tactic: haveI htp : 0 < t := hp.factorization_pos_of_dvd (k + 1).succ_ne_zero (k + 2).minFac_dvd
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ motive (k + 2)
have h : k + 2 = p ^ t * ((k + 2) / p ^ t)
Tactic: convert! prime_pow_mul ((k + 2) / p ^ t) p t hp _ htp (hk _ (Nat.div_lt_of_lt_mul _)) using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
h : k + 2 = p ^ t * ((k + 2) / p ^ t)
⊢ motive (k + 2)
have convert_1 : ¬p ∣ (k + 2) / p ^ t
Tactic: convert! prime_pow_mul ((k + 2) / p ^ t) p t hp _ htp (hk _ (Nat.div_lt_of_lt_mul _)) using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
h : k + 2 = p ^ t * ((k + 2) / p ^ t)
convert_1 : ¬p ∣ (k + 2) / p ^ t
⊢ motive (k + 2)
have convert_2 : k + 2 < p ^ t * (k + 2)
Tactic: convert! prime_pow_mul ((k + 2) / p ^ t) p t hp _ htp (hk _ (Nat.div_lt_of_lt_mul _)) using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ k + 2 = p ^ t * ((k + 2) / p ^ t)
have h : k + 2 = k + 2
Tactic: rw [Nat.mul_div_cancel' hpt]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
a n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := ((k + 2).factorization : (a : ℕ) → ℕ) p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ∣ (k + 2) / p ^ t
have convert_1 : ¬p ^ t.succ ∣ k + 2
Tactic: rw [Nat.dvd_div_iff_mul_dvd hpt, ← Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
⊢ motive (p ^ n * a)
have pos : (ha1 : a = 1) → motive (p ^ n * a)
Tactic: by_cases ha1 : a = 1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
pos : (ha1 : a = 1) → motive (p ^ n * a)
⊢ motive (p ^ n * a)
have neg : (ha1 : ¬a = 1) → motive (p ^ n * a)
Tactic: by_cases ha1 : a = 1
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n * a)
have pos : motive (p ^ n)
Tactic: rw [ha1, mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ motive (p ^ n * a)
have neg : 1 < a
Tactic: refine coprime (p ^ n) a (hp'.one_lt.trans_le (le_self_pow hn.ne' _)) ?_ ?_
      (prime_pow _ _ hp' hn) hPa
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
neg : 1 < a
⊢ motive (p ^ n * a)
have neg₁ : (p ^ n).Coprime a
Tactic: refine coprime (p ^ n) a (hp'.one_lt.trans_le (le_self_pow hn.ne' _)) ?_ ?_
      (prime_pow _ _ hp' hn) hPa
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
a_1 b m n_1 p_1 : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : ¬a = 1
⊢ 1 < a
have neg : ∀ (hpa : a ≤ 1), p ∣ a
Tactic: contrapose! hpa
Cleared hypotheses: hpa
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
⊢ ∀ (n : ℕ), motive n
have refine : ∀ (a p n : ℕ), Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
Tactic: refine recOnPrimePow zero one ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p ^ (n + 1) * a)
have succ : motive (p * (p ^ n * a))
Tactic: rw [pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p n : ℕ
hp : Prime p
ha : motive a
⊢ motive (p ^ n * a)
have zero₁ : motive (HPow.hPow (β := ℕ) p 0 * a)
Tactic: induction n with
  | zero => simpa using ha
  | succ n ih =>
    rw [pow_succ', mul_assoc]
    exact prime_mul _ _ hp ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p n : ℕ
hp : Prime p
ha : motive a
zero₁ : motive (HPow.hPow (β := ℕ) p 0 * a)
⊢ motive (p ^ n * a)
have succ : ∀ (n : ℕ) (ih : motive (p ^ n * a)), motive (p ^ (n + 1) * a)
Tactic: induction n with
  | zero => simpa using ha
  | succ n ih =>
    rw [pow_succ', mul_assoc]
    exact prime_mul _ _ hp ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
Goal:
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n : ℕ
⊢ motive n
have refine : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
Tactic: refine induction_on_primes zero one ?_ _
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
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
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
have prime_pow : ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
Tactic: apply Nat.recOnPosPrimePosCoprime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
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
prime_pow : ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
have zero : Ne (α := ℕ) 0 0 → f 0 = (factorization 0).prod fun (p k : ℕ) ↦ f (p ^ k)
Tactic: apply Nat.recOnPosPrimePosCoprime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
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
prime_pow : ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
zero : Ne (α := ℕ) 0 0 → f 0 = (factorization 0).prod fun (p k : ℕ) ↦ f (p ^ k)
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
have one : Ne (α := ℕ) 1 0 → f 1 = (factorization 1).prod fun (p k : ℕ) ↦ f (p ^ k)
Tactic: apply Nat.recOnPosPrimePosCoprime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
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
prime_pow : ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
zero : Ne (α := ℕ) 0 0 → f 0 = (factorization 0).prod fun (p k : ℕ) ↦ f (p ^ k)
one : Ne (α := ℕ) 1 0 → f 1 = (factorization 1).prod fun (p k : ℕ) ↦ f (p ^ k)
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
have coprime : ∀ (a b : ℕ),
  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: apply Nat.recOnPosPrimePosCoprime
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
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
⊢ f 1 = (factorization 1).prod fun (p k : ℕ) ↦ f (p ^ k)
have one : Eq.{u_1 + 1} (α := β) 1 (Finsupp.prod 0 fun (p k : ℕ) ↦ f (p ^ k))
Tactic: rw [factorization_one, hf]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
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
⊢ f (a * b) = (a * b).factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
have coprime : _root_.Disjoint a.factorization.support b.factorization.support
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
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
⊢ f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
have inl : f 0 = (factorization 0).prod fun (p k : ℕ) ↦ f (p ^ k)
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Induction (goal)
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)
⊢ f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
have inr : ∀ (hn : n ≠ 0), f n = n.factorization.prod fun (p k : ℕ) ↦ f (p ^ k)
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
⊢ 0 < a.factorizationLCMLeft b
have a₁ : a.factorizationLCMLeft b ≠ 0
Tactic: apply Nat.pos_of_ne_zero
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
⊢ a.factorizationLCMLeft b ≠ 0
have 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
Tactic: rw [factorizationLCMLeft, Finsupp.prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
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
⊢ False
have pos : ∀ (h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)), False
Tactic: by_cases h : b.factorization p ≤ a.factorization p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
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
⊢ False
have neg : ∀ (h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)), False
Tactic: by_cases h : b.factorization p ≤ a.factorization p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (hypothesis)
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
have H₁ : p = 0 ∧ ¬Eq (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: simp only [h, reduceIte, pow_eq_zero_iff', ne_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
⊢ 0 < a.factorizationLCMRight b
have a₁ : a.factorizationLCMRight b ≠ 0
Tactic: apply Nat.pos_of_ne_zero
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
⊢ a.factorizationLCMRight b ≠ 0
have 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
Tactic: rw [factorizationLCMRight, Finsupp.prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
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
⊢ False
have pos : ∀ (h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)), False
Tactic: by_cases h : b.factorization p ≤ a.factorization p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
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
⊢ False
have neg : ∀ (h : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)), False
Tactic: by_cases h : b.factorization p ≤ a.factorization p
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (hypothesis)
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
have H₁ : p = 0 ∧ ¬Eq (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: simp only [h, ↓reduceIte, pow_eq_zero_iff', ne_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
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)
have 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))
Tactic: refine coprime_prod_left_iff.mpr fun p hp ↦ coprime_prod_right_iff.mpr fun q hq ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (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).Coprime
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ) then 1
    else HPow.hPow (β := ℕ) q (((a.lcm b).factorization : (a : ℕ) → ℕ) q : ℕ))
have 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
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
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
⊢ (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 : ℕ))
have 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 : ℕ))
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
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 : ℕ))
⊢ (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 : ℕ))
have 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
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
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
⊢ (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 : ℕ))
have 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 : ℕ))
Tactic: split_ifs with h h'