mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this✝ : Measurable ↑expMapBasis
x : realSpace K
this : 0 ≤ (∏ w, ↑expMapBasis x ↑w)⁻¹
⊢ ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (ENNReal.ofReal (∏ i, ↑expMapBasis x ↑i))⁻¹ *
            2⁻¹ ^ nrComplexPlaces K *
          ↑(finrank ℚ K) *
        ENNReal.ofReal (regulator K) *
      f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      (ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
        f (↑expMapBasis x))

Tactic:
ofReal_prod_of_nonneg (fun _ _ ↦ (expMapBasis_pos _ _).le)

Goal state after:
case e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this✝ : Measurable ↑expMapBasis
x : realSpace K
this : 0 ≤ (∏ w, ↑expMapBasis x ↑w)⁻¹
⊢ ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis x ↑i))⁻¹ *
            2⁻¹ ^ nrComplexPlaces K *
          ↑(finrank ℚ K) *
        ENNReal.ofReal (regulator K) *
      f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      (ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
        f (↑expMapBasis x))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
inst✝ : NeZero p
η : K
hη : IsPrimitiveRoot η p
i : ℕ
hi : i.Coprime p
hζη : ζ ^ i = η
⊢ Associated (hζ.toInteger - 1) (hη.toInteger - 1)

Tactic:
rw [show hη.toInteger = hζ.toInteger ^ i from RingOfIntegers.ext hζη.symm]

