mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (b : ℕ) (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

pp: case h₂
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
⊢ Summable fun c ↦ (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

Tactic:
case h₂ =>
    simpa using ((summable_norm_eisSummand hk2 z).subtype _).of_norm.mul_left (a := ((b : ℂ) ^ k)⁻¹)

Goal state after:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (b : ℕ) (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n ↦ cexp (↑π * I * ↑(n + 1) ^ 2 * τ) + cexp (↑π * I * ↑(n + 1) ^ 2 * τ))
    (jacobiTheta τ + cexp 0 - (cexp 0 + cexp 0))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
← mul_two,

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n ↦ cexp (↑π * I * ↑(n + 1) ^ 2 * τ) * 2) (jacobiTheta τ + cexp 0 - cexp 0 * 2)
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
s : HasSum (fun n ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
aux : Summable fun n ↦ ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

Tactic:
exact (norm_tsum_le_tsum_norm aux).trans ((aux.tsum_mono s.summable this).trans_eq s.tsum_eq)

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : ModularFormClass F 𝒢 k
c✝ : OnePoint ℝ
h : IsCusp c✝ ℋ
γ : GL (Fin 2) ℝ
⊢ γ • OnePoint.infty = c✝ → IsBoundedAtImInfty ((SlashInvariantForm.trace ℋ f).toFun ∣[k] γ)

Tactic:
by
    rintro rfl
    rw [SlashInvariantForm.trace, IsBoundedAtImInfty, Filter.BoundedAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]
    refine .fun_sum (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)
    simpa using h.of_isFiniteRelIndex_conj hr

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) atImInfty (𝓝 (∑ c, 0))

Tactic:
refine tendsto_finsetSum _ (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ ?_)

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
x✝¹ : ↥ℋ
r : GL (Fin 2) ℝ
hr : r ∈ ℋ
x✝ : ⟦⟨r, hr⟩⟧ ∈ Finset.univ
⊢ Filter.Tendsto (quotientFunc f ⟦⟨r, hr⟩⟧ ∣[k] γ) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
r : ℝ
⊢ (fun t ↦ f (↑ofComplex (I * ↑t)) - valueAtInfty ⇑f) =O[atTop] fun t ↦ t ^ r

Tactic:
by
  obtain ⟨C, hCpos, hCO⟩ := ModularFormClass.exp_decay_sub_atImInfty' f
  refine (hCO.comp_tendsto tendsto_ofComplex_I_mul_atTop_atImInfty).trans ?_
  refine (EventuallyEq.isBigO ?_).trans (isLittleO_exp_neg_mul_rpow_atTop hCpos r).isBigO
  filter_upwards [eventually_gt_atTop 0] with t ht
  simp [ht, ofComplex_apply_of_im_pos, ← coe_im]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ModularFormClass
    (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range
      (0 *
        ↑(Nat.card
            (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))))
    (Matrix.SpecialLinearGroup.mapGL ℝ).range 0

Tactic:
rw [zero_mul]

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 0) (Matrix.SpecialLinearGroup.mapGL ℝ).range 0
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ∃ c, ⇑f = Function.const ℍ c

Tactic:
let : ModularFormClass (ModularForm 𝒮ℒ (0 * Nat.card (𝒮ℒ ⧸ 𝒢.subgroupOf 𝒮ℒ))) 𝒮ℒ 0 := by
    rw [zero_mul]; infer_instance
  obtain ⟨c, hc⟩ := ModularFormClass.levelOne_weight_zero_const
    (ModularForm.norm 𝒮ℒ (f - .const (f I)))
  -- But the constant must be 0, since `f - f I` vanishes at `I`.
  have : ModularForm.norm 𝒮ℒ (f - .const (f I)) I = 0 := by
    simpa [Finset.prod_eq_zero_iff, QuotientGroup.exists_mk] using ⟨1, by simp⟩
  obtain rfl : c = 0 := by simpa [hc]
  -- So `f - f I` has zero norm, hence it's the zero form.
  simp only [Function.const_zero, FunLike.coe_zero_iff, norm_eq_zero_iff, sub_eq_zero] at hc
  exact ⟨f I, by rw [hc, ModularForm.coe_const, Function.const_apply]⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K∞
v : InfinitePlace K
hv : ¬IsUnit (x v)
⊢ ‖x‖ = 0

Tactic:
exact Finset.prod_eq_zero_iff.2 ⟨v, Finset.mem_univ v, by simpa [isUnit_iff_ne_zero] using hv⟩

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case refine_2
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : ↑k + 1 < s.re
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ ↑k

Tactic:
simpa using ModularFormClass.qExpansion_isBigO hk.le f

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ emultiplicity (↑p) (x ^ (p ^ a * p) - y ^ (p ^ a * p)) = emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) + 1

Tactic:
pow_mul,

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ emultiplicity (↑p) ((x ^ p ^ a) ^ p - y ^ (p ^ a * p)) = emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) + 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
| emultiplicity (↑p) (x ^ (p ^ multiplicity p (n + 1) * k) - y ^ (p ^ multiplicity p (n + 1) * k))

