mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ h.modByMonicHom (h.root ^ n) = X ^ n

Tactic:
rw [← h.map_X, ← map_pow, modByMonicHom_map, modByMonic_eq_self_iff h.monic, degree_X_pow]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ ↑n < f.degree
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
⊢ Associated f (minpoly R h.root)

Tactic:
by
      convert!
        Associated.mul_left (minpoly R h.root) <|
          associated_one_iff_isUnit.2 <|
            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
      rw [mul_one]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s
⊢ deriv (fun w ↦ w - 1) s * LFunction 1 s + (s - 1) * deriv (LFunction 1) s =
    (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
deriv_sub_const,

Goal state after:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s
⊢ deriv (fun w ↦ w) s * LFunction 1 s + (s - 1) * deriv (LFunction 1) s =
    (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
hw' : w ≠ 1
⊢ LFunctionTrivChar₁ n w ≠ 0

Tactic:
· rw [LFunctionTrivChar₁, Function.update_of_ne hw', mul_ne_zero_iff]
    exact ⟨sub_ne_zero_of_ne hw', (Set.mem_ofPred.mp hw).resolve_left hw'⟩

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
⊢ ContinuousOn (fun s ↦ -deriv (LFunction χ) s / LFunction χ s) {s | LFunction χ s ≠ 0}

Tactic:
have h := differentiable_LFunction hχ

Goal state after:
n : ℕ
inst✝ : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
h : Differentiable ℂ (LFunction χ)
⊢ ContinuousOn (fun s ↦ -deriv (LFunction χ) s / LFunction χ s) {s | LFunction χ s ≠ 0}
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
⊢ hurwitzZetaEven (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
have h3 : Gammaℂ (2 * k) ≠ 0 := by
    refine mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)
    simp [pi_ne_zero]

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ hurwitzZetaEven (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    ∑ i, cexp (↑π * (I * s) / 2) * (Φ i * expZeta (toAddCircle (-i)) s) +
      ∑ i, cexp (-↑π * (I * s) / 2) * (Φ i * expZeta (toAddCircle i) s)

Tactic:
← sum_add_distrib,

Goal state after:
case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    ∑ x,
      (cexp (↑π * (I * s) / 2) * (Φ x * expZeta (toAddCircle (-x)) s) +
        cexp (-↑π * (I * s) / 2) * (Φ x * expZeta (toAddCircle x) s))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
suffices hurwitzZetaOdd x (1 - 2 * k) = 0 by
    rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖(toArithmeticFunction fun x ↦ χ ↑x) n‖ ≤ 1

Tactic:
simpa only [toArithmeticFunction, coe_mk, hn, ↓reduceIte]
  using norm_le_one χ _

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x))
    (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))

Tactic:
convert! (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).nat_add_neg using 1

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n ↦ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x)) = fun n ↦
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x

case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) =
    -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / ↑0 ^ k * (fourier 0) ↑x
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1.refine_2
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun x ↦ x + 1
u : Nat.Primes × ℕ
hu : u ∉ Set.range (Prod.map id fun x ↦ x + 1)
⊢ F' u = 0