Goal state after:
p : ℕ
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
inst✝ : NeZero p
η : K
hη : IsPrimitiveRoot η p
i : ℕ
hi : i.Coprime p
hζη : ζ ^ i = η
⊢ Associated (hζ.toInteger - 1) (hζ.toInteger ^ i - 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left✝ : P.IsPrime
right✝ : P.LiesOver 𝒑
⊢ 𝒑.ramificationIdxIn (𝓞 K) = 1

Tactic:
rw [ramificationIdxIn_eq_ramificationIdx 𝒑 P Gal(K/ℚ), ramificationIdx_eq_of_not_dvd p K P hm]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
⊢ 0 = (a *ᵥ ξ K x) k

Tactic:
have lin_0 : ∀ u, ∑ r, ∑ l, (a' K a k l r u * x (l, r) : 𝓞 K) = 0 := by
    intro u
    have hξ := ξ_ne_0 K x hxl
    rw [Ne, funext_iff, not_forall] at hξ
    rcases hξ with ⟨l, hξ⟩
    rw [funext_iff] at hmulvec0
    specialize hmulvec0 ⟨k, u⟩
    simp only [Fintype.sum_prod_type, mulVec, dotProduct, asiegel] at hmulvec0
    rw [sum_comm] at hmulvec0
    exact mod_cast hmulvec0

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
⊢ 0 = (a *ᵥ ξ K x) k
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hpq : q ≠ p
⊢ q = 1

Tactic:
rw [ne_comm, ← Nat.coprime_primes hp hq.elim, hp.coprime_iff_not_dvd] at hpq

Goal state after:
case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hpq : ¬p ∣ q
⊢ q = 1
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
x✝¹ : ℕ × ℕ
i a : ℕ
x✝ : (i, a) ∈ L.zipIdx
⊢ ↑n₀ * f ↑n₀ ^ (i, a).2 ≤ ↑n₀

Tactic:
exact mul_le_of_le_one_right (by positivity) (pow_le_one₀ (by positivity) h)

Goal state after:
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k ↦ ↑(k.choose j)) 0 • a j = a n

Tactic:
by
    simp only [fwdDiff_iter_choose_zero, ite_smul, one_smul, zero_smul, sum_ite_eq,
      Finset.mem_range, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte]

Goal state after:
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
a✝ : E
n : ℕ
x : ℤ_[p]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
f g : C(ℤ_[p], E)
⊢ { toFun := fun x ↦ Δ_[1]^[x] (⇑(f + g)) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ } =
    { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ } +
      { toFun := fun x ↦ Δ_[1]^[x] (⇑g) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ }

Tactic:
by
    ext x
    simp only [ContinuousMap.coe_add, fwdDiff_iter_add, Pi.add_apply,
      ZeroAtInftyContinuousMap.coe_mk, ZeroAtInftyContinuousMap.coe_add]

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ z' = a

Tactic:
by
  let h := z' - a
  let ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion a h
  simp only [Polynomial.eval_map_algebraMap, Polynomial.derivative_map] at hq
  have : (F.derivative.aeval a + q * h) * h = 0 := by calc
    _ = F.aeval (a + h) := by rw [hq, ha, zero_add, sq, right_distrib, mul_assoc]
    _ = _ := show F.aeval (a + (z' - a)) = 0 by simp [hz']
  have : h = 0 := by_contra fun hne ↦
    have : F.derivative.aeval a + q * h = 0 :=
      (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne
    have : F.derivative.aeval a = -q * h := by simpa using eq_neg_of_add_eq_zero_left this
    lt_irrefl ‖F.derivative.aeval a‖
      (calc
        ‖F.derivative.aeval a‖ = ‖q‖ * ‖h‖ := by simp [this]
        _ ≤ 1 * ‖h‖ := by gcongr; apply PadicInt.norm_le_one
        _ < ‖F.derivative.aeval a‖ := by simpa)
  exact eq_of_sub_eq_zero (by rw [← this])

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖z' - z‖ = ‖z1‖

Tactic:
simp only [sub_eq_add_neg, add_assoc, hz', add_add_neg_cancel'_right, norm_neg]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
⊢ ∃ a, IsFundamental a

Tactic:
let x₁ := Nat.find P
  obtain ⟨hx, y₁, hy₀, hy₁⟩ := Nat.find_spec P
  refine ⟨mk x₁ y₁ hy₁, by rw [x_mk]; exact mod_cast hx, hy₀, fun {b} hb => ?_⟩
  rw [x_mk]
  have hb' := (Int.toNat_of_nonneg <| zero_le_one.trans hb.le).symm
  have hb'' := hb
  rw [hb'] at hb ⊢
  norm_cast at hb ⊢
  refine Nat.find_min' P ⟨hb, |b.y|, abs_pos.mpr <| y_ne_zero_of_one_lt_x hb'', ?_⟩
  rw [← hb', sq_abs]
  exact b.prop

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * (T_gen p F a ^ 2 ^ n) ^ 2 =
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ (n + 1)

Tactic:
← pow_mul,

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ (2 ^ n * 2) =
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ (n + 1)
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n k : ℕ
hnk : n ≤ k
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Tactic:
by
  have hex : ∃ m, k = n + m := Nat.exists_eq_add_of_le hnk
  let ⟨_, hex'⟩ := hex
  rw [hex']; apply newton_seq_dist_aux

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
m : ℤ
h₂ : beattySeq' s m = j
⊢ False

Tactic:
beattySeq,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ⌊↑k * r⌋ = j
m : ℤ
h₂ : beattySeq' s m = j
⊢ False
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : (r⁻¹ + s⁻¹) * ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < (r⁻¹ + s⁻¹) * (↑j + 1)
⊢ False

Tactic:
hrs.inv_add_inv_eq_one,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : 1 * ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < 1 * (↑j + 1)
⊢ False
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : ↑k < ↑j / r
h₁₂ : (↑j + 1) / r ≤ ↑k + 1
h₂₁ : ↑m ≤ ↑j / s
h₂₂ : (↑j + 1) / s < ↑m + 1
h₃ : ↑k + ↑m < (r⁻¹ + s⁻¹) * ↑j
h₄ : (r⁻¹ + s⁻¹) * (↑j + 1) < ↑k + 1 + (↑m + 1)
⊢ False

Tactic:
hrs.inv_add_inv_eq_one,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : ↑k < ↑j / r
h₁₂ : (↑j + 1) / r ≤ ↑k + 1
h₂₁ : ↑m ≤ ↑j / s
h₂₂ : (↑j + 1) / s < ↑m + 1
h₃ : ↑k + ↑m < 1 * ↑j
h₄ : 1 * (↑j + 1) < ↑k + 1 + (↑m + 1)
⊢ False
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ beattySeq r (⌈(↑j + 1) / r⌉ - 1) = j

Tactic:
beattySeq,

Goal state after:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ ⌊↑(⌈(↑j + 1) / r⌉ - 1) * r⌋ = j
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case a.inl
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ 0 < beattySeq r k

Tactic:
beattySeq,

Goal state after:
case a.inl
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ 0 < ⌊↑k * r⌋
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq s✝ k = x}
k : ℤ
hj : 0 < beattySeq s✝ k
hk : beattySeq s✝ k = j
⊢ k > 0

Tactic:
beattySeq,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq s✝ k = x}
k : ℤ
hj : 0 < ⌊↑k * s✝⌋
hk : beattySeq s✝ k = j
⊢ k > 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ s.nu d ≠ 0

Tactic:
by
  apply _root_.ne_of_gt
  exact nu_pos_of_dvd_prodPrimes hd

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d =
    ∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0

Tactic:
simp_rw [mul_sum, ← sum_filter]
    congr with n
    congr
    · rw [← divisors_filter_dvd_of_dvd prodPrimes_ne_zero (Nat.gcd_dvd_left _ _)]
      ext x; simp +contextual [dvd_gcd_iff]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d =
    s.totalMass * mainSum muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem d

Tactic:
mainSum,

Goal state after:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d =
    s.totalMass * ∑ d ∈ (prodPrimes ?m.65).divisors, muPlus d * (nu ?m.65) d +
      ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem d

s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ BoundingSieve
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
⊢ IsCoprime x n

Tactic:
have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
    rw [show y ^ 2 = n + -1 * x ^ 2 by lia] at hc2
    exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / (m ^ n !) ^ n

Tactic:
← pow_mul,

Goal state after:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / m ^ (n ! * n)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ e • Module.rank (R ⧸ p) (S ⧸ P) = ↑e * Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
nsmul_eq_mul

Goal state after:
case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ ↑e * Module.rank (R ⧸ p) (S ⧸ P) = ↑e * Module.rank (R ⧸ p) (S ⧸ P)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
hr : r ∈ f.aroots ℂ
⊢ ‖↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
        else 0) ^
        p /
      ↑(p - 1)!

Tactic:
nsmul_eq_mul

Goal state after:
case h.right.refine_2
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
⊢ ‖↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
        else 0) ^
        p /
      ↑(p - 1)!
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - ↑a < 1 ∧ ↑a - x * ↑b < 1
⊢ a ∈ Finset.Icc 0 ↑b

Tactic:
sub_lt_iff_lt_add,

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b < 1 + ↑a ∧ ↑a - x * ↑b < 1
⊢ a ∈ Finset.Icc 0 ↑b
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b < 1 + ↑a ∧ ↑a - x * ↑b < 1
⊢ a ∈ Finset.Icc 0 ↑b

Tactic:
sub_lt_iff_lt_add,

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b < 1 + ↑a ∧ ↑a < 1 + x * ↑b
⊢ a ∈ Finset.Icc 0 ↑b
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r * (↑r)⁻¹ = ↑1

Tactic:
mul_inv_cancel₀

Goal state after:
case inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ 1 = ↑1

case inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r ≠ 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
hx : Liouville x
n : ℕ
H : ∃ a, ∀ (b : ℕ), a ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
⊢ False

Tactic:
rcases H with ⟨N, hN⟩

Goal state after:
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
⊢ False
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ IsCompl a b ↔ IsCompl ↑a ↑b

Tactic:
rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
⊢ ∀ t ⊆ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a},
    t.Nonempty →
      t.Countable → ∀ (x : α), IsLUB t x → x ∈ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}

Tactic:
intro A hA hA_ne hAc x hx

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA : A ⊆ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
⊢ x ∈ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋₊

Tactic:
simp [floor_lt ha]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ

Tactic:
obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : ↑(Icc 0 n)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x : X
⊢ x ∈ range ⇑n → n x = x

Tactic:
by rintro ⟨x, rfl⟩; exact idempotent _

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
P : Partition ⊥
x : α
⊢ x ∉ P

Tactic:
rintro hxP
  obtain rfl := le_bot_iff.mp <| P.le_of_mem hxP
  exact P.bot_notMem hxP

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ f a b ≤ ⨅ x ∈ X, f x b

Tactic:
· simp only [le_iInf_iff]
      intro x hx
      exact h x hx b hb

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥

Tactic:
have : Order.pred^[0] r = ⊥ := by
      rw [← h]
      apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

Goal state after:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
this : Order.pred^[0] r = ⊥
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
this : Order.pred^[0] r = ⊥
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥

Tactic:
simp only [Function.iterate_zero, id_eq] at this

Goal state after:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
this : r = ⊥
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