harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/EReal.lean
theorem coe_ennreal_top_mul (x : ℝ≥0) : ((⊤ * x : ℝ≥0∞) : EReal) = ⊤ * x

Proof state:
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑⊤ = ⊤ * ↑↑x

Tactic:
exact Eq.symm <| if_pos <| NNReal.coe_pos.2 h0.bot_lt

Result:
no goals

Proof state:
case inl

⊢ ↑(⊤ * ↑0) = ⊤ * ↑↑0

Tactic:
simp

Result:
no goals

Proof state:
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(⊤ * ↑x) = ⊤ * ↑↑x

Tactic:
rw [ENNReal.top_mul (ENNReal.coe_ne_zero.2 h0)]

Result:
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑⊤ = ⊤ * ↑↑x

Proof state:
x : ℝ≥0
⊢ ↑(⊤ * ↑x) = ⊤ * ↑↑x

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)

Result:
case inl

⊢ ↑(⊤ * ↑0) = ⊤ * ↑↑0

case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(⊤ * ↑x) = ⊤ * ↑↑x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h))

Proof state:
case nil
α : Type u_1
p q : α → Prop
f : ∀ (a : α), p a → q a
H : ∀ (a : α), a ∈ [] → p a
⊢ pmap (fun a h => ⟨a, ⋯⟩) [] H = [].attachWith q ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
p q : α → Prop
f : ∀ (a : α), p a → q a
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap (fun a h => ⟨a, ⋯⟩) l H = l.attachWith q ⋯

Tactic:
induction l with
| nil => rfl
| cons a l ih =>
  simp [pmap, attachWith, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Prop
f : ∀ (a : α), p a → q a
a : α
l : List α
ih : ∀ (H : ∀ (a : α), a ∈ l → p a), pmap (fun a h => ⟨a, ⋯⟩) l H = l.attachWith q ⋯
H : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ pmap (fun a h => ⟨a, ⋯⟩) (a :: l) H = (a :: l).attachWith q ⋯

Tactic:
simp [pmap, attachWith, ih]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem Measurable.prod {f : α → β × γ} (hf₁ : Measurable fun a => (f a).1)
    (hf₂ : Measurable fun a => (f a).2) : Measurable f :=
  Measurable.of_le_map <|
    sup_le
      (by
        rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
        exact hf₁)
      (by
        rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
        exact hf₂)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).1
hf₂ : Measurable fun a => (f a).2
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m

Tactic:
exact hf₂

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).1
hf₂ : Measurable fun a => (f a).2
⊢ MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m

Tactic:
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).1
hf₂ : Measurable fun a => (f a).2
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).1
hf₂ : Measurable fun a => (f a).2
⊢ MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m

Tactic:
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).1
hf₂ : Measurable fun a => (f a).2
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).1
hf₂ : Measurable fun a => (f a).2
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m

