internlm/Lean-Github huggingface dataset:
Theorem: mapsTo_rectangle_left_re
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.im, w.im]]
⊢ (fun y => ↑z.re + ↑y * I) x✝ ∈ re ⁻¹' [[z.re, w.re]]
Tactic:
simp
Proof state after:
no goals
Theorem: mapsTo_rectangle_left_re
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.im, w.im]]
⊢ (fun y => ↑z.re + ↑y * I) x✝ ∈ im ⁻¹' [[z.im, w.im]]
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: mapsTo_rectangle_right_re
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.im, w.im]]
⊢ (fun y => ↑w.re + ↑y * I) x✝ ∈ re ⁻¹' [[z.re, w.re]]
Tactic:
simp
Proof state after:
no goals
Theorem: mapsTo_rectangle_right_re
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.im, w.im]]
⊢ (fun y => ↑w.re + ↑y * I) x✝ ∈ im ⁻¹' [[z.im, w.im]]
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: mapsTo_rectangle_left_im
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.re, w.re]]
⊢ (fun x => ↑x + ↑z.im * I) x✝ ∈ re ⁻¹' [[z.re, w.re]]
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: mapsTo_rectangle_left_im
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.re, w.re]]
⊢ (fun x => ↑x + ↑z.im * I) x✝ ∈ im ⁻¹' [[z.im, w.im]]
Tactic:
simp
Proof state after:
no goals
Theorem: mapsTo_rectangle_right_im
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.re, w.re]]
⊢ (fun x => ↑x + ↑w.im * I) x✝ ∈ re ⁻¹' [[z.re, w.re]]
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: mapsTo_rectangle_right_im
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
x✝ : ℝ
hx : x✝ ∈ [[z.re, w.re]]
⊢ (fun x => ↑x + ↑w.im * I) x✝ ∈ im ⁻¹' [[z.im, w.im]]
Tactic:
simp
Proof state after:
no goals
Theorem: mapsTo_rectangleBorder_left_re
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w x✝ : ℂ
⊢ x✝ ∈ (fun y => ↑z.re + ↑y * I) '' [[z.im, w.im]] → x✝ ∈ RectangleBorder z w
Tactic:
simp_all [verticalSegment_eq, RectangleBorder]
Proof state after:
no goals
Theorem: mapsTo_rectangleBorder_right_re
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w x✝ : ℂ
⊢ x✝ ∈ (fun y => ↑w.re + ↑y * I) '' [[z.im, w.im]] → x✝ ∈ RectangleBorder z w
Tactic:
simp_all [verticalSegment_eq, RectangleBorder]
Proof state after:
no goals
Theorem: mapsTo_rectangleBorder_left_im
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w x✝ : ℂ
⊢ x✝ ∈ (fun x => ↑x + ↑z.im * I) '' [[z.re, w.re]] → x✝ ∈ RectangleBorder z w
Tactic:
simp_all [horizontalSegment_eq, RectangleBorder]
Proof state after:
no goals
Theorem: mapsTo_rectangleBorder_right_im
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w x✝ : ℂ
⊢ x✝ ∈ (fun x => ↑x + ↑w.im * I) '' [[z.re, w.re]] → x✝ ∈ RectangleBorder z w
Tactic:
simp_all [horizontalSegment_eq, RectangleBorder]
Proof state after:
no goals
Theorem: mapsTo_rectangle_left_re_NoP
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ MapsTo (fun y => ↑z.re + ↑y * I) [[z.im, w.im]] (Rectangle z w \ {p})
Tactic:
refine (mapsTo_rectangleBorder_left_re z w).mono_right (Set.subset_diff.mpr ?_)
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Theorem: mapsTo_rectangle_left_re_NoP
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Tactic:
exact ⟨rectangleBorder_subset_rectangle z w, disjoint_singleton_right.mpr pNotOnBorder⟩
Proof state after:
no goals
Theorem: mapsTo_rectangle_right_re_NoP
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ MapsTo (fun y => ↑w.re + ↑y * I) [[z.im, w.im]] (Rectangle z w \ {p})
Tactic:
refine (mapsTo_rectangleBorder_right_re z w).mono_right (Set.subset_diff.mpr ?_)
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Theorem: mapsTo_rectangle_right_re_NoP
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Tactic:
exact ⟨rectangleBorder_subset_rectangle z w, disjoint_singleton_right.mpr pNotOnBorder⟩
Proof state after:
no goals
Theorem: mapsTo_rectangle_left_im_NoP
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ MapsTo (fun x => ↑x + ↑z.im * I) [[z.re, w.re]] (Rectangle z w \ {p})
Tactic:
refine (mapsTo_rectangleBorder_left_im z w).mono_right (Set.subset_diff.mpr ?_)
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Theorem: mapsTo_rectangle_left_im_NoP
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Tactic:
exact ⟨rectangleBorder_subset_rectangle z w, disjoint_singleton_right.mpr pNotOnBorder⟩
Proof state after:
no goals
Theorem: mapsTo_rectangle_right_im_NoP
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ MapsTo (fun x => ↑x + ↑w.im * I) [[z.re, w.re]] (Rectangle z w \ {p})
Tactic:
refine (mapsTo_rectangleBorder_right_im z w).mono_right (Set.subset_diff.mpr ?_)
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Theorem: mapsTo_rectangle_right_im_NoP
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Tactic:
exact ⟨rectangleBorder_subset_rectangle z w, disjoint_singleton_right.mpr pNotOnBorder⟩
Proof state after:
no goals
Theorem: not_mem_rectangleBorder_of_rectangle_mem_nhds
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
⊢ p ∉ RectangleBorder z w
Tactic:
refine Set.disjoint_right.mp (rectangleBorder_disjoint_singleton ?_) rfl
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
⊢ p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
Theorem: not_mem_rectangleBorder_of_rectangle_mem_nhds
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
⊢ p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
Tactic:
have h1 := rectangle_mem_nhds_iff.mp hp
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
h1 : p ∈ uIoo z.re w.re ×ℂ uIoo z.im w.im
⊢ p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
Theorem: not_mem_rectangleBorder_of_rectangle_mem_nhds
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
hp : Rectangle z w ∈ 𝓝 p
h1 : p ∈ uIoo z.re w.re ×ℂ uIoo z.im w.im
⊢ p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
Tactic:
exact ⟨Set.ne_left_of_mem_uIoo h1.1, Set.ne_right_of_mem_uIoo h1.1,
  Set.ne_left_of_mem_uIoo h1.2, Set.ne_right_of_mem_uIoo h1.2⟩
