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

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (cexp (2 * ↑π * I * ↑↑x✝ * ↑x) - cexp (2 * ↑π * I * ↑(-↑x✝) * ↑x / 1)) / (2 * I) =
    (cexp (-(↑(2 * π * ↑x✝) * ↑x) * I) - cexp (↑(2 * π * ↑x✝) * ↑x * I)) * I / 2

Tactic:
div_one,

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (cexp (2 * ↑π * I * ↑↑x✝ * ↑x) - cexp (2 * ↑π * I * ↑(-↑x✝) * ↑x)) / (2 * I) =
    (cexp (-(↑(2 * π * ↑x✝) * ↑x) * I) - cexp (↑(2 * π * ↑x✝) * ↑x * I)) * I / 2
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1.inr
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
n : ℕ
hn : n > 0
⊢ residueClass a n / ↑n ^ x ≤ residueClass a n / ↑n

Tactic:
· refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_
        conv_lhs => rw [← Real.rpow_one n]
        exact Real.rpow_le_rpow_of_exponent_le (by norm_cast) hx.le

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

Goal state before:
pp: case refine_1
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
n : ℕ
⊢ residueClass a n / ↑n ^ x ≤ residueClass a n / ↑n

pp: case refine_2
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
⊢ Summable fun n ↦ residueClass a n / ↑n ^ x

Tactic:
· rcases n.eq_zero_or_pos with rfl | hn
      · simp
      · refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_
        conv_lhs => rw [← Real.rpow_one n]
        exact Real.rpow_le_rpow_of_exponent_le (by norm_cast) hx.le

Goal state after:
case refine_2
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
⊢ Summable fun n ↦ residueClass a n / ↑n ^ x
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q a : ℕ
hq : q ≠ 0
h : a.Coprime q
n p : ℕ
hn : p > n
hp : Prime p
ha : p ≡ a [MOD q]
⊢ ∃ b, n ≤ b ∧ Prime b ∧ b ≡ a [MOD q]

Tactic:
exact ⟨p, hn.le, hp, ha⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
⊢ x < 1

Tactic:
simp [-exp_neg, x, ← lt_map_inv_iff, ← exp_zero]

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

Goal state before:
pp: case inr
a : ℤ
b : ℕ
h✝ : NeZero b
h : J(a | b) = 0
⊢ a.gcd ↑b ≠ 1

Tactic:
exact eq_zero_iff_not_coprime.1 h

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inl
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : y < x
⊢ (Set.Icc x y).Finite

pp: case inr.inl
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
⊢ (Set.Icc y y).Finite

pp: case inr.inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
⊢ (Set.Icc x y).Finite

Tactic:
· rw [Set.Icc_eq_empty_of_lt]
      · exact Set.finite_empty
      · simp [hxy]

Goal state after:
case inr.inl
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
⊢ (Set.Icc y y).Finite

case inr.inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
⊢ (Set.Icc x y).Finite
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.specialize_2
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 ≤ 1
⊢ ∃ i, w ∈ if v i ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v i}

Tactic:
use if v w ≤ z then a else w

Goal state after:
case h
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 := ⋯
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : v w ≤ 1
⊢ w ∈ if v (if v w ≤ ↑↑z then a else w) ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w_1 | v w_1 = v (if v w ≤ ↑↑z then a else w)}
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = if false = true then -J(↑(a % ↑b).natAbs | b) else J(↑(a % ↑b).natAbs | b)

pp: case neg.hb2
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b % 2 = 1

pp: case neg.hb1
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b > 1

Tactic:
if_neg Bool.false_ne_true,

Goal state after:
case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = J(↑(a % ↑b).natAbs | b)

case neg.hb2
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b % 2 = 1

case neg.hb1
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b > 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p i : ℕ
⊢ sZMod p i = ↑(sMod p i)

Tactic:
induction i <;> push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]

Goal state after:
case zero
p : ℕ
⊢ 4 = 4

case succ
p n✝ : ℕ
a✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ ↑(sMod p n✝) ^ 2 - 2 = ↑(sMod p n✝) ^ 2 - 2
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
⊢ a * b ∈ {g | ↑(↑g 1 0) = 0}

Tactic:
have h := (Matrix.two_mul_expl a.1 b.1).2.2.1

