awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
rcases :
  ∀ (x : β → ℤ) (hxT : Membership.mem (γ := Finset (β → ℤ)) T x) (y : β → ℤ)
    (hyT : Membership.mem (γ := Finset (β → ℤ)) T y) (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y),
    ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rcases₁ :
  ∀ (x : β → ℤ) (hxT : Membership.mem (γ := Finset (β → ℤ)) T x) (y : β → ℤ)
    (hyT : Membership.mem (γ := Finset (β → ℤ)) T y) (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y),
    ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rcases₂ :
  ∀ (x : β → ℤ) (hxT : Membership.mem (γ := Finset (β → ℤ)) T x) (y : β → ℤ)
    (hyT : Membership.mem (γ := Finset (β → ℤ)) T y) (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y)
    (n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e), ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rcases₃ rcases₄ :
  ∀ (x : β → ℤ) (hxT : Membership.mem (γ := Finset (β → ℤ)) T x) (y : β → ℤ)
    (hyT : Membership.mem (γ := Finset (β → ℤ)) T y) (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y)
    (n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e) (i : β) (j : Unit),
    ‖replicateCol Unit (x - y) i j‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rcases₅ :
  ∀ (x : β → ℤ) (hxT : Membership.mem (γ := Finset (β → ℤ)) T x) (y : β → ℤ)
    (hyT : Membership.mem (γ := Finset (β → ℤ)) T y) (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y)
    (n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e) (i : β) (j : Unit),
    ‖x i - y i‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have rcases₆ : ∀ (x : β → ℤ) (hxT : Membership.mem (γ := Finset (β → ℤ)) T x) (y : β → ℤ)
  (hyT : Membership.mem (γ := Finset (β → ℤ)) T y) (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y)
  (n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e) (i : β) (j : Unit),
  (↑|x i - y i| : ℝ) ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