Proof state after:
no goals
Theorem: Complex.nhds_hasBasis_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p).HasBasis (fun x => 0 < x) fun x => Square p x
Tactic:
suffices (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (0 < .) (equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p .)
  by simpa only [← nhds_prod_eq, Homeomorph.map_nhds_eq, Homeomorph.image_preimage]
    using this.map equivRealProdCLM.symm.toHomeomorph
Proof state after:
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (fun x => 0 < x) fun x => ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p x
Theorem: Complex.nhds_hasBasis_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
⊢ (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (fun x => 0 < x) fun x => ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p x
Tactic:
apply ((nhds_basis_Icc_pos p.re).prod_same_index_mono (nhds_basis_Icc_pos p.im) ?_ ?_).congr
Proof state after:
case hp
z w : ℂ
c : ℝ
p : ℂ
⊢ ∀ (i : ℝ), 0 < i ↔ 0 < i

case hs
z w : ℂ
c : ℝ
p : ℂ
⊢ ∀ (i : ℝ),
    0 < i → Icc (p.re - i) (p.re + i) ×ˢ Icc (p.im - i) (p.im + i) = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i

z w : ℂ
c : ℝ
p : ℂ
⊢ MonotoneOn (fun ε => Icc (p.re - ε) (p.re + ε)) {i | 0 < i}

z w : ℂ
c : ℝ
p : ℂ
⊢ MonotoneOn (fun ε => Icc (p.im - ε) (p.im + ε)) {i | 0 < i}
Theorem: Complex.nhds_hasBasis_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
⊢ MonotoneOn (fun ε => Icc (p.re - ε) (p.re + ε)) {i | 0 < i}

z w : ℂ
c : ℝ
p : ℂ
⊢ MonotoneOn (fun ε => Icc (p.im - ε) (p.im + ε)) {i | 0 < i}
Tactic:
all_goals exact (antitone_const_tsub.Icc (monotone_id.const_add _)).monotoneOn _
Proof state after:
no goals
Theorem: Complex.nhds_hasBasis_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
this : (𝓝 p.re ×ˢ 𝓝 p.im).HasBasis (fun x => 0 < x) fun x => ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p x
⊢ (𝓝 p).HasBasis (fun x => 0 < x) fun x => Square p x
Tactic:
simpa only [← nhds_prod_eq, Homeomorph.map_nhds_eq, Homeomorph.image_preimage]
using this.map equivRealProdCLM.symm.toHomeomorph
Proof state after:
no goals
Theorem: Complex.nhds_hasBasis_square
Proof state before:
case hp
z w : ℂ
c : ℝ
p : ℂ
⊢ ∀ (i : ℝ), 0 < i ↔ 0 < i
Tactic:
intro
Proof state after:
case hp
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
⊢ 0 < i✝ ↔ 0 < i✝
Theorem: Complex.nhds_hasBasis_square
Proof state before:
case hp
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
⊢ 0 < i✝ ↔ 0 < i✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Complex.nhds_hasBasis_square
Proof state before:
case hs
z w : ℂ
c : ℝ
p : ℂ
⊢ ∀ (i : ℝ),
    0 < i → Icc (p.re - i) (p.re + i) ×ˢ Icc (p.im - i) (p.im + i) = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i
Tactic:
intros
Proof state after:
case hs
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ Icc (p.re - i✝) (p.re + i✝) ×ˢ Icc (p.im - i✝) (p.im + i✝) = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i✝
Theorem: Complex.nhds_hasBasis_square
Proof state before:
case hs
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ Icc (p.re - i✝) (p.re + i✝) ×ˢ Icc (p.im - i✝) (p.im + i✝) = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i✝
Tactic:
rw [← uIcc_of_lt (by linarith), ← uIcc_of_lt (by linarith)]
Proof state after:
case hs
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ [[p.re - i✝, p.re + i✝]] ×ˢ [[p.im - i✝, p.im + i✝]] = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i✝
Theorem: Complex.nhds_hasBasis_square
Proof state before:
case hs
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ [[p.re - i✝, p.re + i✝]] ×ˢ [[p.im - i✝, p.im + i✝]] = ⇑equivRealProdCLM.symm.toHomeomorph ⁻¹' Square p i✝
Tactic:
simpa [Square, Rectangle] using by ring_nf
Proof state after:
no goals
Theorem: Complex.nhds_hasBasis_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ p.re - i✝ < p.re + i✝
Tactic:
linarith
Proof state after:
no goals
Theorem: Complex.nhds_hasBasis_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ p.im - i✝ < p.im + i✝
Tactic:
linarith
Proof state after:
no goals
Theorem: Complex.nhds_hasBasis_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
i✝ : ℝ
a✝ : 0 < i✝
⊢ [[(p.re - i✝, p.im - i✝), (p.re + i✝, p.im + i✝)]] = [[(-i✝ + p.re, -i✝ + p.im), (i✝ + p.re, i✝ + p.im)]]
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Complex.nhds_hasBasis_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
⊢ MonotoneOn (fun ε => Icc (p.im - ε) (p.im + ε)) {i | 0 < i}
Tactic:
exact (antitone_const_tsub.Icc (monotone_id.const_add _)).monotoneOn _
Proof state after:
no goals
Theorem: square_mem_nhds
Proof state before:
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
⊢ Square p c ∈ 𝓝 p
Tactic:
wlog hc_pos : 0 < c generalizing c with h
Proof state after:
case inr
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
h : ∀ {c : ℝ}, c ≠ 0 → 0 < c → Square p c ∈ 𝓝 p
hc_pos : ¬0 < c
⊢ Square p c ∈ 𝓝 p

z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
hc_pos : 0 < c
⊢ Square p c ∈ 𝓝 p
Theorem: square_mem_nhds
Proof state before:
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
hc_pos : 0 < c
⊢ Square p c ∈ 𝓝 p
Tactic:
exact (nhds_hasBasis_square p).mem_of_mem hc_pos
Proof state after:
no goals
Theorem: square_mem_nhds
Proof state before:
case inr
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
h : ∀ {c : ℝ}, c ≠ 0 → 0 < c → Square p c ∈ 𝓝 p
hc_pos : ¬0 < c
⊢ Square p c ∈ 𝓝 p
Tactic:
rw [← square_neg]
Proof state after:
case inr
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
h : ∀ {c : ℝ}, c ≠ 0 → 0 < c → Square p c ∈ 𝓝 p
hc_pos : ¬0 < c
⊢ Square p (-c) ∈ 𝓝 p
Theorem: square_mem_nhds
Proof state before:
case inr
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
hc : c ≠ 0
h : ∀ {c : ℝ}, c ≠ 0 → 0 < c → Square p c ∈ 𝓝 p
hc_pos : ¬0 < c
⊢ Square p (-c) ∈ 𝓝 p
Tactic:
exact h (neg_ne_zero.mpr hc) <| neg_pos.mpr <| hc.lt_of_le <| not_lt.mp hc_pos
Proof state after:
no goals
Theorem: square_subset_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
c₁ c₂ : ℝ
hc₁ : 0 < c₁
hc : c₁ ≤ c₂
⊢ Square p c₁ ⊆ Square p c₂
Tactic:
apply RectSubRect' <;> simpa using by linarith
Proof state after:
no goals
Theorem: square_subset_square
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
c₁ c₂ : ℝ
hc₁ : 0 < c₁
hc : c₁ ≤ c₂
⊢ c₁ ≤ c₂
Tactic:
linarith
Proof state after:
no goals
Theorem: SmallSquareInRectangle
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, Square p c ⊆ Rectangle z w
Tactic:
obtain ⟨ε, hε0, hε⟩ := ((Complex.nhds_hasBasis_square p).1 _).mp pInRectInterior
Proof state after:
case intro.intro
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, Square p c ⊆ Rectangle z w
Theorem: SmallSquareInRectangle
Proof state before:
case intro.intro
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, Square p c ⊆ Rectangle z w
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' (hε0)] with _ ⟨hε'0, hε'⟩
Proof state after:
case h
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
a✝ : ℝ
hε'0 : 0 < a✝
hε' : a✝ < ε
⊢ Square p a✝ ⊆ Rectangle z w
Theorem: SmallSquareInRectangle
Proof state before:
case h
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
a✝ : ℝ
hε'0 : 0 < a✝
hε' : a✝ < ε
⊢ Square p a✝ ⊆ Rectangle z w
Tactic:
exact subset_trans (square_subset_square hε'0 hε'.le) hε
Proof state after:
no goals
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
⊢ Squarefree (∏ p ∈ s, p)
Tactic:
refine Iff.mpr Nat.squarefree_iff_prime_squarefree ?_
Proof state after:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
⊢ ∀ (x : ℕ), x.Prime → ¬x * x ∣ ∏ p ∈ s, p
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
⊢ ∀ (x : ℕ), x.Prime → ¬x * x ∣ ∏ p ∈ s, p
Tactic:
intro p hp
Proof state after:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
⊢ ¬p * p ∣ ∏ p ∈ s, p
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
⊢ ¬p * p ∣ ∏ p ∈ s, p
Tactic:
by_contra h_dvd
Proof state after:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
⊢ False
Tactic:
by_cases hps : p ∈ s
Proof state after:
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∈ s
⊢ False

case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∈ s
⊢ False
Tactic:
rw [←Finset.mul_prod_erase (a:=p) (h := hps), mul_dvd_mul_iff_left (Nat.Prime.ne_zero hp)] at h_dvd
Proof state after:
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
⊢ False
Tactic:
cases' Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h_dvd with q hq
Proof state after:
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : q ∈ s.erase p ∧ p ∣ q
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : q ∈ s.erase p ∧ p ∣ q
⊢ False
Tactic:
rw [Finset.mem_erase] at hq
Proof state after:
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : (q ≠ p ∧ q ∈ s) ∧ p ∣ q
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : (q ≠ p ∧ q ∈ s) ∧ p ∣ q
⊢ False
Tactic:
exact hq.1.1 $ symm $ (Nat.prime_dvd_prime_iff_eq hp (h q hq.1.2)).mp hq.2
Proof state after:
no goals
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
⊢ False
Tactic:
have : p ∣ ∏ p in s, p := Trans.trans (dvd_mul_right p p) h_dvd
Proof state after:
case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
⊢ False
Tactic:
cases' Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) this with q hq
Proof state after:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ False
Tactic:
have heq : p = q := by
  rw [←Nat.prime_dvd_prime_iff_eq hp (h q hq.1)]
  exact hq.2
Proof state after:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False
Tactic:
rw [heq] at hps
Proof state after:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
this : p ∣ ∏ p ∈ s, p
q : ℕ
hps : q ∉ s
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
this : p ∣ ∏ p ∈ s, p
q : ℕ
hps : q ∉ s
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False
Tactic:
exact hps hq.1
Proof state after:
no goals
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ p = q
Tactic:
rw [←Nat.prime_dvd_prime_iff_eq hp (h q hq.1)]
Proof state after:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ p ∣ q
Theorem: Sieve.prodDistinctPrimes_squarefree
Proof state before:
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ p ∣ q
Tactic:
exact hq.2
Proof state after:
no goals
Theorem: Sieve.primorial_squarefree
Proof state before:
n : ℕ
⊢ Squarefree (primorial n)
Tactic:
apply prodDistinctPrimes_squarefree
Proof state after:
case h
n : ℕ
⊢ ∀ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p.Prime
Theorem: Sieve.primorial_squarefree
Proof state before:
case h
n : ℕ
⊢ ∀ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p.Prime
Tactic:
simp_rw [Finset.mem_filter]
Proof state after:
case h
n : ℕ
⊢ ∀ (p : ℕ), p ∈ Finset.range (n + 1) ∧ p.Prime → p.Prime
Theorem: Sieve.primorial_squarefree
Proof state before:
case h
n : ℕ
⊢ ∀ (p : ℕ), p ∈ Finset.range (n + 1) ∧ p.Prime → p.Prime
Tactic:
exact fun _ h => h.2
Proof state after:
no goals
Theorem: Sieve.zeta_pos_of_prime
Proof state before:
⊢ ∀ (p : ℕ), p.Prime → 0 < ↑ζ p
Tactic:
intro p hp
Proof state after:
p : ℕ
hp : p.Prime
⊢ 0 < ↑ζ p
Theorem: Sieve.zeta_pos_of_prime
Proof state before:
p : ℕ
hp : p.Prime
⊢ 0 < ↑ζ p
Tactic:
rw [ArithmeticFunction.natCoe_apply, ArithmeticFunction.zeta_apply, if_neg (Nat.Prime.ne_zero hp)]
Proof state after:
p : ℕ
hp : p.Prime
⊢ 0 < ↑1
Theorem: Sieve.zeta_pos_of_prime
Proof state before:
p : ℕ
hp : p.Prime
⊢ 0 < ↑1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Sieve.zeta_lt_self_of_prime
Proof state before:
⊢ ∀ (p : ℕ), p.Prime → ↑ζ p < ↑p
Tactic:
intro p hp
Proof state after:
p : ℕ
hp : p.Prime
⊢ ↑ζ p < ↑p
Theorem: Sieve.zeta_lt_self_of_prime
Proof state before:
p : ℕ
hp : p.Prime
⊢ ↑ζ p < ↑p
Tactic:
rw [ArithmeticFunction.natCoe_apply, ArithmeticFunction.zeta_apply, if_neg (Nat.Prime.ne_zero hp)]
Proof state after:
p : ℕ
hp : p.Prime
⊢ ↑1 < ↑p
Theorem: Sieve.zeta_lt_self_of_prime
Proof state before:
p : ℕ
hp : p.Prime
⊢ ↑1 < ↑p
Tactic:
norm_num
Proof state after:
p : ℕ
hp : p.Prime
⊢ 1 < p
Theorem: Sieve.zeta_lt_self_of_prime
Proof state before:
p : ℕ
hp : p.Prime
⊢ 1 < p
Tactic:
exact Nat.succ_le.mp (Nat.Prime.two_le hp)
Proof state after:
no goals
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
n p : ℕ
hp : p.Prime
⊢ p ∣ primorial n ↔ p ≤ n
Tactic:
unfold primorial
Proof state after:
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ↔ p ≤ n
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ↔ p ≤ n
Tactic:
constructor
Proof state after:
case mp
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p → p ≤ n

case mpr
n p : ℕ
hp : p.Prime
⊢ p ≤ n → p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mp
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p → p ≤ n
Tactic:
intro h
Proof state after:
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
⊢ p ≤ n
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
⊢ p ≤ n
Tactic:
let h' : ∃ i, i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)) ∧ p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
Proof state after:
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
⊢ p ≤ n
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
⊢ p ≤ n
Tactic:
cases' h' with q hq
Proof state after:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : q ∈ Finset.filter Nat.Prime (Finset.range (n + 1)) ∧ p ∣ q
⊢ p ≤ n
Theorem: Sieve.prime_dvd_primorial_iff
Proof state before:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : q ∈ Finset.filter Nat.Prime (Finset.range (n + 1)) ∧ p ∣ q
⊢ p ≤ n
Tactic:
rw [Finset.mem_filter, Finset.mem_range] at hq
Proof state after:
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p ∣ q
⊢ p ≤ n