Tactic:
· simp only [Set.range_prodMap, Set.range_id, Set.mem_prod, Set.mem_univ, Set.mem_range,
      Nat.exists_add_one_eq, true_and, not_lt, nonpos_iff_eq_zero] at hu
    rw [← hF'₀ u.1, ← hu]

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : s ∈ {s | 1 < s.re}
⊢ LFunctionResidueClassAux a s = (fun s ↦ L (fun n ↦ ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) s

Tactic:
replace hs := Set.mem_ofPred.mp hs

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ LFunctionResidueClassAux a s = (fun s ↦ L (fun n ↦ ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) s
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1
hb : b ≠ 0
h : a.gcd ↑b ≠ 1
⊢ J(a | b) = 0

Tactic:
rw [← neZero_iff] at hb; exact eq_zero_iff_not_coprime.2 h

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
n : ℕ
h : (List.map (fun n ↦ J(a | n)) n.primeFactorsList).prod = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
obtain ⟨p, hmem, hj⟩ := List.mem_map.mp (List.neg_one_mem_of_prod_eq_neg_one h)

Goal state after:
a : ℤ
n : ℕ
h : (List.map (fun n ↦ J(a | n)) n.primeFactorsList).prod = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
p : ℕ
hmem : p ∈ n.primeFactorsList
hj : J(a | p) = -1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ Nat.gcd 2 1 = 1

Tactic:
Nat.gcd_one_right

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ 1 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
⊢ J(↑a | b) = qrSign b a * J(↑b | a)

Tactic:
have rhs_apply : ∀ a b : ℕ, rhs a b = qrSign b a * J(b | a) := fun a b => rfl

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
⊢ J(↑a | b) = qrSign b a * J(↑b | a)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' i : ℕ
⊢ sZMod (p' + 2) i = ↑(s i)

Tactic:
induction i with

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0

Tactic:
sZMod_eq_sMod p

Goal state after:
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 ↔ sMod p (p - 2) = 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q i : ℕ
⊢ ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i

Tactic:
induction i with

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
⊢ ∀ (s : Set ↥H),
    IsOpen[instTopologicalSpaceSubtype] (⇑(subgroupOfEquivOfLe hHK) ⁻¹' s) ↔ IsOpen[instTopologicalSpaceSubtype] s

Tactic:
simp only [subgroupOfEquivOfLe, Topology.IsInducing.subtypeVal.isOpen_iff,
      exists_exists_and_eq_and]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
⊢ ∀ (s : Set ↥H),
    (∃ a,
        IsOpen[inst✝] a ∧
          Subtype.val ⁻¹' Subtype.val ⁻¹' a =
            ⇑{ toFun := fun g ↦ ⟨↑↑g, ⋯⟩, invFun := fun g ↦ ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
                  map_mul' := ⋯ } ⁻¹'
              s) ↔
      ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = s
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
⊢ Fintype.card (X q) = q ^ 2

Tactic:
by
  change Fintype.card (ZMod q × ZMod q) = q ^ 2
  rw [Fintype.card_prod, ZMod.card q, sq]

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
inst✝² : Γ.HasDetOne
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (c • ⇑f) ∣[k] γ = c • ⇑f

Tactic:
rw [← smul_one_smul ℂ]

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
inst✝² : Γ.HasDetOne
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ((c • 1) • ⇑f) ∣[k] γ = (c • 1) • ⇑f
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h𝒢 : -1 ∈ 𝒢
⊢ 𝒢.strictPeriods = 𝒢.periods

Tactic:
by
  simp [Subgroup.periods, adjoinNegOne_eq_self_iff.mpr h𝒢]

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

Goal state before:
pp: case mpr.hx
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ γ ∈ Subgroup.closure s

Tactic:
· simpa [← hΓ]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
⊢ ?m.56 ∈ ball 0 1

Tactic:
by simpa using hq

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
obtain ⟨F, hF𝒟⟩ : ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t :=
    exists_bound_fundamental_domain_of_isBigO hf_cont hf_infinity
  refine ⟨F, fun τ ↦ ?_⟩
  -- Given `τ`, choose a `g = [a, b; c, d] ∈ SL(2, ℤ)` that translates `τ` into `𝒟`.
  obtain ⟨g, hg⟩ := exists_smul_mem_fd τ
  specialize hF𝒟 (g • τ) hg
  rw [hf_inv g τ] at hF𝒟
  grw [hF𝒟]
  gcongr
  · rw [← div_le_iff₀ (by positivity)] at hF𝒟
    exact le_trans (by positivity) hF𝒟
  -- It remains to show `(g • τ).im ≤ max τ.im (1 / τ.im)`.
  -- We split into two cases depending whether `c = g 1 0` is zero.
  rw [im_smul_eq_div_normSq, denom_apply]
  by_cases hg : g 1 0 = 0
  · -- If `c = 0`, then `(g • τ).im = τ.im / d ^ 2` and `d ^ 2 ≥ 1`.
    -- (In fact `d = ±1`, but we do not need this stronger statement).
    have : g 1 1 ≠ 0 := fun hg' ↦ zero_ne_one <| by
      simpa only [Matrix.det_fin_two, hg, hg', mul_zero, mul_zero, sub_zero] using g.det_coe
    have : (1 : ℝ) ≤ g 1 1 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs this)
    refine le_trans ?_ <| le_max_left _ _
    rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) = (g 1 1) ^ 2 by simp [hg, sq]]
    simpa [field] using inv_le_one_of_one_le₀ this
  · -- If `c ≠ 0`, then `1 ≤ c ^ 2`, so
    -- `(g • τ).im = τ.im / (c ^ 2 * τ.im ^ 2 +  ...) ≤ 1 / τ.im`.
    refine le_trans ?_ <| le_max_right _ _
    rw [show 1 / τ.im = τ.im / τ.im ^ 2 by field_simp]
    gcongr
    rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) =
      ((g 1 0) * τ.re + (g 1 1)) ^ 2 + (g 1 0) ^ 2 * τ.im ^ 2 by simp [Complex.normSq_apply]; ring]
    have : (1 : ℝ) ≤ g 1 0 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs hg)
    nlinarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
rw [hzre, add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_le,
      Int.abs_le_one_iff] at this
    rcases this with h | h | h <;> simp only [h, Int.cast_zero, zero_add, Int.cast_one] at this
    · grind [zpow_zero]
    · rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre <;> [skip; norm_num [hzre] at this]
      rw [h, zpow_one] at hg'
      refine .inr <| .inr ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) ?_⟩
      simp [hz', show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_ρ]
    · rw [abs_eq (by norm_num)] at hzre
      rcases hzre with hzre | hzre <;> [norm_num [hzre] at this; skip]
      rw [h, zpow_neg_one] at hg'
      exact .inr <| .inl ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) (by rw [hz', norm_ρ])⟩

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

Goal state before:
pp: k : ℕ
x✝ : ℂ
hq : x✝ ∈ Metric.ball 0 1
⊢ ‖x✝‖ < 1

Tactic:
by simpa using hq

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

Goal state before:
pp: z : ℍ
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = deriv sqrt ↑z / (↑z).sqrt + logDeriv η ↑z

Tactic:
have hE2 := congrFun (E2_slash_action ModularGroup.S) z

Goal state after:
z : ℍ
hE2 : (E2 ∣[2] ModularGroup.S) z = (E2 - (1 / (2 * riemannZeta 2)) • D2 ModularGroup.S) z
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = deriv sqrt ↑z / (↑z).sqrt + logDeriv η ↑z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hg
⊢ DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet

pp: case hs2
⊢ IsOpen upperHalfPlaneSet

pp: case hsc
⊢ IsPreconnected upperHalfPlaneSet

pp: case hgn
⊢ ∀ x ∈ upperHalfPlaneSet, (sqrt * η) x ≠ 0

pp: case hfn
⊢ ∀ x ∈ upperHalfPlaneSet, (η ∘ fun z ↦ -1 / z) x ≠ 0

Tactic:
· exact fun x hx ↦ ((differentiableAt_sqrt (mem_slitPlane ⟨x, hx⟩)).mul
     (differentiableAt_eta_of_mem_upperHalfPlaneSet hx)).differentiableWithinAt

Goal state after:
case hs2
⊢ IsOpen upperHalfPlaneSet

case hsc
⊢ IsPreconnected upperHalfPlaneSet

case hgn
⊢ ∀ x ∈ upperHalfPlaneSet, (sqrt * η) x ≠ 0

case hfn
⊢ ∀ x ∈ upperHalfPlaneSet, (η ∘ fun z ↦ -1 / z) x ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hf
htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this : Tendsto (fun x ↦ (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑x) ^ (n + 1))) ^ 24) atImInfty (𝓝 1)
τ : ℍ
⊢ ∀ (b : ℕ), 1 - eta_q b ↑τ = 1 - cexp (2 * ↑π * I * ↑τ) ^ (b + 1)