Tactic: classical
  -- Pigeonhole
  rcases Finset.exists_ne_map_eq_of_card_lt_of_maps_to
    (card_S_lt_card_T A hn hm) (image_T_subset_S A)
    with ⟨x, hxT, y, hyT, hneq, hfeq⟩
  -- Proofs that x - y ≠ 0 and x - y is a solution
  refine ⟨x - y, sub_ne_zero.mpr hneq, by simp only [mulVec_sub, sub_eq_zero, hfeq], ?_⟩
  -- Inequality
  have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity
  rw [← norm_replicateCol (ι := Unit), norm_le_iff n_mul_norm_A_pow_e_nonneg]
  intro i j
  simp only [replicateCol_apply, Pi.sub_apply]
  rw [Int.norm_eq_abs, ← Int.cast_abs]
  refine le_trans ?_ (Nat.floor_le n_mul_norm_A_pow_e_nonneg)
  norm_cast
  rw [abs_le]
  rw [Finset.mem_Icc] at hxT hyT
  constructor
  · simp only [neg_le_sub_iff_le_add]
    apply le_trans (hyT.2 i)
    norm_cast
    simp only [le_add_iff_nonneg_left]
    exact hxT.1 i
  · simp only [tsub_le_iff_right]
    apply le_trans (hxT.2 i)
    norm_cast
    simp only [le_add_iff_nonneg_right]
    exact hyT.1 i
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * ‖A‖) ^ e
have this : ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
Tactic: have := exists_ne_zero_int_vec_norm_le A hn hm
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
this : ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * ‖A‖) ^ e
have rwa : 1 ≤ ‖A‖
Tactic: rwa [max_eq_right] at this
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
m k : ℕ
h : m ∈ factoredNumbers s
h' : k ∣ m
⊢ k ∈ factoredNumbers s
have h₁ : m ≠ 0
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
m k : ℕ
h : m ∈ factoredNumbers s
h' : k ∣ m
h₁ : m ≠ 0
⊢ k ∈ factoredNumbers s
have h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ k ∈ factoredNumbers s
have hk : k ≠ 0
Tactic: have hk := ne_zero_of_dvd_ne_zero h₁ h'
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
⊢ k ∈ factoredNumbers s
have refine : ∀ (p : ℕ) (hp : p ∈ k.primeFactorsList), p ∈ m.primeFactorsList
Tactic: refine ⟨hk, fun p hp ↦ h₂ p ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : p ∈ k.primeFactorsList
⊢ p ∈ m.primeFactorsList
have rw : ∀ (hp : Prime p ∧ p ∣ k), Prime p ∧ p ∣ m
Tactic: rw [mem_primeFactorsList <| by assumption] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s
have simp_rw : (m ≠ 0 ∧ ∀ (p : ℕ), Prime p ∧ p ∣ m ∧ m ≠ 0 → p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s
Tactic: simp_rw [mem_factoredNumbers, mem_primeFactorsList']
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
have obtain : ∀ (p : ℕ) (hp₁ : 1 + s.sup id ≤ p) (hp₂ : Prime p), m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
Tactic: obtain ⟨p, hp₁, hp₂⟩ := exists_infinite_primes (1 + Finset.sup s id)
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
have rw : (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
Tactic: rw [mem_factoredNumbers_iff_forall_le]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
have refine : ∀ (H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s) (h : m = 0), p < p
Tactic: refine ⟨fun ⟨H₀, H₁⟩ ↦ fun p hp₁ hp₂ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero H₀) hp₂) hp₁ hp₂,
         fun H ↦ ⟨fun h ↦ lt_irrefl p ?_, fun p _ ↦ H p⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
m : ℕ
hm : m ∈ factoredNumbers s
⊢ m.primeFactors ⊆ s
have hm₁ : m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
Tactic: rw [mem_factoredNumbers] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
⊢ factoredNumbers ∅ = {1}
have h : ∀ (m : ℕ), m ∈ factoredNumbers ∅ ↔ Membership.mem (γ := Set ℕ) {1} m
Tactic: ext m
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
⊢ m * n ∈ factoredNumbers s
have hm' : m.primeFactors ⊆ s
Tactic: have hm' := primeFactors_subset_of_mem_factoredNumbers hm
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
hm' : m.primeFactors ⊆ s
⊢ m * n ∈ factoredNumbers s
have hn' : n.primeFactors ⊆ s
Tactic: have hn' := primeFactors_subset_of_mem_factoredNumbers hn
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
n : ℕ
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ∈ factoredNumbers s
have h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
Tactic: have h₀ : (n.primeFactorsList.filter (· ∈ s)).prod ≠ 0 :=
    List.prod_ne_zero fun h ↦ (pos_of_mem_primeFactorsList (List.mem_of_mem_filter h)).false
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ∈ factoredNumbers s
have refine : ∀ (p : ℕ) (hp : p ∈ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList), p ∈ s
Tactic: refine ⟨h₀, fun p hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
⊢ p ∈ s
have H₁ : Prime p
Tactic: obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
H₁ : Prime p
⊢ p ∈ s
have H₂ : p ∣ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) n.primeFactorsList).prod
Tactic: obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
⊢ factoredNumbers (insert N s) = factoredNumbers s
have h : ∀ (m : ℕ), m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s
Tactic: ext m
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
N : ℕ
hN : ¬Prime N
m : ℕ
⊢ m ∈ factoredNumbers (insert N s) ↔ m ∈ factoredNumbers s
have h : ∀ (hm : m ∈ factoredNumbers (insert N s)) (p : ℕ) (hp : p ∈ m.primeFactorsList), p ∈ s
Tactic: refine ⟨fun hm ↦ ⟨hm.1, fun p hp ↦ ?_⟩,
          fun hm ↦ ⟨hm.1, fun p hp ↦ Finset.mem_insert_of_mem <| hm.2 p hp⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : n ∈ (factoredNumbers s)ᶜ \ {0}
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | N ≤ n} n
have hn₁ : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
Tactic: simp only [Set.mem_compl_iff, mem_factoredNumbers, Set.mem_diff, ne_eq, not_and, not_forall,
    exists_prop, Set.mem_singleton_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
⊢ N ≤ n
have obtain : ∀ (p : ℕ) (hp₁ : p ∈ n.primeFactorsList) (hp₂ : p ∉ s), N ≤ n
Tactic: obtain ⟨p, hp₁, hp₂⟩ := hn.1 hn.2
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
⊢ N ≤ p
have contrapose! : ∀ (hp₂ : p < N), p ∈ s
Tactic: contrapose! hp₂
Cleared hypotheses: hp₂
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
⊢ N ≤ n
have this : N ≤ p
Tactic: have : N ≤ p := by
    contrapose! hp₂
    exact h <| mem_primesBelow.mpr ⟨hp₂, prime_of_mem_primeFactorsList hp₁⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
⊢ p ^ e * n ∈ factoredNumbers (insert p s)
have hp' : p ^ e ≠ 0
Tactic: have hp' := pow_ne_zero e hp.ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ factoredNumbers (insert p s)
have refine : ∀ (q : ℕ) (hq : q ∈ (p ^ e * n).primeFactorsList), q ∈ insert p s
Tactic: refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
⊢ q ∈ insert p s
have inl : ∀ (H : q ∈ (p ^ e).primeFactorsList), q ∈ insert p s
Tactic: rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
inl : ∀ (H : q ∈ (p ^ e).primeFactorsList), q ∈ insert p s
⊢ q ∈ insert p s
have inr : ∀ (H : q ∈ n.primeFactorsList), q ∈ insert p s
Tactic: rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ (p ^ e).primeFactorsList
⊢ q ∈ insert p s
have H₁ : Prime q ∧ q ∣ p ^ e
Tactic: rw [mem_primeFactorsList hp'] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q ∈ insert p s
have inl : p ∈ insert p s
Tactic: rw [(prime_dvd_prime_iff_eq H.1 hp).mp <| H.1.dvd_of_dvd_pow H.2]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p.Coprime n
have rw : p ∉ n.primeFactorsList
Tactic: rw [hp.coprime_iff_not_dvd, ← mem_primeFactorsList_iff_dvd hn.1 hp]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ Eq (α := ℕ × (↑(factoredNumbers s) : Type))
    ((fun (x : (↑(factoredNumbers (insert p s)) : Type)) ↦
        (match (motive := (↑(factoredNumbers (insert p s)) : Type) → ℕ × (↑(factoredNumbers s) : Type)) x with
          | ⟨m, property⟩ =>
            ((m.factorization : (a : ℕ) → ℕ) p,
              Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers s)
                (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod ⋯) :
          ℕ × (↑(factoredNumbers s) : Type)))
      ((fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
          (match (motive := ℕ × (↑(factoredNumbers s) : Type) → (↑(factoredNumbers (insert p s)) : Type)) x with
            | (e, n) => Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers (insert p s)) (p ^ e * (↑n : ℕ)) ⋯ :
            (↑(factoredNumbers (insert p s)) : Type)))
        (e, Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers s) m ⋯)))
    (e, Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers s) m ⋯)