Tactic:
exact hf₁

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Algebra.IsAlgebraic.ringHom_of_comp_eq [Algebra.IsAlgebraic R A]
    (hf : Function.Injective f) (hg : Function.Surjective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.IsAlgebraic S B

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring A
inst✝⁷ : Algebra R A
B : Type u_2
inst✝⁶ : Ring B
inst✝⁵ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝⁴ : FunLike FRS R S
inst✝³ : RingHomClass FRS R S
inst✝² : FunLike FAB A B
inst✝¹ : RingHomClass FAB A B
f : FRS
g : FAB
inst✝ : Algebra.IsAlgebraic R A
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
b : B
⊢ IsAlgebraic S b

Tactic:
obtain ⟨a, rfl⟩ := hg b

Result:
case intro
R : Type u
S : Type u_1
A : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring A
inst✝⁷ : Algebra R A
B : Type u_2
inst✝⁶ : Ring B
inst✝⁵ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝⁴ : FunLike FRS R S
inst✝³ : RingHomClass FRS R S
inst✝² : FunLike FAB A B
inst✝¹ : RingHomClass FAB A B
f : FRS
g : FAB
inst✝ : Algebra.IsAlgebraic R A
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
a : A
⊢ IsAlgebraic S (g a)

Proof state:
case intro
R : Type u
S : Type u_1
A : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring A
inst✝⁷ : Algebra R A
B : Type u_2
inst✝⁶ : Ring B
inst✝⁵ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝⁴ : FunLike FRS R S
inst✝³ : RingHomClass FRS R S
inst✝² : FunLike FAB A B
inst✝¹ : RingHomClass FAB A B
f : FRS
g : FAB
inst✝ : Algebra.IsAlgebraic R A
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
a : A
⊢ IsAlgebraic S (g a)

Tactic:
exact (Algebra.IsAlgebraic.isAlgebraic a).ringHom_of_comp_eq f g hf h

Result:
no goals

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring A
inst✝⁷ : Algebra R A
B : Type u_2
inst✝⁶ : Ring B
inst✝⁵ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝⁴ : FunLike FRS R S
inst✝³ : RingHomClass FRS R S
inst✝² : FunLike FAB A B
inst✝¹ : RingHomClass FAB A B
f : FRS
g : FAB
inst✝ : Algebra.IsAlgebraic R A
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.IsAlgebraic S B

Tactic:
refine ⟨fun b ↦ ?_⟩

Result:
R : Type u
S : Type u_1
A : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring A
inst✝⁷ : Algebra R A
B : Type u_2
inst✝⁶ : Ring B
inst✝⁵ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝⁴ : FunLike FRS R S
inst✝³ : RingHomClass FRS R S
inst✝² : FunLike FAB A B
inst✝¹ : RingHomClass FAB A B
f : FRS
g : FAB
inst✝ : Algebra.IsAlgebraic R A
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
b : B
⊢ IsAlgebraic S b
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem Spec_zeroLocus_eq_zeroLocus {R : CommRingCat} (s : Set R) :
    (Spec R).zeroLocus ((Scheme.ΓSpecIso R).inv '' s) = PrimeSpectrum.zeroLocus s

Proof state:
case h
R : CommRingCat
s : Set ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
simp [Spec_carrier, PrimeSpectrum.mem_zeroLocus, Set.subset_def,
  PrimeSpectrum.mem_basicOpen _ x]

Result:
no goals

Proof state:
R : CommRingCat
s : Set ↑R
x : ↑↑(Spec R).toPresheafedSpace
this : (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s
⊢ x ∈ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
simpa

Result:
no goals

Proof state:
case h
R : CommRingCat
s : Set ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ x ∈ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
suffices (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s by simpa

Result:
case h
R : CommRingCat
s : Set ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s

Proof state:
R : CommRingCat
s : Set ↑R
⊢ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) = PrimeSpectrum.zeroLocus s

Tactic:
ext x

Result:
case h
R : CommRingCat
s : Set ↑R
x : ↑↑(Spec R).toPresheafedSpace
⊢ x ∈ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) ↔ x ∈ PrimeSpectrum.zeroLocus s
-- Mathlib/RingTheory/Localization/Defs.lean
theorem map_map {A : Type*} [CommSemiring A] {U : Submonoid A} {W} [CommSemiring W] [Algebra A W]
    [IsLocalization U W] {l : P →+* A} (hl : T ≤ U.comap l) (x : S) :
    map W l hl (map Q g hy x) = map W (l.comp g) (fun _ hx => hl (hy hx)) x

Proof state:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_6
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ (map W l hl) ((map Q g hy) x) = (map W (l.comp g) ⋯) x

Tactic:
rw [← map_comp_map (Q := Q) hy hl]

Result:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_6
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ (map W l hl) ((map Q g hy) x) = ((map W l hl).comp (map Q g hy)) x

Proof state:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_6
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ (map W l hl) ((map Q g hy) x) = ((map W l hl).comp (map Q g hy)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
theorem cocompact_le_atBot_atTop [CompactIccSpace α] :
    cocompact α ≤ atBot ⊔ atTop

Proof state:
case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs.1

Result:
case refine_2.intro
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Proof state:
case refine_2.intro.intro
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ b ≥ u, b ∈ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩

Result:
case refine_2.intro.intro
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ b ≥ u, b ∈ s
x : α
hx : x ∈ (Icc t u)ᶜ
⊢ x ∈ s

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
⊢ cocompact α ≤ atBot ⊔ atTop

Tactic:
refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro

Result:
case refine_1
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : IsEmpty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Proof state:
case refine_2.intro
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2

Result:
case refine_2.intro.intro
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ b ≥ u, b ∈ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Proof state:
case refine_1
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : IsEmpty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ b ≥ u, b ∈ s
x : α
hx : x ∈ (Icc t u)ᶜ
⊢ x ∈ s

Tactic:
exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_le h)) fun h ↦ hu x (le_of_not_le h)

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- If `p` is positive and `n` is `p`-smooth, then every product `p^e * n` is `(p+1)`-smooth. -/
lemma pow_mul_mem_smoothNumbers {p n : ℕ} (hp : p ≠ 0) (e : ℕ) (hn : n ∈ smoothNumbers p) :
    p ^ e * n ∈ smoothNumbers (succ p)

Proof state:
case inl
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ (p ^ e).primeFactorsList
⊢ q < p.succ