Tactic:
simp [eta_q, Periodic.qParam, ← exp_nat_mul]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ Δ * ⇑(CuspForm.discriminantEquiv f) = ⇑f

Tactic:
grind [Pi.mul_apply, discriminant_mul_discriminantEquiv_apply]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝ : T • z ≠ z
this : T⁻¹ • z ≠ z
⊢ g = 1 ∨ g = -1

Tactic:
have : (z : ℂ) ≠ -I := by grind [neg_im, coe_I, Complex.I_im, z.coe_im_pos]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
⊢ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hx : 1 ≤ normSq ↑x
hx' : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ

Tactic:
rw [one_le_normSq_iff] at hx

Goal state after:
x : ℍ
hx : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
⊢ (fun x ↦
      (translate f
            (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))
          (↑ofComplex (I * ↑x)) -
        valueAtInfty
          ⇑(translate f
              (Matrix.SpecialLinearGroup.toGL
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))) =O[atTop]
    fun x ↦ x ^ r

Tactic:
exact isBigO_comp_ofComplex_I_mul_sub_valueAtInfty (translate f ModularGroup.S) r

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: v : InfinitePlace ℚ
x : ℚ
⊢ ‖↑x‖ = ↑|x|

Tactic:
rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv,
    norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
    Rat.infinitePlace_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ single A i (x i * r) = x * single A i r