have simp : ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e ∧
  (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m
Tactic: simp (etaStruct := .all) only [Prod.mk.injEq, Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e ∧
    (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m
have left : ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
left : ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e
⊢ ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e ∧
    (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m
have right : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ ((p ^ e * m).factorization : (a : ℕ) → ℕ) p = e
have left : ((p ^ e).factorization + m.factorization : (a : ℕ) → ℕ) p = e
Tactic: rw [factorization_mul (pos_iff_ne_zero.mp <| Nat.pow_pos hp.pos) hm₀]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ ((p ^ e).factorization + m.factorization : (a : ℕ) → ℕ) p = e
have left : Eq (α := ℕ) ((m.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: simp only [factorization_pow, Finsupp.coe_add, Finsupp.coe_smul, nsmul_eq_mul,
        Pi.natCast_def, cast_id, Pi.add_apply, Pi.mul_apply, hp.factorization_self,
        mul_one, add_eq_left]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m
have right : (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m.primeFactorsList.prod
Tactic: nth_rewrite 2 [← prod_primeFactorsList hm₀]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m.primeFactorsList.prod
have right : List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) ((p ^ e).primeFactorsList ++ m.primeFactorsList) ~ m.primeFactorsList
Tactic: refine prod_eq <|
        (filter _ <| perm_primeFactorsList_mul (pow_ne_zero e hp.ne_zero) hm₀).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (hypothesis)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
q : ℕ
hq : q ∈ replicate e p
⊢ ¬decide (q ∈ s) = true
have hq₁ : e ≠ 0 ∧ q = p
Tactic: rw [mem_replicate] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) ((p ^ e).primeFactorsList ++ m.primeFactorsList) ~ m.primeFactorsList
have right : List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e).primeFactorsList ++
    List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
  m.primeFactorsList
Tactic: rw [filter_append, hp.primeFactorsList_pow,
          filter_eq_nil_iff.mpr fun q hq ↦ by rw [mem_replicate] at hq; simp [hq.2, hs],
          nil_append, filter_eq_self.mpr fun q hq ↦ by simp only [hm q hq, decide_true]]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
right :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e).primeFactorsList ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
⊢ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) ((p ^ e).primeFactorsList ++ m.primeFactorsList) ~ m.primeFactorsList
have right₁ : List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (replicate e p) ++
    List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
  m.primeFactorsList
Tactic: rw [filter_append, hp.primeFactorsList_pow,
          filter_eq_nil_iff.mpr fun q hq ↦ by rw [mem_replicate] at hq; simp [hq.2, hs],
          nil_append, filter_eq_self.mpr fun q hq ↦ by simp only [hm q hq, decide_true]]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
right :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e).primeFactorsList ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
right₁ :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (replicate e p) ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
⊢ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) ((p ^ e).primeFactorsList ++ m.primeFactorsList) ~ m.primeFactorsList
have right₂ : [] ++ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList
Tactic: rw [filter_append, hp.primeFactorsList_pow,
          filter_eq_nil_iff.mpr fun q hq ↦ by rw [mem_replicate] at hq; simp [hq.2, hs],
          nil_append, filter_eq_self.mpr fun q hq ↦ by simp only [hm q hq, decide_true]]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