Tactic:
pow_mul,

Goal state after:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
| emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - y ^ (p ^ multiplicity p (n + 1) * k))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ ↑k

Tactic:
rw [Int.natCast_dvd_natCast]
    rintro ⟨c, rfl⟩
    refine hpn ⟨c, ?_⟩
    rwa [pow_succ, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
⊢ (Support R k).Finite

Tactic:
have hd' : d ≠ 0 := nonZeroDivisors.ne_zero hd

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ (Support R k).Finite
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (∏ i ∈ range (d + 1), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by
      rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2.succ
x✝ y : ℤ
hx✝ : ¬2 ∣ x✝
hxy : 4 ∣ x✝ - y
hx_odd : Odd x✝
hxy_even : Even (x✝ - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
⊢ x ^ (2 ^ i * 2) % 4 = 1

Tactic:
pow_mul,

Goal state after:
case refine_2.succ
x✝ y : ℤ
hx✝ : ¬2 ∣ x✝
hxy : 4 ∣ x✝ - y
hx_odd : Odd x✝
hxy_even : Even (x✝ - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
⊢ (x ^ 2 ^ i) ^ 2 % 4 = 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ emultiplicity 2 (x ^ (2 ^ multiplicity 2 (n + 1) * k) - y ^ (2 ^ multiplicity 2 (n + 1) * k)) =
    emultiplicity 2 (x - y) + emultiplicity 2 ↑(2 ^ multiplicity 2 (n + 1) * k)

Tactic:
pow_mul,

Goal state after:
case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ emultiplicity 2 ((x ^ 2 ^ multiplicity 2 (n + 1)) ^ k - y ^ (2 ^ multiplicity 2 (n + 1) * k)) =
    emultiplicity 2 (x - y) + emultiplicity 2 ↑(2 ^ multiplicity 2 (n + 1) * k)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ emultiplicity 2 ((x ^ 2 ^ multiplicity 2 (n + 1)) ^ k - y ^ (2 ^ multiplicity 2 (n + 1) * k)) =
    emultiplicity 2 (x - y) + emultiplicity 2 ↑(2 ^ multiplicity 2 (n + 1) * k)

Tactic:
pow_mul,

Goal state after:
case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ emultiplicity 2 ((x ^ 2 ^ multiplicity 2 (n + 1)) ^ k - (y ^ 2 ^ multiplicity 2 (n + 1)) ^ k) =
    emultiplicity 2 (x - y) + emultiplicity 2 ↑(2 ^ multiplicity 2 (n + 1) * k)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
⊢ ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u

Tactic:
have : IsUnit y := by
    apply IsUnit.of_map (algebraMap (𝓞 K⁺) (𝓞 K))
    rw [show algebraMap (𝓞 K⁺) (𝓞 K) y = u by exact RingOfIntegers.ext hy]
    exact u.isUnit

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
this : IsUnit y
⊢ ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x_1, Real.exp ((↑x_1.mult)⁻¹ * (completeBasis K).equivFun.symm x x_1) =
    Real.exp (x w₀) ^ finrank ℚ K * (∏ w, ↑expMapBasis x ↑w)⁻¹

Tactic:
simp_rw [← prod_expMapBasis_pow, prod_eq_prod_mul_prod, expMapBasis_apply, expMap_apply,
      mult_isReal, mult_isComplex, pow_one, Finset.prod_pow, pow_two, mul_assoc, mul_inv_cancel₀
      (Finset.prod_ne_zero_iff.mpr <| fun _ _ ↦ Real.exp_ne_zero _), mul_one]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ (∫⋯∫⁻_univ.erase w₀, fun x ↦
        ∫⁻ (xᵢ : ℝ) in if w₀ = w₀ then Set.Iic 0 else Set.Ico 0 1,
          ENNReal.ofReal (Real.exp (Function.update x w₀ xᵢ w₀ * ↑n)) ∂fun i ↦
        volume.restrict (if i = w₀ then Set.Iic 0 else Set.Ico 0 1))
      0 =
    (↑n)⁻¹

Tactic:
if_pos rfl

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ (∫⋯∫⁻_univ.erase w₀, fun x ↦
        ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp (Function.update x w₀ xᵢ w₀ * ↑n)) ∂fun i ↦
        volume.restrict (if i = w₀ then Set.Iic 0 else Set.Ico 0 1))
      0 =
    (↑n)⁻¹
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) (∏ j ∈ primitiveRoots p (𝓞 K), eval 1 (X - C j))

Tactic:
simp only [eval_sub, eval_X, eval_C]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ -(↑B * (A i j)⁻) ≤ A i j * v j

Tactic:
← mul_comm (v j)

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ A i j * v j ≤ ↑B * (A i j)⁺

Tactic:
← mul_comm (v j)

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ v j * A i j ≤ ↑B * (A i j)⁺
Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
⊢ ∀ (x y z : C(X, Y)), dist x z ≤ max (dist x y) (dist y z)

Tactic:
intro f g h

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
⊢ dist f h ≤ max (dist f g) (dist g h)
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ x, 1 < ‖x‖

Tactic:
by
    choose x hx using NontriviallyNormedField.non_trivial (α := ℚ_[p])
    use x
    rw [PadicAlgCl.norm_extends]
    exact hx

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

Goal state before:
pp: case ih
p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ : WithVal (Rat.padicValuation p)
⊢ ⋯.extend coe' (((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) a✝) = ↑a✝

Tactic:
apply IsDenseInducing.extend_eq

Goal state after:
case ih
p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ : WithVal (Rat.padicValuation p)
⊢ Continuous coe'
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ q : ℚ
⊢ ⋯.extend coe' ↑q = ↑((WithVal.equiv (Rat.padicValuation p)).symm q)

Tactic:
apply IsDenseInducing.extend_eq

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ q : ℚ
⊢ Continuous coe'
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case ih
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
⊢ ‖withValUniformEquiv ↑a‖ ≤ 1 ↔ Valued.v a ≤ 1

Tactic:
← WithVal.apply_ofVal,

Goal state after:
case ih
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
⊢ ‖withValUniformEquiv ↑a‖ ≤ 1 ↔ (Rat.padicValuation p) a.ofVal ≤ 1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ^ 2 - a.x ^ 2 ≤ 0

Tactic:
sub_nonpos,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ^ 2 ≤ a.x ^ 2
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case left
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := ⋯
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1

Tactic:
rw [← coePolynomial_eq_algebraMap]

Goal state after:
case left
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ↑(q % π) = 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
l : ℕ
hl : l ∣ s.prodPrimes
⊢ 0 < selbergTerms l

Tactic:
rw [selbergTerms_apply]
  refine mul_pos (nu_pos_of_dvd_prodPrimes hl) <| prod_pos fun p hp ↦ ?_
  rw [inv_pos]
  have hp_prime : p.Prime := prime_of_mem_primeFactors hp
  have hp_dvd : p ∣ s.prodPrimes := (Nat.dvd_of_mem_primeFactors hp).trans hl
  linarith only [s.nu_lt_one_of_prime p hp_prime hp_dvd]

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: m n : ℕ
hc : m.Coprime n
hn : IsSquare (-1)
x : ZMod m
hx : -1 = x * x
⊢ IsSquare (-1, -1)

Tactic:
obtain ⟨y, hy⟩ := hn

Goal state after:
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (-1, -1)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
⊢ p % 4 ≠ 3

Tactic:
obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd (Nat.dvd_of_mem_primeFactors hp) hs

Goal state after:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : -1 = y * y
⊢ p % 4 ≠ 3
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: ⊢ Dense {x | Irrational x}

Tactic:
refine Real.isTopologicalBasis_Ioo_rat.dense_iff.2 ?_
  simp only [mem_iUnion, mem_singleton_iff, exists_prop, forall_exists_index, and_imp]
  rintro _ a b hlt rfl _
  rw [inter_comm]
  exact exists_irrational_btwn (Rat.cast_lt.2 hlt)

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

Goal state before:
pp: ⊢ Filter.Eventually (Membership.mem (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n))) (residual ℝ)

Tactic:
refine residual_of_dense_Gδ ?_ (Rat.isDenseEmbedding_coe_real.dense.mono ?_)

Goal state after:
case refine_1
⊢ IsGδ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

case refine_2
⊢ range Rat.cast ⊆ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
⊢ Unbounded (fun x1 x2 ↦ x1 ≤ x2) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a < b

Tactic:
by
  simp only [Unbounded, not_le]

Goal state after:
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ ⋂ i, lowerBounds {u i} = ⋂ i, lowerBounds (s i)

Tactic:
lowerBounds_singleton,

Goal state after:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ ⋂ i, Iic (u i) = ⋂ i, lowerBounds (s i)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x

Tactic:
by rw [add_comm, add_int_iff]

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

Goal state before:
pp: r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), volume {x | ∃ a ∈ Finset.Icc 0 ↑i, |x - ↑a / ↑i| < 1 / ↑i ^ r} ≠ ∞

Tactic:
simp only [ofPred_exists, ← exists_prop, ← Real.dist_eq, ← mem_ball, ofPred_mem_eq]

Goal state after:
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ∞
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ ∃ m, x ≠ ↑m / ↑b ∧ |x - ↑m / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊

Tactic:
refine ⟨a, hne, ?_⟩

Goal state after:
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ |x - ↑a / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: α : Type u
l : Filter α
x✝ : CardinalInterFilter l (ℵ_ 1)
⊢ CountableInterFilter l

Tactic:
by
    refine ⟨fun S h a ↦ CardinalInterFilter.cardinal_sInter_mem (c := ℵ₁) S ?_ a⟩
    rwa [lt_aleph_one_iff, le_aleph0_iff_set_countable]

Goal state after:
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
⊢ ⊥ᶜᶜ = ⊥

Tactic:
compl_bot,

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
⊢ ⊤ᶜ = ⊥