mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case pos
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Even
⊢ ZMod.completedLFunction (⇑χ) (1 - s) = ↑N ^ (s - 1) * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)

Goal state after:
case pos
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Even
⊢ ↑N ^ (s - 1) * ZMod.completedLFunction (𝓕 ⇑χ) s = ↑N ^ (s - 1) * ZMod.completedLFunction (𝓕 ⇑χ) s
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ normalizedFactors (Ideal.map (algebraMap R S) I) =
    Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach

Tactic:
ext J
  -- WLOG, assume J is a normalized factor
  by_cases hJ : J ∈ normalizedFactors (I.map (algebraMap R S))
  swap
  · rw [Multiset.count_eq_zero.mpr hJ, eq_comm, Multiset.count_eq_zero, Multiset.mem_map]
    simp only [not_exists]
    rintro J' ⟨_, rfl⟩
    exact
      hJ ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J').prop
  -- Then we just have to compare the multiplicities, which we already proved are equal.
  have := emultiplicity_factors_map_eq_emultiplicity hI hI' hx hx' hJ
  rw [emultiplicity_eq_count_normalizedFactors, emultiplicity_eq_count_normalizedFactors,
    UniqueFactorizationMonoid.normalize_normalized_factor _ hJ,
    UniqueFactorizationMonoid.normalize_normalized_factor, Nat.cast_inj] at this
  · refine this.trans ?_
    -- Get rid of the `map` by applying the equiv to both sides.
    generalize hJ' :
      (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
    have : ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J' : Ideal S) =
        J := by
      rw [← hJ', Equiv.symm_apply_apply _ _, Subtype.coe_mk]
    subst this
    -- Get rid of the `attach` by applying the subtype `coe` to both sides.
    rw [Multiset.count_map_eq_count' fun f =>
        ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f :
          Ideal S),
      Multiset.count_attach]
    · exact Subtype.coe_injective.comp (Equiv.injective _)
  · exact (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop
  · exact irreducible_of_normalized_factor _
        (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop
  · exact Polynomial.map_monic_ne_zero (minpoly.monic hx')
  · exact irreducible_of_normalized_factor _ hJ
  · rwa [← bot_eq_zero, Ne,
      map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case refine_1.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ Φ 0 = 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Tactic:
· exact fun h ↦ by simp only [h, funext zero_div, differentiableAt_const]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
⊢ 0 ≤ χ.zetaMul (p ^ k)

Tactic:
by
  simp only [zetaMul, toArithmeticFunction, coe_zeta_mul_apply, coe_mk,
    Nat.sum_divisors_prime_pow hp, pow_eq_zero_iff', hp.ne_zero, ne_eq, false_and, ↓reduceIte,
    Nat.cast_pow, map_pow]
  rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h
  · refine Finset.sum_nonneg fun i _ ↦ ?_
    simp only [h, le_refl, pow_nonneg]
  · refine Finset.sum_nonneg fun i _ ↦ ?_
    simp only [h, one_pow, zero_le_one]
  · simp only [h, neg_one_geom_sum]
    split_ifs
    exacts [le_rfl, zero_le_one]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
⊢ ↑(bernoulliFun k y) = ↑(periodizedBernoulli k ↑y)

Tactic:
ofReal_inj,

Goal state after:
case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
⊢ bernoulliFun k y = periodizedBernoulli k ↑y
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s = deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Tactic:
deriv_LFunctionTrivChar₁_apply_of_ne_one _ hs₁,

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ ((s - 1) * deriv (LFunctionTrivChar q) s + LFunctionTrivChar q s) / LFunctionTrivChar₁ q s =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case pos
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : v w ≤ ↑↑z
b : K
hb : (MonoidWithZeroHom.ofClass v) b = ↑↑z
⊢ IsOpen {w | v w ≤ ↑↑z}

Tactic:
← hb

Goal state after:
case pos
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : v w ≤ ↑↑z
b : K
z0 : 0 < (MonoidWithZeroHom.ofClass v) b
hb : (MonoidWithZeroHom.ofClass v) b = ↑↑z
⊢ IsOpen {w | v w ≤ (MonoidWithZeroHom.ofClass v) b}
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ J(a | 2 * b) = J(a | 2 * b / 2)

Tactic:
mul_right' a (by decide) fun h ↦ hb0 (mul_eq_zero_of_right 2 h),

Goal state after:
case neg
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ J(a | 2) * J(a | b) = J(a | 2 * b / 2)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (1 + α) ^ (q + 1) = -2

Tactic:
rw [pow_succ, one_add_α_pow_q odd leg3, mul_comm, ← _root_.sq_sub_sq, α_sq]
  norm_num

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
⊢ ∃ N, N ≠ 0 ∧ ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)

Tactic:
by
  -- Give names to the numerators and denominators of `g` and `g⁻¹`
  let A₁ := g.1
  let A₂ := (g⁻¹).1
  have hA₁₂ : A₁ * A₂ = 1 := by simp only [← Matrix.GeneralLinearGroup.coe_mul,
    mul_inv_cancel, Matrix.GeneralLinearGroup.coe_one, A₁, A₂]
  let a₁ := A₁.den
  let a₂ := A₂.den
  -- we take `N = a₁ * a₂`
  refine ⟨a₁ * a₂ * M, mul_ne_zero (mul_ne_zero A₁.den_ne_zero A₂.den_ne_zero) (NeZero.ne _),
    fun ⟨y, hy⟩ hy' ↦ ?_⟩
  -- Show that `y` is of the form `1 + (a₁ * a₂) • k` for some integer matrix `k`.
  obtain ⟨k, hk⟩ : ∃ k, y = 1 + (a₁ * a₂ * M) • k := by
    replace hy' : y.map (Int.cast : ℤ → ZMod (a₁ * a₂ * M)) = 1 := by
      rw [CongruenceSubgroup.Gamma_mem', Subtype.ext_iff] at hy'
      simpa using! hy'
    use Matrix.of fun i j ↦ (y - 1) i j / (a₁ * a₂ * M)
    rw [← sub_eq_iff_eq_add']
    ext i j
    simp_rw [Matrix.smul_apply, Matrix.of_apply, nsmul_eq_mul, Nat.cast_mul]
    refine (Int.mul_ediv_cancel_of_dvd ?_).symm
    rw [← Matrix.map_one Int.cast (by simp) (by simp), ← sub_eq_zero,
      ← Matrix.map_sub _ (by simp)] at hy'
    simpa only [Matrix.zero_apply, Matrix.map_apply, ZMod.intCast_zmod_eq_zero_iff_dvd,
      Nat.cast_mul] using! congr_fun₂ hy' i j
  -- use this `k` to cook up a new integer matrix, which we will show comes from `SL(2, ℤ)`
  let z := 1 + M • (A₁.num * k * A₂.num)
  have hz_coe : z.map Int.cast = A₁ * (y.map Int.cast) * A₂ := by
    simp only [Matrix.map_add _ Int.cast_add, Matrix.map_one _ Int.cast_zero Int.cast_one, hk,
      mul_add, mul_one, add_mul, hA₁₂, add_right_inj, z]
    conv_rhs => rw [← A₁.inv_denom_smul_num, ← A₂.inv_denom_smul_num, Matrix.map_smul _ _ (by simp)]
    simp only [Matrix.smul_mul, Matrix.mul_smul, Matrix.map_smul (Int.cast : ℤ → ℚ) M (by simp),
      Matrix.map_mul_intCast]
    rw [← Nat.cast_smul_eq_nsmul ℚ (_ * M), ← mul_smul, ← mul_smul,
      mul_comm a₁ a₂, Nat.cast_mul, Nat.cast_mul, mul_assoc _ _ (M : ℚ), mul_comm _ (M : ℚ),
      inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),
      mul_inv_cancel_right₀ (mod_cast A₁.den_ne_zero), Nat.cast_smul_eq_nsmul]
  have hz_det : z.det = 1 := by
    have := congr_arg Matrix.det hz_coe
    simp_rw [Matrix.det_mul, ← Int.cast_det] at this
    rwa [mul_right_comm, ← Matrix.det_mul, hA₁₂, Matrix.det_one, one_mul, hy, Int.cast_inj] at this
  refine ⟨⟨z, hz_det⟩, ?_, by simpa only [Subtype.ext_iff, Subgroup.coe_mul, Units.ext_iff,
    Units.val_mul] using! hz_coe⟩
  rw [SetLike.mem_coe, CongruenceSubgroup.Gamma_mem', Subtype.ext_iff]
  ext i j
  simp_rw [map_apply_coe, z, map_add, map_one, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    Matrix.add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul,
    Int.cast_mul, Int.cast_natCast, ZMod.natCast_self M, zero_mul]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Set.SurjOn (fun g ↦ ↑g 1) Set.univ {cd | IsCoprime (cd 0) (cd 1)}

Tactic:
by
  rintro cd ⟨b₀, a, gcd_eqn⟩
  let A := of ![![a, -b₀], cd]
  have det_A_1 : det A = 1 := by
    convert! gcd_eqn
    rw [det_fin_two]
    simp [A, (by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]
  refine ⟨⟨A, det_A_1⟩, Set.mem_univ _, ?_⟩
  ext; simp [A]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
⊢ (((↑z).im⁻¹ • g) ∘ₗ f) c = LinearMap.id c

Tactic:
have hz : (z : ℂ).im ≠ 0 := z.2.ne'

Goal state after:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (((↑z).im⁻¹ • g) ∘ₗ f) c = LinearMap.id c
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : g • ∞ = ∞
⊢ 𝒢.strictWidthInfty ≠ 0

Tactic:
← AddSubgroup.zmultiples_ne_bot

Goal state after:
case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : g • ∞ = ∞
⊢ AddSubgroup.zmultiples 𝒢.strictWidthInfty ≠ ⊥
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ 0 < 𝒢.strictWidthInfty

Tactic:
strictWidthInfty_pos_iff

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ IsCusp ∞ 𝒢
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.left
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ -(1 / 2) ≤ (g • z).re

Tactic:
contrapose! hg'

Goal state after:
case right.left
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
⊢ ∃ g', ↑g 1 = ↑g' 1 ∧ |(g' • z).re| < |(g • z).re|
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.right
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ (g • z).re ≤ 1 / 2

Tactic:
contrapose! hg'

Goal state after:
case right.right
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
⊢ ∃ g', ↑g 1 = ↑g' 1 ∧ |(g' • z).re| < |(g • z).re|
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
this :
  (qExpansionRingHom h hh hΓ) ((DirectSum.of (ModularForm Γ) k) f ^ n) =
    (qExpansionRingHom h hh hΓ) ((DirectSum.of (ModularForm Γ) k) f) ^ n
⊢ qExpansion h ⇑(((DirectSum.of (ModularForm Γ) k) f ^ n) (↑n * k)) = qExpansion h ⇑f ^ n

Tactic:
simpa [DirectSum.ofPow]

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun x ↦ ∑' (y : ↥(↑x).divisorsAntidiagonal), ‖↑(↑⟨x, y⟩.snd).2 ^ k * r ^ ((↑⟨x, y⟩.snd).1 * (↑⟨x, y⟩.snd).2)‖

Tactic:
simp only [norm_mul, norm_pow, tsum_fintype, Finset.univ_eq_attach]

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun x ↦ ∑ y ∈ (↑x).divisorsAntidiagonal.attach, ‖↑(↑y).2‖ ^ k * ‖r‖ ^ ((↑y).1 * (↑y).2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ 1 = -↑ρ * (↑1 + ↑ρ)

Tactic:
grind [ρ_sq, ofReal_one]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
⊢ 1 = -↑ρ * (↑1 + ↑ρ)

Tactic:
grind [ρ_sq, ofReal_one]

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * ↑(↑g).det ^ (k - 1 + 2) * denom g ↑z ^ (-(k + 2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))

Tactic:
show -(k + 2) = -k + -2 by ring,

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * ↑(↑g).det ^ (k - 1 + 2) * denom g ↑z ^ (-k + -2)) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: x : ℂ
hx : x ∈ upperHalfPlaneSet
⊢ x.sqrt ≠ 0

Tactic:
by simp [sqrt, ne_zero ⟨x, hx⟩]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
⊢ a ∈ Set.Ioi 0 → { coe := ↑x + ↑↑a * Complex.I, coe_im_pos := ⋯ } ∈ closure 𝒟ᵒ

Tactic:
(ha : 0 < a)

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ { coe := ↑x + ↑↑a * Complex.I, coe_im_pos := ⋯ } ∈ closure 𝒟ᵒ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: ⊢ ∃ c, ∀ᶠ (b : ℝ) in atTop, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖

Tactic:
Filter.eventually_atTop

Goal state after:
⊢ ∃ c a, ∀ (b : ℝ), a ≤ b → ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: ⊢ Tendsto (fun t ↦ ↑ofComplex (I * ↑t)) atTop (comap UpperHalfPlane.im atTop)

Tactic:
tendsto_comap_iff

Goal state after:
⊢ Tendsto (UpperHalfPlane.im ∘ fun t ↦ ↑ofComplex (I * ↑t)) atTop atTop
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:
by
    rw [zero_mul]; infer_instance

Goal state after:
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 : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n

Tactic:
rw [← sub_neg_eq_add, ← sub_neg_eq_add, ← Odd.neg_pow hn]

Goal state after:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - -y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n - (-y) ^ n) = emultiplicity (↑p) (x - -y) + emultiplicity p n
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
φ : K →+* ℂ
⊢ ComplexEmbedding.IsConj φ (complexConj K)

Tactic:
obtain ⟨σ, hσ⟩ := exists_isConj _ φ
  have := (exists_isConj K (Classical.choice (inferInstance : Nonempty (K →+* ℂ)))).choose_spec
  rwa [isConj_eq_isConj K hσ this] at hσ

Goal state after:
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
x✝¹ x✝ : K
⊢ (complexConj K) (x✝¹ * x✝) = (complexConj K) x✝ * (complexConj K) x✝¹

Tactic:
by rw [map_mul, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ AddSubgroup.map (logEmbedding K)
      (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)) ⊔ Subgroup.toAddSubgroup (torsion K)) ≤
    AddSubgroup.map (logEmbedding K)
      (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)) ⊔ Subgroup.toAddSubgroup (torsion K))

Tactic:
← SupHomClass.map_sup,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u) ⊔ torsion K)) ≤
    AddSubgroup.map (logEmbedding K)
      (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)) ⊔ Subgroup.toAddSubgroup (torsion K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap
            (mixedSpaceOfRealSpace (↑expMap ((completeBasis K).equivFun.symm fun i ↦ if i = w₀ then 0 else x i)))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
logMap_expMap (by rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun w ↦
          (completeBasis K).equivFun.symm (fun i ↦ if i = w₀ then 0 else x i) ↑w)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1