right :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e).primeFactorsList ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
right₁ :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (replicate e p) ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
right₂ : [] ++ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList
⊢ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) ((p ^ e).primeFactorsList ++ m.primeFactorsList) ~ m.primeFactorsList
have right₃ : List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList
Tactic: rw [filter_append, hp.primeFactorsList_pow,
          filter_eq_nil_iff.mpr fun q hq ↦ by rw [mem_replicate] at hq; simp [hq.2, hs],
          nil_append, filter_eq_self.mpr fun q hq ↦ by simp only [hm q hq, decide_true]]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
right :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (p ^ e).primeFactorsList ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
right₁ :
  List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) (replicate e p) ++
      List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
right₂ : [] ++ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList
right₃ : List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList
⊢ List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) ((p ^ e).primeFactorsList ++ m.primeFactorsList) ~ m.primeFactorsList
have right₄ : m.primeFactorsList ~ m.primeFactorsList
Tactic: rw [filter_append, hp.primeFactorsList_pow,
          filter_eq_nil_iff.mpr fun q hq ↦ by rw [mem_replicate] at hq; simp [hq.2, hs],
          nil_append, filter_eq_self.mpr fun q hq ↦ by simp only [hm q hq, decide_true]]
-- Lean 4 proof step from Mathlib.NumberTheory.SmoothNumbers (goal)
Goal:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ Eq (α := (↑(factoredNumbers (insert p s)) : Type))
    ((fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
        (match (motive := ℕ × (↑(factoredNumbers s) : Type) → (↑(factoredNumbers (insert p s)) : Type)) x with
          | (e, n) => Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers (insert p s)) (p ^ e * (↑n : ℕ)) ⋯ :
          (↑(factoredNumbers (insert p s)) : Type)))
      ((fun (x : (↑(factoredNumbers (insert p s)) : Type)) ↦
          (match (motive := (↑(factoredNumbers (insert p s)) : Type) → ℕ × (↑(factoredNumbers s) : Type)) x with
            | ⟨m, property⟩ =>
              ((m.factorization : (a : ℕ) → ℕ) p,
                Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers s)
                  (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod ⋯) :
            ℕ × (↑(factoredNumbers s) : Type)))
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers (insert p s)) m ⋯)))
    (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ factoredNumbers (insert p s)) m ⋯)
have simp : HPow.hPow (β := ℕ) p ((m.factorization : (a : ℕ) → ℕ) p : ℕ) *
    (List.filter (fun (x : ℕ) ↦ decide (x ∈ s)) m.primeFactorsList).prod =
  m
Tactic: simp only [Subtype.mk.injEq]