Tactic:
rw [mem_primeFactorsList hp'] at H

Result:
case inl
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q < p.succ

Proof state:
case inr
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ n.primeFactorsList
⊢ q < p.succ

Tactic:
exact (hn.2 q H).trans <| lt_succ_self p

Result:
no goals

Proof state:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
⊢ q < p.succ

Tactic:
rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H

Result:
case inl
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ (p ^ e).primeFactorsList
⊢ q < p.succ

case inr
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ n.primeFactorsList
⊢ q < p.succ

Proof state:
case inl
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q < p.succ

Tactic:
exact lt_succ.mpr <| le_of_dvd hp.bot_lt <| H.1.dvd_of_dvd_pow H.2

Result:
no goals

Proof state:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
⊢ p ^ e * n ∈ p.succ.smoothNumbers

Tactic:
have hp' := pow_ne_zero e hp

Result:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ p.succ.smoothNumbers

Proof state:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
⊢ p ^ e * n ∈ p.succ.smoothNumbers

Tactic:
have : NoZeroDivisors ℕ := inferInstance

Result:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
⊢ p ^ e * n ∈ p.succ.smoothNumbers

Proof state:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ p.succ.smoothNumbers

Tactic:
refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩

Result:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
⊢ q < p.succ
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_sub : (p - q).smeval x = p.smeval x - q.smeval x

Proof state:
R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p q : R[X]
x : S
⊢ (p - q).smeval x = p.smeval x - q.smeval x

Tactic:
rw [sub_eq_add_neg, smeval_add, smeval_neg, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem cauchy_map_integralSum_toFilteriUnion (h : Integrable I l f vol) (π₀ : Prepartition I) :
    Cauchy ((l.toFilteriUnion I π₀).map (integralSum f vol))

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Cauchy (Filter.map (integralSum f vol) (toFilteriUnion I π₀))

Tactic:
refine ⟨inferInstance, ?_⟩

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Filter.map (integralSum f vol) (toFilteriUnion I π₀) ×ˢ Filter.map (integralSum f vol) (toFilteriUnion I π₀) ≤ 𝓤 F

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Filter.map (fun p => (integralSum f vol p.1, integralSum f vol p.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 ({π | π.iUnion = π₀.iUnion} ×ˢ {π | π.iUnion = π₀.iUnion})) ≤
    𝓤 F

Tactic:
exact h.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity.mono_left
  (inf_le_inf_left _ <| principal_mono.2 fun π h => h.1.trans h.2.symm)

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Filter.map (integralSum f vol) (toFilteriUnion I π₀) ×ˢ Filter.map (integralSum f vol) (toFilteriUnion I π₀) ≤ 𝓤 F

Tactic:
rw [prod_map_map_eq, ← toFilter_inf_iUnion_eq, ← prod_inf_prod, prod_principal_principal]

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Filter.map (fun p => (integralSum f vol p.1, integralSum f vol p.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 ({π | π.iUnion = π₀.iUnion} ×ˢ {π | π.iUnion = π₀.iUnion})) ≤
    𝓤 F
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem iInf_adj_of_nonempty [Nonempty ι] {f : ι → G.Subgraph} :
    (⨅ i, f i).Adj a b ↔ ∀ i, (f i).Adj a b

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst✝ : Nonempty ι
f : ι → G.Subgraph
⊢ (∀ G' ∈ Set.range fun i => f i, G'.Adj a b) ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
simp

Result:
no goals

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst✝ : Nonempty ι
f : ι → G.Subgraph
⊢ (⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _)]

Result:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst✝ : Nonempty ι
f : ι → G.Subgraph
⊢ (∀ G' ∈ Set.range fun i => f i, G'.Adj a b) ↔ ∀ (i : ι), (f i).Adj a b
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem zeta_sub_one_prime [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) : Prime (hζ.toInteger - 1)

Proof state:
case pos
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p = 2
⊢ Prime (hζ.toInteger - 1)

Tactic:
subst htwo

Result:
case pos
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
hp : Fact (Nat.Prime ↑2)
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
⊢ Prime (hζ.toInteger - 1)

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
⊢ Prime (hζ.toInteger - 1)

Tactic:
by_cases htwo : p = 2

Result:
case pos
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : p = 2
⊢ Prime (hζ.toInteger - 1)

case neg
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ¬p = 2
⊢ Prime (hζ.toInteger - 1)

Proof state:
case pos
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
hp : Fact (Nat.Prime ↑2)
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
⊢ Prime (hζ.toInteger - 1)

Tactic:
apply hζ.zeta_sub_one_prime_of_two_pow

Result:
no goals

Proof state:
case neg
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ¬p = 2
⊢ Prime (hζ.toInteger - 1)

Tactic:
apply hζ.zeta_sub_one_prime_of_ne_two htwo

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem max_add_right {a b : Nat} : max a (a + b) = a + b

Proof state:
a b : Nat
⊢ max a (a + b) = a + b

Tactic:
rw [Nat.max_def]

Result:
a b : Nat
⊢ (if a ≤ a + b then a + b else a) = a + b

Proof state:
a b : Nat
⊢ (if a ≤ a + b then a + b else a) = a + b

Tactic:
simp

Result:
no goals