Goal state after:
N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
h : (↑a * ↑b) 1 0 = ↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0
⊢ a * b ∈ {g | ↑(↑g 1 0) = 0}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ) t = g ^ n
this : GeneralLinearGroup.det (g ^ n) = GeneralLinearGroup.det ((mapGL ℝ) t)
⊢ |↑(GeneralLinearGroup.det g ^ n)| = 1

Tactic:
Matrix.SpecialLinearGroup.det_mapGL,

Goal state after:
n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ) t = g ^ n
this : GeneralLinearGroup.det (g ^ n) = 1
⊢ |↑(GeneralLinearGroup.det g ^ n)| = 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ DiscreteTopology ↥(map (Int.castRingHom ℝ)).range

Tactic:
refine (Topology.IsEmbedding.toHomeomorph ?_).discreteTopology
  exact Real.isClosedEmbedding_intCast.specialLinearGroup_map.1

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
i j : Fin 2
⊢ ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod M))) ⟨z, hz_det⟩) i j = ↑1 i j

Tactic:
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.ModularForms.Cusps

Goal state before:
pp: case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0

Tactic:
· simpa [Subgroup.inf_relIndex_left] using h𝒢.2

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

Goal state before:
pp: ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ (∏ i ∈ s, f i) ∣[k * ↑(#s)] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#s) - 1) • ∏ i ∈ s, f i ∣[k] g

Tactic:
have : k * (#s) = ∑ i ∈ s, k := by
    rw [Finset.sum_const, nsmul_eq_mul']

Goal state after:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
this : k * ↑(#s) = ∑ i ∈ s, k
⊢ (∏ i ∈ s, f i) ∣[k * ↑(#s)] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#s) - 1) • ∏ i ∈ s, f i ∣[k] g
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖petersson k (⇑f) (⇑f') x‖) =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
simp_rw [petersson, norm_mul, Complex.norm_conj, mul_comm ‖f _‖ ‖f' _‖, norm_zpow, mul_assoc,
      Complex.norm_real, Real.norm_of_nonneg (fun {τ : ℍ} ↦ τ.im_pos).le]

Goal state after:
case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖f' x‖ * (‖f x‖ * x.im ^ k)) =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
| fun τ ↦ Real.exp (-a * τ.im)

Tactic:
enter [τ]; rw [← one_mul (Real.exp _)]

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
τ : ℍ
| 1 * Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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|
⊢ g • z ∈ 𝒟

Tactic:
have hg₀' : ∀ g' : SL(2, ℤ), (g' • z).im ≤ (g • z).im := by
    have hg'' : (g • z).im = (g₀ • z).im := by
      rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, hg]
    simpa only [hg''] using hg₀

Goal state after:
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 ∈ 𝒟
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        ↑g 1 0 = 0 →
          0 ≤ ↑g 1 1 → (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
specialize this hz (g := -g) (SL_neg_smul g z ▸ hg) (by simpa using hc) ?_

Goal state after:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        ↑g 1 0 = 0 →
          0 ≤ ↑g 1 1 → (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ 0 ≤ ↑(-g) 1 1

case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
⊢ z.re = 1 / 2

Tactic:
linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
⊢ (-↑z).re / 1 = -z.re

Tactic:
div_one,

Goal state after:
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
⊢ (-↑z).re = -z.re
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
x✝ : f.IsCuspForm
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : CuspForm.toModularFormₗ g = f
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑(CuspForm.toModularFormₗ g)) = 0

Tactic:
qExpansion_coeff_zero one_pos
    (ModularFormClass.analyticAt_cuspFunction_zero _ one_pos one_mem_strictPeriods_SL)
    (periodic_comp_ofComplex _ one_mem_strictPeriods_SL)

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
x✝ : f.IsCuspForm
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : CuspForm.toModularFormₗ g = f
⊢ valueAtInfty ⇑(CuspForm.toModularFormₗ g) = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case pos
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : n = -1
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹

pp: case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
· simp [hb, hn, δ_eq_two]
        ring

Goal state after:
case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ logDeriv (η ∘ fun x ↦ -1 / x) ↑z = logDeriv (sqrt * η) ↑z

Tactic:
rw [logDeriv_eta_comp_div_eq z, Pi.mul_def,
      logDeriv_mul _ (by simp [sqrt, ne_zero z]) (eta_ne_zero z.2)
      (differentiableAt_sqrt (mem_slitPlane z))
      (differentiableAt_eta_of_mem_upperHalfPlaneSet z.2), logDeriv_apply sqrt]

Goal state after:
z : ℍ
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = deriv sqrt ↑z / (↑z).sqrt + logDeriv η ↑z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ IsZeroAtImInfty Δ

Tactic:
apply Tendsto.congr (fun z ↦ (discriminant_eq_q_prod z).symm)

Goal state after:
⊢ Tendsto (fun z ↦ 𝕢 1 ↑z * ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Set.EqOn (cuspFunction 1 Δ) (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1)

Tactic:
intro q hq
  by_cases hq0 : q = 0
  · simpa [hq0] using! Periodic.cuspFunction_zero_of_zero_at_inf one_pos
      discriminant_isZeroAtImInfty.zero_at_infty_comp_ofComplex
  · have him := Periodic.im_invQParam_pos_of_norm_lt_one one_pos
      (by simpa [dist_zero_right] using hq) hq0
    simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero 1 _ hq0,
      ofComplex_apply_of_im_pos him, discriminant_eq_q_prod ⟨_, him⟩,
      Periodic.qParam_right_inv one_ne_zero hq0, eta_q]

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

Goal state before:
pp: case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ Submodule.Quotient.mk (E hk) ≠ 0

pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k),
    ∃ c, c • Submodule.Quotient.mk (E hk) = w

Tactic:
· intro h
    have hE := E_qExpansion_coeff_zero hk hk2
    rw [Submodule.Quotient.mk_eq_zero] at h
    exact one_ne_zero <| hE.symm.trans <| (isCuspForm_iff_coeffZero_eq_zero _).mp h

Goal state after:
case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k),
    ∃ c, c • Submodule.Quotient.mk (E hk) = w
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hf
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ ↑ofComplex (↑t * ↑x)) (𝓝[<] 1) (𝓝 x)

Tactic:
refine .mono_left ?_ nhdsWithin_le_nhds

Goal state after:
case hf
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ ↑ofComplex (↑t * ↑x)) (𝓝 1) (𝓝 x)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hf
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ { coe := ↑x + ↑↑t * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)

Tactic:
refine .mono_left ?_ nhdsWithin_le_nhds

Goal state after:
case hf
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ { coe := ↑x + ↑↑t * Complex.I, coe_im_pos := ⋯ }) (𝓝 0) (𝓝 x)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : ¬p ∣ ↑n
⊢ emultiplicity p (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) + emultiplicity p (x - y) = emultiplicity p (x - y)

Tactic:
emultiplicity_eq_zero.2 (not_dvd_geom_sum₂ hp hxy hx hn),

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : ¬p ∣ ↑n
⊢ 0 + emultiplicity p (x - y) = emultiplicity p (x - y)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝¹ i] (A i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, x i ∈ A i
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
have hSA : ∀ i ∈ S, IsCompact (A i) := fun i hi ↦ hi.1

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝¹ i] (A i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, x i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : realMixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target, (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) =
    ∫ (x : realMixedSpace K), f x

Tactic:
rw [← setIntegral_univ (f := f),
    ← setIntegral_congr_set (polarCoordReal_symm_target_ae_eq_univ K),
    integral_image_eq_integral_abs_det_fderiv_smul volume
      (polarCoordReal K).open_target.measurableSet
      (fun x _ ↦ (hasFDerivAt_polarCoordReal_symm K x).hasFDerivWithinAt)
      (polarCoordReal K).symm.injOn f]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : realMixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target, (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) =
    ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      |(FDerivPolarCoordRealSymm K x).det| • f (↑(polarCoordReal K).symm x)
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 : 𝓞 K
⊢ (ringOfIntegersComplexConj K) x = x ↔ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K))

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · rw [RingOfIntegers.ext_iff, coe_ringOfIntegersComplexConj,
      RingOfIntegers.complexConj_eq_self_iff] at h
    obtain ⟨y, hy⟩ := h
    exact ⟨y, RingOfIntegers.ext_iff.mpr hy⟩
  · rintro ⟨y, rfl⟩
    simp

Goal state after: