awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
rw : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)

Tactic:
rw [primeFactorsList]

Premises used: Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ¬k + 2 = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
refine : ∀ (p : ℕ), Prime p → p ∣ (k + 2) / (k + 2).minFac → (k + 2).minFac ≤ p
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)

Tactic:
refine List.IsChain.cons_cons
        ((le_minFac.2 h).resolve_left (by simp)) (isChain_cons_primeFactorsList ?_)

Premises used: Iff.mpr, List.IsChain.cons_cons, Nat.le_minFac, Or.resolve_left
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / (k + 2).minFac → (k + 2).minFac ≤ p

Tactic:
fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)

Premises used: Nat.minFac_le_of_dvd, Nat.minFac_dvd, HAdd.hAdd, Nat.Prime.two_le, Nat.div_dvd_of_dvd, OfNat.ofNat, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / (k + 2).minFac → (k + 2).minFac ≤ p

Tactic:
exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)

Premises used: Nat.minFac_le_of_dvd
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: n.primeFactorsList)

Tactic:
match n with
  | 0 => simp
  | 1 => simp
  | k + 2 =>
      intro a h
      let m := minFac (k + 2)
      have : (k + 2) / m < (k + 2) := factors_lemma
      rw [primeFactorsList]
      refine List.IsChain.cons_cons
        ((le_minFac.2 h).resolve_left (by simp)) (isChain_cons_primeFactorsList ?_)
      exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (2 :: n.primeFactorsList)

Tactic:
isChain_cons_primeFactorsList fun _ pp _ => pp.two_le

Premises used: Nat.isChain_cons_primeFactorsList, Nat.Prime.two_le
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) n.primeFactorsList

Tactic:
(isChain_two_cons_primeFactorsList _).tail

Premises used: Nat.isChain_two_cons_primeFactorsList, WellFounded.Nat.fix, List.tail, List.IsChain.tail, WellFounded.Nat.fix.go
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ n.primeFactorsList.SortedLE

Tactic:
(isChain_primeFactorsList _).sortedLE

