mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inl
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
ha : 1 ≤ 1
⊢ DiscreteTopology ↥(zpowers 1)

Tactic:
zpowers_one_eq_bot

Goal state after:
case inl
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
ha : 1 ≤ 1
⊢ DiscreteTopology ↥⊥
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)
⊢ y.map Int.cast = 1

Tactic:
rw [CongruenceSubgroup.Gamma_mem', Subtype.ext_iff] at hy'

Goal state after:
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' : ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod (a₁ * a₂ * M)))) ⟨y, hy⟩) = ↑1
⊢ y.map Int.cast = 1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN✝ : M ≠ 0
hΓM : Γ(M) ≤ Γ
x✝ : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) Γ(M)
⊢ IsCongruenceSubgroup (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))

Tactic:
refine ⟨N, ‹_›, fun x hx ↦ ?_⟩

Goal state after:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN✝ : M ≠ 0
hΓM : Γ(M) ≤ Γ
x✝ : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) Γ(M)
x : SL(2, ℤ)
hx : x ∈ Γ(N)
⊢ x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsZeroAt f k ↔ ∀ (γ : SL(2, ℤ)), (mapGL ℝ) γ • ∞ = c → IsZeroAtImInfty (f ∣[k] γ)

Tactic:
by
  refine ⟨fun hc _ hγ ↦ by simpa using! hc _ hγ, fun h ↦ ?_⟩
  obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
  simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using! h γ rfl

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a ≈ b
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧

Tactic:
rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hab
      refine Quotient.eq.mpr ⟨⟨_, hab⟩, ?_⟩
      simp [mul_smul]

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
⊢ (map (mapGL ℝ) Γ).strictWidthInfty = 1

Tactic:
have hsp := strictPeriods_eq_zmultiples_one_of_T_mem hΓ

Goal state after:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : (map (mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1
⊢ (map (mapGL ℝ) Γ).strictWidthInfty = 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_3.«0».«1»
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
convert! congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1
    simp only [Fin.zero_eta, Function.comp_apply, lcRow0Extend_apply, cons_val_zero,
      LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
      mulVecLin_apply, mulVec, dotProduct, det_fin_two, f₁]
    simp only [Fin.isValue, Fin.mk_one, val_planeConformalMatrix, neg_neg, of_apply, cons_val',
      empty_val', cons_val_fin_one, cons_val_one, map_apply, Fin.sum_univ_two,
      cons_val_zero, neg_mul, Int.cast_sub, Int.cast_mul, neg_sub]
    ring

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

Goal state before:
pp: case inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k < 0
f : F
hf : ⇑f = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0)
hf₀ : UpperHalfPlane.cuspFunction 1 (⇑f) 0 = 0
⊢ Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0) = 0

Tactic:
hf₀,

Goal state after:
case inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k < 0
f : F
hf : ⇑f = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0)
hf₀ : UpperHalfPlane.cuspFunction 1 (⇑f) 0 = 0
⊢ Function.const ℍ 0 = 0
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
C : ℝ
| ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
τ,

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
C : ℝ
τ : ℍ
| ‖petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
C : ℝ
| ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C

Tactic:
τ,

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
C : ℝ
τ : ℍ
| ‖petersson k (⇑f) (⇑f') τ‖ ≤ C
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ C / (τ.im ^ (↑k / 2)) ^ 2

Tactic:
← hC

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ ‖petersson k (⇑f) (⇑f) τ‖ / (τ.im ^ (↑k / 2)) ^ 2
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ Tendsto (fun N ↦ Ioc (-N) N) atTop atTop

Tactic:
exact tendsto_Ioc_neg_atTop_atTop

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hre
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
⊢ z.re = ρ.re

pp: case hnorm
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
⊢ ‖↑z‖ = ‖↑ρ‖

Tactic:
· simp [hre, ρ]

Goal state after:
case hnorm
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
⊢ ‖↑z‖ = ‖↑ρ‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ G2 z = (↑z ^ 2)⁻¹ * G2 (S • z) - -2 * ↑π * I / ↑z

Tactic:
rw [G2_S_action_eq_tsum_G2Term, G2_eq_tsum_G2Term z, ← tsum_G2Term_eq_tsum',
  tsum_G2Term_eq_tsum]

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

Goal state before:
pp: ⊢ Set.EqOn (logDeriv (η ∘ fun z ↦ -1 / z)) (logDeriv (sqrt * η)) upperHalfPlaneSet

pp: case hf
⊢ DifferentiableOn ℂ (η ∘ fun z ↦ -1 / z) upperHalfPlaneSet

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 z hz ↦ logDeriv_eta_comp_eq_logDeriv_csqrt_eta ⟨z, hz⟩

Goal state after:
case hf
⊢ DifferentiableOn ℂ (η ∘ fun z ↦ -1 / z) upperHalfPlaneSet

case hg
⊢ DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet

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: z : ℍ
this : η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
⊢ (Δ ∣[12] ModularGroup.S) z = Δ z

Tactic:
rw [SL_slash_apply, UpperHalfPlane.modular_S_smul]
    simpa [denom, ModularGroup.S]

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

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
γ : SL(2, ℤ)
hγ :
  Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) ∈
    (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ (fun z ↦ f z / Δ z) ∣[k - 12] γ = fun z ↦ f z / Δ z

Tactic:
change (⇑f / ⇑CuspForm.discriminant) ∣[k - 12] γ = ⇑f / ⇑CuspForm.discriminant

Goal state after:
k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
γ : SL(2, ℤ)
hγ :
  Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) ∈
    (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ (⇑f / ⇑discriminant) ∣[k - 12] γ = ⇑f / ⇑discriminant
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z

Tactic:
← iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow hk (by simpa using z.2)

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ ↑z =
    iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z
Module: Mathlib.NumberTheory.Modular

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

Tactic:
rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz him.le hc) with hd | hd | hd

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