Tactic:
ext j
  rcases eq_or_ne i j with rfl | hne; · simp
  simp [single_eq_of_ne' A _ hne]

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ single A i (r * x i) = single A i r * x

Tactic:
ext j
  rcases eq_or_ne i j with rfl | hne; · simp
  simp [single_eq_of_ne' A _ hne]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = emultiplicity ↑p ↑(x - y) + emultiplicity p n

Tactic:
← Int.natCast_dvd_natCast

Goal state after:
case inl
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑(x - y)
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = emultiplicity ↑p ↑(x - y) + emultiplicity p n
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: p : ℕ
hp : 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:
← Int.natCast_dvd_natCast

Goal state after:
p : ℕ
hp : 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.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
a : 𝔸ᶠ[R, K]ˣ
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    Valued.v ↑(((RestrictedProduct.unitsEquiv (adicCompletion K)) a) v) = 1

Tactic:
filter_upwards [(RestrictedProduct.unitsEquiv _ a).2] using fun _ h ↦
    adicCompletionIntegers.mem_units_iff_valued_eq_one.1 h

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 =
    emultiplicity (↑2) (↑x + ↑y) + emultiplicity (↑2) (↑x - ↑y) + emultiplicity 2 n

Tactic:
← Int.natCast_dvd_natCast

Goal state after:
case inl
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 =
    emultiplicity (↑2) (↑x + ↑y) + emultiplicity (↑2) (↑x - ↑y) + emultiplicity 2 n
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 * Module.finrank ℚ ↥K⁺ = 2 * nrComplexPlaces K

Tactic:
← IsTotallyComplex.finrank,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 * Module.finrank ℚ ↥K⁺ = Module.finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ↑x ∈ K⁺
this : IsIntegral ℤ ⟨↑x, h⟩
⊢ (algebraMap (↥K⁺) K) ((algebraMap (𝓞 ↥K⁺) ↥K⁺) ⟨⟨↑x, h⟩, this⟩) = ↑x

Tactic:
RingOfIntegers.map_mk

Goal state after:
case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ↑x ∈ K⁺
this : IsIntegral ℤ ⟨↑x, h⟩
⊢ (algebraMap (↥K⁺) K) ⟨↑x, h⟩ = ↑x
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case e'_3
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 = (Subgroup.map (unitsMulComplexConjInv K) (torsion K)).index

Tactic:
map_unitsMulComplexConjInv_torsion,

Goal state after:
case e'_3
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 = (powMonoidHom 2).range.index