Premises used: Nat.isChain_primeFactorsList, List.IsChain.sortedLE
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
rw rw₁ :
  (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList =
    (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList
⊢ (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList

Tactic:
rw [primeFactorsList]

Premises used: Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
mp : n.primeFactorsList = [] → n = 0 ∨ n = 1
mpr : n = 0 ∨ n = 1 → n.primeFactorsList = []
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
h : n.primeFactorsList = []
mp : ∀ (h : primeFactorsList 0 = []), Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1
mp₁ : ∀ (h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList = []), HAdd.hAdd (α := ℕ) 0 1 = 0 ∨ HAdd.hAdd (α := ℕ) 0 1 = 1
mp₂ : ∀ (n : ℕ) (h : (n + 1 + 1).primeFactorsList = []), n + 1 + 1 = 0 ∨ n + 1 + 1 = 1
⊢ n = 0 ∨ n = 1

Tactic:
rcases n with (_ | _ | n)
-- Module: Mathlib.Data.Nat.Factors
Goal:
h : primeFactorsList 0 = []
⊢ Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
h : primeFactorsList 0 = []
⊢ Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList = []
⊢ HAdd.hAdd (α := ℕ) 0 1 = 0 ∨ HAdd.hAdd (α := ℕ) 0 1 = 1

Tactic:
Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList = []
⊢ HAdd.hAdd (α := ℕ) 0 1 = 0 ∨ HAdd.hAdd (α := ℕ) 0 1 = 1

Tactic:
exact Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []

Tactic:
rw [primeFactorsList] at h

Premises used: Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
h : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
injection h
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
h : n = 0 ∨ n = 1
mpr : primeFactorsList 0 = []
mpr₁ : primeFactorsList 1 = []
⊢ n.primeFactorsList = []

Tactic:
rcases h with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
⊢ primeFactorsList 0 = []

Tactic:
primeFactorsList_zero

Premises used: Nat.primeFactorsList_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
⊢ primeFactorsList 0 = []

Tactic:
exact primeFactorsList_zero

Premises used: Nat.primeFactorsList_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
⊢ primeFactorsList 1 = []

Tactic:
primeFactorsList_one

Premises used: Nat.primeFactorsList_one
-- Module: Mathlib.Data.Nat.Factors
Goal:
⊢ primeFactorsList 1 = []

Tactic:
exact primeFactorsList_one

Premises used: Nat.primeFactorsList_one
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
⊢ n.primeFactorsList ≠ [] ↔ 1 < n

Tactic:
simp [primeFactorsList_eq_nil n, one_lt_iff_ne_zero_and_ne_one]

Premises used: Nat.one_lt_iff_ne_zero_and_ne_one, Nat.primeFactorsList_eq_nil
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : a.primeFactorsList ~ b.primeFactorsList
⊢ a = b

Tactic:
simpa [prod_primeFactorsList ha, prod_primeFactorsList hb] using List.Perm.prod_eq h

Premises used: List.Perm.prod_eq, Nat.prod_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
inl : ∀ (h : p ∈ primeFactorsList 0), p ∣ 0
inr : ∀ (hn : n > 0), p ∣ n
⊢ p ∣ n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0

Tactic:
dvd_zero p

Premises used: dvd_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0

Tactic:
exact dvd_zero p

Premises used: dvd_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
inr inr₁ inr₂ inr₃ : p ∈ n.primeFactorsList
⊢ p ∣ n

Tactic:
rwa [← mem_primeFactorsList_iff_dvd hn.ne' (prime_of_mem_primeFactorsList h)]

Premises used: Nat.mem_primeFactorsList_iff_dvd, Nat.prime_of_mem_primeFactorsList, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
hn : n ≠ 0
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n

Tactic:
⟨fun h => ⟨prime_of_mem_primeFactorsList h, dvd_of_mem_primeFactorsList h⟩, fun ⟨hprime, hdvd⟩ =>
    (mem_primeFactorsList_iff_dvd hn hprime).mpr hdvd⟩

Premises used: Iff.mpr, Nat.mem_primeFactorsList_iff_dvd, Nat.prime_of_mem_primeFactorsList, Membership.mem, _private.0.Nat.mem_primeFactorsList.match_1, And.intro, Iff.intro, Nat.primeFactorsList, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
zero : p ∈ primeFactorsList 0 ↔ Prime p ∧ p ∣ 0 ∧ Ne (α := ℕ) 0 0
succ : ∀ (n : ℕ), p ∈ (n + 1).primeFactorsList ↔ Prime p ∧ p ∣ n + 1 ∧ n + 1 ≠ 0
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
⊢ p ∈ primeFactorsList 0 ↔ Prime p ∧ p ∣ 0 ∧ Ne (α := ℕ) 0 0

Tactic:
simp [mem_primeFactorsList, *]

Premises used: Nat.mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
p n : ℕ
⊢ p ∈ (n + 1).primeFactorsList ↔ Prime p ∧ p ∣ n + 1 ∧ n + 1 ≠ 0

Tactic:
simp [mem_primeFactorsList, *]

Premises used: Nat.mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
inl : ∀ (h : p ∈ primeFactorsList 0), p ≤ 0
inr : ∀ (hn : n > 0), p ≤ n
⊢ p ≤ n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
h : p ∈ primeFactorsList 0
⊢ Membership.mem (γ := List ℕ) [] p

Tactic:
rw [primeFactorsList_zero] at h

Premises used: Nat.primeFactorsList_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
h : Membership.mem (γ := List ℕ) [] p
⊢ p ≤ 0

Tactic:
cases h
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n

Tactic:
le_of_dvd hn (dvd_of_mem_primeFactorsList h)

Premises used: Nat.le_of_dvd, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n

Tactic:
exact le_of_dvd hn (dvd_of_mem_primeFactorsList h)

Premises used: Nat.le_of_dvd, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l ~ n.primeFactorsList

Tactic:
perm_of_prod_eq_prod ?_ ?_ ?_

Premises used: perm_of_prod_eq_prod
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
refine_1 : l.prod = n.primeFactorsList.prod
refine_2 : ∀ (p : ℕ), p ∈ l → _root_.Prime p
refine_3 : ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p
⊢ l ~ n.primeFactorsList

Tactic:
refine perm_of_prod_eq_prod ?_ ?_ ?_

Premises used: perm_of_prod_eq_prod
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
refine_1 : n = n.primeFactorsList.prod
⊢ l.prod = n.primeFactorsList.prod

Tactic:
rw [h₁]
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = n.primeFactorsList.prod

Tactic:
(prod_primeFactorsList ?_).symm

Premises used: Eq.symm, Nat.prod_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
refine_1 : n ≠ 0
⊢ n = n.primeFactorsList.prod

Tactic:
refine (prod_primeFactorsList ?_).symm

Premises used: Eq.symm, Nat.prod_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : l.prod = 0
⊢ 0 ∈ l

Tactic:
rw [prod_eq_zero_iff] at h₁

Premises used: List.prod_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factors
Goal:
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False

Tactic:
Prime.ne_zero (h₂ 0 h₁) rfl

Premises used: Nat.Prime.ne_zero, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False

Tactic:
exact Prime.ne_zero (h₂ 0 h₁) rfl

Premises used: Nat.Prime.ne_zero, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ refine_2 : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p

Tactic:
simp_rw [← prime_iff]

Premises used: Nat.prime_iff
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → Prime p

Tactic:
h₂
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → Prime p

Tactic:
exact h₂
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
refine_3 : ∀ (p : ℕ), p ∈ n.primeFactorsList → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p

Tactic:
simp_rw [← prime_iff]

Premises used: Nat.prime_iff
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → Prime p

Tactic:
fun p => prime_of_mem_primeFactorsList

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → Prime p

Tactic:
exact fun p => prime_of_mem_primeFactorsList

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
n : ℕ
symm : replicate n p = (p ^ n).primeFactorsList
⊢ (p ^ n).primeFactorsList = replicate n p

Tactic:
symm
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
n : ℕ
rw : replicate n p ~ (p ^ n).primeFactorsList
⊢ replicate n p = (p ^ n).primeFactorsList

Tactic:
rw [← List.replicate_perm]

Premises used: List.replicate_perm
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
n : ℕ
apply : ∀ (p_1 : ℕ), p_1 ∈ replicate n p → Prime p_1
⊢ replicate n p ~ (p ^ n).primeFactorsList

Tactic:
apply Nat.primeFactorsList_unique (List.prod_replicate n p)

Premises used: Nat.primeFactorsList_unique, List.prod_replicate
-- Module: Mathlib.Data.Nat.Factors
Goal:
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
rwa rwa₁ rwa₂ rwa₃ : Prime p
⊢ Prime q

Tactic:
rwa [eq_of_mem_replicate hq]

Premises used: List.eq_of_mem_replicate
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
set :
  let k := n.primeFactorsList.length;
  n = p ^ k
⊢ n = p ^ n.primeFactorsList.length

Tactic:
set k := n.primeFactorsList.length

Premises used: List.length, Nat.primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
rw : n.primeFactorsList.prod = p ^ k
rw₁ : n.primeFactorsList.prod = (replicate k p).prod
rw₂ rw₃ : (replicate n.primeFactorsList.length p).prod = (replicate k p).prod
⊢ n = p ^ k

Tactic:
rw [← prod_primeFactorsList hpos, ← prod_replicate k p, eq_replicate_of_mem fun d hd =>
    h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)]

Premises used: Nat.prime_of_mem_primeFactorsList, List.eq_replicate_of_mem, List.prod_replicate, Nat.prod_primeFactorsList, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
(primeFactorsList_unique ?_ ?_).symm

Premises used: Nat.primeFactorsList_unique, List.Perm.symm
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
refine_1 : (a.primeFactorsList ++ b.primeFactorsList).prod = a * b
refine_2 : ∀ (p : ℕ), p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
refine (primeFactorsList_unique ?_ ?_).symm

Premises used: Nat.primeFactorsList_unique, List.Perm.symm
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
refine_1 : a.primeFactorsList.prod * b.primeFactorsList.prod = a * b
refine_1₁ : a * b.primeFactorsList.prod = a * b
refine_1₂ refine_1₃ : a * b = a * b
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b

Tactic:
rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]

Premises used: List.prod_append, Nat.prod_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ++ b.primeFactorsList
⊢ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

Tactic:
rw [List.mem_append] at hp

Premises used: List.mem_append
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
refine_2 : ∀ (hp' : p ∈ a.primeFactorsList), Prime p
refine_2₁ : ∀ (hp' : p ∈ b.primeFactorsList), Prime p
⊢ Prime p

Tactic:
rcases hp with hp' | hp'
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ a.primeFactorsList
⊢ Prime p

Tactic:
prime_of_mem_primeFactorsList hp'

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ a.primeFactorsList
⊢ Prime p

Tactic:
exact prime_of_mem_primeFactorsList hp'

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ b.primeFactorsList
⊢ Prime p

Tactic:
prime_of_mem_primeFactorsList hp'

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ b.primeFactorsList
⊢ Prime p

Tactic:
exact prime_of_mem_primeFactorsList hp'

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
inl : ∀ (hab : Coprime 0 b), (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList
inr : ∀ (ha : a > 0), (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
rcases a.eq_zero_or_pos with (rfl | ha)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
b : ℕ
hab : Coprime 0 b
⊢ (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList

Tactic:
simp [(coprime_zero_left _).mp hab]

Premises used: Nat.coprime_zero_left, Iff.mp
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
ha : a > 0
inr : ∀ (hab : a.Coprime 0), (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0
inr₁ : ∀ (hb : b > 0), (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0

Tactic:
simp [(coprime_zero_right _).mp hab]

Premises used: Nat.coprime_zero_right, Iff.mp
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
ha : a > 0
hb : b > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
perm_primeFactorsList_mul ha.ne' hb.ne'

Premises used: LT.lt.ne', Nat.perm_primeFactorsList_mul
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
hab : a.Coprime b
ha : a > 0
hb : b > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
exact perm_primeFactorsList_mul ha.ne' hb.ne'

Premises used: LT.lt.ne', Nat.perm_primeFactorsList_mul
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k : ℕ
h : k ≠ 0
zero : primeFactorsList 0 <+ (0 * k).primeFactorsList
succ : ∀ (hn : ℕ), (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList
⊢ n.primeFactorsList <+ (n * k).primeFactorsList

Tactic:
rcases n with - | hn
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h : k ≠ 0
⊢ primeFactorsList 0 <+ (0 * k).primeFactorsList

Tactic:
simp [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h : k ≠ 0
hn : ℕ
apply : (hn + 1).primeFactorsList <+~ ((hn + 1) * k).primeFactorsList
⊢ (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList

Tactic:
apply sublist_of_subperm_of_pairwise _
    (primeFactorsList_sorted _).pairwise (primeFactorsList_sorted _).pairwise

Premises used: Nat.primeFactorsList_sorted, List.sublist_of_subperm_of_pairwise, List.SortedLE.pairwise
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h : k ≠ 0
hn : ℕ
simp : (hn + 1).primeFactorsList <+~ hn.succ.primeFactorsList ++ k.primeFactorsList
⊢ (hn + 1).primeFactorsList <+~ ((hn + 1) * k).primeFactorsList

Tactic:
simp only [(perm_primeFactorsList_mul (Nat.succ_ne_zero _) h).subperm_left]

Premises used: Nat.succ_ne_zero, Nat.perm_primeFactorsList_mul, List.Perm.subperm_left
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ hn.succ.primeFactorsList ++ k.primeFactorsList

Tactic:
(sublist_append_left _ _).subperm

Premises used: List.sublist_append_left, List.Sublist.subperm
-- Module: Mathlib.Data.Nat.Factors
Goal:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ hn.succ.primeFactorsList ++ k.primeFactorsList

Tactic:
exact (sublist_append_left _ _).subperm

Premises used: List.sublist_append_left, List.Sublist.subperm
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k : ℕ
h : n ∣ k
h' : k ≠ 0
obtain : ∀ (a : ℕ) (h' : n * a ≠ 0), n.primeFactorsList <+ (n * a).primeFactorsList
⊢ n.primeFactorsList <+ k.primeFactorsList

Tactic:
obtain ⟨a, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
n a : ℕ
h' : n * a ≠ 0
⊢ n.primeFactorsList <+ (n * a).primeFactorsList

Tactic:
primeFactorsList_sublist_right (right_ne_zero_of_mul h')

Premises used: right_ne_zero_of_mul, Nat.primeFactorsList_sublist_right
-- Module: Mathlib.Data.Nat.Factors
Goal:
n a : ℕ
h' : n * a ≠ 0
⊢ n.primeFactorsList <+ (n * a).primeFactorsList

Tactic:
exact primeFactorsList_sublist_right (right_ne_zero_of_mul h')

Premises used: right_ne_zero_of_mul, Nat.primeFactorsList_sublist_right
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k : ℕ
h : k ≠ 0
⊢ n.primeFactorsList ⊆ (n * k).primeFactorsList

Tactic:
(primeFactorsList_sublist_right h).subset

Premises used: Nat.primeFactorsList_sublist_right, List.Sublist.subset
-- Module: Mathlib.Data.Nat.Factors
Goal:
n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ n.primeFactorsList ⊆ k.primeFactorsList

Tactic:
(primeFactorsList_sublist_of_dvd h h').subset

Premises used: List.Sublist.subset, Nat.primeFactorsList_sublist_of_dvd
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
inl : ∀ (h : a.primeFactorsList <+~ primeFactorsList 0), a ∣ 0
inr : ∀ (hb : b > 0), a ∣ b
⊢ a ∣ b

Tactic:
rcases b.eq_zero_or_pos with (rfl | hb)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Data.Nat.Factors
Goal:
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
inr : ∀ (ha : Ne (α := ℕ) 0 0) (h : primeFactorsList 0 <+~ b.primeFactorsList), 0 ∣ b
inr₁ :
  ∀ (ha : HAdd.hAdd (α := ℕ) 0 1 ≠ 0) (h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList <+~ b.primeFactorsList),
    HAdd.hAdd (α := ℕ) 0 1 ∣ b
inr₂ : ∀ (a : ℕ) (ha : a + 1 + 1 ≠ 0) (h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList), a + 1 + 1 ∣ b
⊢ a ∣ b

Tactic:
rcases a with (_ | _ | a)
-- Module: Mathlib.Data.Nat.Factors
Goal:
b : ℕ
hb : b > 0
ha : Ne (α := ℕ) 0 0
h : primeFactorsList 0 <+~ b.primeFactorsList
⊢ 0 ∣ b

Tactic:
(ha rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
b : ℕ
hb : b > 0
ha : Ne (α := ℕ) 0 0
h : primeFactorsList 0 <+~ b.primeFactorsList
⊢ 0 ∣ b

Tactic:
exact (ha rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Nat.Factors
Goal:
b : ℕ
hb : b > 0
ha : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList <+~ b.primeFactorsList
⊢ HAdd.hAdd (α := ℕ) 0 1 ∣ b

Tactic:
one_dvd _

Premises used: one_dvd
-- Module: Mathlib.Data.Nat.Factors
Goal:
b : ℕ
hb : b > 0
ha : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList <+~ b.primeFactorsList
⊢ HAdd.hAdd (α := ℕ) 0 1 ∣ b

Tactic:
exact one_dvd _

Premises used: one_dvd
-- Module: Mathlib.Data.Nat.Factors
Goal:
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
h₁ : b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
⊢ a + 1 + 1 ∣ b

Tactic:
use (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Premises used: List.diff, Nat.succ, List.prod, Nat.primeFactorsList