case inr.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

case inr.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ
n : ℤ
hn : n ∈ Ico (-↑N) ↑N
⊢ ∀ (b : ℤ), (↑z ^ 2)⁻¹ * ((-(↑n * (↑z)⁻¹) + ↑(-b)) ^ 2)⁻¹ = ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
grind [zpow_two, ne_zero z]

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

Goal state before:
pp: case inr
k : ℤ
hk_nonneg : 0 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
rcases Int.even_or_odd k with hk_even | hk_odd

Goal state after:
case inr.inl
k : ℤ
hk_nonneg : 0 ≤ k
hk_even : Even k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
this : ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ

Tactic:
by simp_rw [this, jacobiTheta_two_add]

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ (E hk) z =
    1 +
      (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n

Tactic:
by
  rw [show E hk z = (1 / 2 : ℂ) • eisensteinSeriesSIF (N := 1) 0 k z from rfl,
    eisensteinSeriesSIF_apply 0 k z, eisensteinSeries]
  have HE1 := tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow hk hk2 z
  have HE2 := tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries hk z
  have z2 : riemannZeta k ≠ 0 := riemannZeta_ne_zero_of_one_lt_re <| by norm_cast; grind
  simp [eisSummand, eisensteinSeries, ← inv_mul_eq_iff_eq_mul₀ z2] at HE1 HE2 ⊢
  grind

Goal state after:
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
    simpa [show 𝓝 (x : ℂ) = 𝓝 (x + (((0 : ℝ≥0) : ℝ) : ℂ) * Complex.I) by simp,
      isOpenEmbedding_coe.tendsto_nhds_iff] using! Continuous.tendsto (by fun_prop) _

Goal state after:
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)
x : (i : ι) → ↑(A i)
⊢ 𝓝 (structureMap R A cofinite x) = Filter.map (structureMap R A cofinite) (𝓝 x)

Tactic:
by
  rw [isOpenEmbedding_structureMap hAopen |>.map_nhds_eq x]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ = 1
⊢ ζ = 1

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ * ↑(preimageOfMemIntegerSet a) = ↑(preimageOfMemIntegerSet a)
⊢ ↑(preimageOfMemIntegerSet a) ≠ 0

Tactic:
Units.val_eq_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑ζ = 1
⊢ ζ = 1

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ * ↑(preimageOfMemIntegerSet a) = ↑(preimageOfMemIntegerSet a)
⊢ ↑(preimageOfMemIntegerSet a) ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hy₁ : mixedSpaceOfRealSpace (normAtAllPlaces y) ∈ normLeOne K
hy₂ : normAtAllPlaces y = normAtAllPlaces x
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ normLeOne K

Tactic:
← hy₂

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hy₁ : mixedSpaceOfRealSpace (normAtAllPlaces y) ∈ normLeOne K
hy₂ : normAtAllPlaces y = normAtAllPlaces x
⊢ mixedSpaceOfRealSpace (normAtAllPlaces y) ∈ normLeOne K
Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
x : K
⊢ (algebraMap K w.Completion) x = (algebraMap v.Completion w.Completion) ((algebraMap K v.Completion) x)

Tactic:
by
    have h : algebraMap K v.Completion x = ((WithAbs.toAbs v.1 x : WithAbs v.1) : v.Completion) :=
      rfl
    rw [RingHom.algebraMap_toAlgebra, h, completionMap_coe]
    apply Completion.ext
    rw [Completion.algebraMap_toCompletion, UniformSpace.Completion.algebraMap_def]
    simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply]

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

Goal state before:
pp: case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : ↑(E ⊔ maximalRealSubfield K) = ↑⊥
⊢ ↑⊥ = ↑E

Tactic:
IntermediateField.coe_bot

Goal state after:
case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : ↑(E ⊔ maximalRealSubfield K) = ↑⊥
⊢ Set.range ⇑(algebraMap (↥E) K) = ↑E
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ regulator K = regOfFamily (fundSystem K)

Tactic:
classical
  rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]

Goal state after:
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₀
⊢ (∑ x_1,
          (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun a ↦
            (x ↑x_1 • (completeBasis K) ↑x_1) ↑a)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
Pi.smul_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1,
          (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun a ↦
            x ↑x_1 • (completeBasis K) ↑x_1 ↑a)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
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₀
⊢ ∑ c,
        (x ↑c •
            ⇑((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦
                ↑((basisUnitLattice K) (equivFinRank.symm c)) i))
          (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
Pi.smul_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ∑ x_1,
        x ↑x_1 •
          ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦
              ↑((basisUnitLattice K) (equivFinRank.symm x_1)) i)
            (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ multiplicity (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩))
      (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p})) =
    multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
apply multiplicity_eq_of_emultiplicity_eq

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ emultiplicity (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩))
      (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p})) =
    emultiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case neg
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
this : (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K) = 0

Tactic:
rwa [← mul_eq_zero_iff_right this, Subgroup.relIndex_mul_index h,
      ← Subgroup.not_finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex,
      ← isMaxRank_iff_closure_finiteIndex.not]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : IsGalois ℚ K
⊢ IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))

Tactic:
refine IsGalois.of_equiv_equiv (f := (FractionRing.algEquiv ℤ ℚ).toRingEquiv.symm)
      (g := (FractionRing.algEquiv (𝓞 K) K).toRingEquiv.symm) <|
        RingHom.ext fun x ↦ IsFractionRing.algEquiv_commutes (FractionRing.algEquiv ℤ ℚ).symm
          (FractionRing.algEquiv (𝓞 K) K).symm _

Goal state after: