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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
⊢ False

Tactic:
have hz₁ : t ≠ 0 ∨ χ ≠ 1 := by
    refine h.symm.imp_right (fun h H ↦ ?_)
    simp only [H, one_pow, ne_eq, not_true_eq_false] at h

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
⊢ False
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
⊢ (fun n ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn using by simp_rw [if_neg hn]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑(∏ x ∈ Ico 1 (p / 2).succ, a * ↑x)

Tactic:
prod_mul_distrib,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((∏ x ∈ Ico 1 (p / 2).succ, a) * ∏ x ∈ Ico 1 (p / 2).succ, ↑x)
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ∏ x ∈ Ico 1 (p / 2).succ, (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs

Tactic:
prod_mul_distrib,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (∏ x ∈ Ico 1 (p / 2).succ, if (↑a * ↑x).val ≤ p / 2 then 1 else -1) *
      ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
exact ⟨hb, mt jacobiSym.ne_zero <| Classical.not_not.2 h⟩

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case h
n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B
d : Fin (n + 1)
⊢ (map (castRingHom ℂ) p).natDegree ≤ n

Tactic:
· grind [Polynomial.natDegree_map_le]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ IsCyclic ↥H ↔ DiscreteTopology ↥H

Tactic:
rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]

Goal state after:
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ (∃ g, zpowers g = H) ↔ DiscreteTopology ↥H
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetOne
g : ConjAct (GL n R)
h : GL n R
hh : h ∈ g • Γ
⊢ GeneralLinearGroup.det h = 1

Tactic:
by
    rw [mem_pointwise_smul_iff_inv_smul_mem] at hh
    simpa [ConjAct.smul_def] using HasDetOne.det_eq hh

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, y = 1 + (a₁ * a₂ * M) • k

Tactic:
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

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

Goal state before:
pp: k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
⊢ (f * g) ∣[k1 + k2] A = |↑(Matrix.GeneralLinearGroup.det A)| • (f ∣[k1] A * g ∣[k2] A)

Tactic:
ext1 x

Goal state after:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
⊢ ((f * g) ∣[k1 + k2] A) x = (|↑(Matrix.GeneralLinearGroup.det A)| • (f ∣[k1] A * g ∣[k2] A)) x
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.Commensurable 𝒢.periods

Tactic:
constructor
  · rcases 𝒢.relIndex_strictPeriods with h | h <;> simp [h]
  · simp [AddSubgroup.relIndex_eq_one.mpr 𝒢.strictPeriods_le_periods]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
⊢ (cuspFunction h f ∘ fun τ ↦ 𝕢 h ↑τ) = f

Tactic:
funext τ

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
τ : ℍ
⊢ (cuspFunction h f ∘ fun τ ↦ 𝕢 h ↑τ) τ = f τ
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto ((σ g) (c • 1) • ⇑f ∣[k] g) atImInfty (𝓝 0)

Tactic:
exact (f.zero_at_cusps' hc g hg).smul _

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto ((σ g) (c • 1) • ⇑f ∣[k] g) atImInfty (𝓝 0)

Tactic:
exact (f.zero_at_cusps' hc g hg).smul _

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ f = fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)

Tactic:
funext τ

Goal state after:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
τ : ℍ
⊢ f τ = update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI :
  f (S • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑UpperHalfPlane.I ^
        k *
      f UpperHalfPlane.I
⊢ k = 0 ∨ c = 0

Tactic:
have h2I2 := slash_action_eqn_SL'' f (mem_Gamma_one S) ((⟨2, two_pos⟩ : {x : ℝ // 0 < x}) • .I)

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI :
  f (S • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑UpperHalfPlane.I ^
        k *
      f UpperHalfPlane.I
h2I2 :
  f (S • ⟨2, ⋯⟩ • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S))
          ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^
        k *
      f (⟨2, ⋯⟩ • UpperHalfPlane.I)
⊢ k = 0 ∨ c = 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
⊢ c 0 = cuspFunction h f 0

Tactic:
have := (L1.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE L2).mp <|
      by filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..

Goal state after:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
this : update (cuspFunction h f) 0 (c 0) =ᶠ[𝓝 0] cuspFunction h f
⊢ c 0 = cuspFunction h f 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
b : ℕ
⊢ { x // finGcdMap x = b } ≃ ↑(gammaSet 1 b 0)

Tactic:
apply Equiv.subtypeEquivProp

Goal state after:
N r : ℕ
a : Fin 2 → ZMod N
b : ℕ
⊢ (fun x ↦ finGcdMap x = b) = fun x ↦ x ∈ gammaSet 1 b 0
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, ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)

Tactic:
obtain ⟨C, hC⟩ := petersson_bounded_left k Γ f f

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
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n✝ i : ℕ
hi : i ∈ Finset.range (n✝ + 1)
⊢ (↑n✝.factorial)⁻¹ *
      (↑n✝.factorial / (↑i.factorial * ↑(n✝ - i).factorial) * iteratedDeriv i (cuspFunction h f) 0 *
        iteratedDeriv (n✝ - i) (cuspFunction h g) 0) =
    (↑i.factorial)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n✝ - i).factorial)⁻¹ * iteratedDeriv (n✝ - i) (cuspFunction h g) 0)

Tactic:
field_simp [Nat.factorial_ne_zero]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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 ^ b
hre : (g • z).re = ↑b + z.re
this : |↑b| ≤ 1 / 2 + |z.re|
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
hz.2,

Goal state after:
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 ^ b
hre : (g • z).re = ↑b + z.re
this : |↑b| ≤ 1 / 2 + 1 / 2
⊢ (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: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑(↑g 1 1)| ≤ 1 + |z.re|
⊢ |↑g 1 1| ≤ 1

Tactic:
hz.2,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑(↑g 1 1)| ≤ 1 + 1 / 2
⊢ |↑g 1 1| ≤ 1
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ logDeriv (η ∘ fun x ↦ -x⁻¹) ↑z = (↑z ^ 2)⁻¹ * logDeriv η (-(↑z)⁻¹)

Tactic:
rw [logDeriv_comp, mul_comm]

Goal state after:
z : ℍ
⊢ deriv (fun x ↦ -x⁻¹) ↑z * logDeriv η (-(↑z)⁻¹) = (↑z ^ 2)⁻¹ * logDeriv η (-(↑z)⁻¹)

case hf
z : ℍ
⊢ DifferentiableAt ℂ η (-(↑z)⁻¹)

case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
this : (fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p)) = fun s ↦ cexp (2 * ↑π * I * ↑m / ↑p * s)
⊢ iteratedDeriv k (fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p)) x =
    (fun s ↦ (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m * s / ↑p)) x

Tactic:
simp only [this, iteratedDeriv_cexp_const_mul]

Goal state after:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
this : (fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p)) = fun s ↦ cexp (2 * ↑π * I * ↑m / ↑p * s)
⊢ (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m / ↑p * x) =
    (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m * x / ↑p)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = 1

Tactic:
rcases case_c_one_d_neg_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩

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

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
v : Fin 2 → ℤ
⊢ eisSummand (↑k) v z = ((fun x ↦ eisSummand ↑k ![x.1, x.2] z) ∘ ⇑(finTwoArrowEquiv ℤ)) v

Tactic:
simp [show ![v 0, v 1] = v from List.ofFn_inj.mp rfl]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
this : S • I = I
⊢ g ∈ {1, -1, S, -S} → g • I = I

Tactic:
simp +contextual [-sl_moeb, or_imp, this]

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

Goal state before:
pp: case h
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
⊢ f = 0

Tactic:
have h0 : (qExpansion 1 f).coeff 0 = 0 :=
    PowerSeries.coeff_of_lt_order _ ((Nat.cast_nonneg _).trans_lt h)
  suffices CuspForm.discriminantEquiv (toCuspForm f h0) = 0 by
    simpa [CuspForm.discriminantEquiv.map_eq_zero_iff, DFunLike.ext_iff]
  rcases lt_or_ge k 12 with hk12 | hk12
  · apply rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero (by lia))
  · rw [← mcast_eq_zero_iff (b := ↑(k - 12)) (by lia) rfl]
    refine ih (k - 12) (by lia) ?_
    have hsucc : k / 12 = (k - 12) / 12 + 1 := by lia
    rw [qExpansion_eq_qExpansion_discriminant_mul f h0, PowerSeries.order_mul,
      discriminant_qExpansion_order, add_comm, hsucc, Nat.cast_add, Nat.cast_one] at h
    exact (ENat.add_lt_add_iff_right (ENat.natCast_ne_top 1)).mp h

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

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

Tactic:
simp_rw [this, jacobiTheta_two_add]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
this : (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} → g • ρ = ρ

Tactic:
simp +contextual [-sl_moeb, or_imp, this]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h₂
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.im ≤ y

Tactic:
exact hz.2.1

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
⊢ (valuation K v) ((algebraMap R K) d) < 1

Tactic:
valuation_of_algebraMap

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
⊢ v.intValuation d < 1
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)
S : Set ι
hS : cofinite ≤ 𝓟 S
⊢ IsOpen[topologicalSpace R A (𝓟 S)] {f | ∀ (i : ι), ↑f i ∈ A i}

Tactic:
by
  convert! isOpen_forall_imp_mem_of_principal hAopen hS (p := fun _ ↦ True)
  simp

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

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
hS : S ∈ 𝓕₁
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ T ∈ 𝓕₂

Tactic:
exact inter_mem (hf hS) hφ

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
w : InfinitePlace K
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) w = normAtComplexPlaces (mixedSpaceOfRealSpace x.1) w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) w = normAtComplexPlaces (mixedSpaceOfRealSpace x.1) w

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) w = normAtComplexPlaces (mixedSpaceOfRealSpace x.1) w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
⊢ logMap (c • x) = logMap x

Tactic:
by
  have : mixedEmbedding.norm (c • (1 : mixedSpace K)) ≠ 0 := by
    rw [norm_smul, map_one, mul_one]
    exact pow_ne_zero _ (abs_ne_zero.mpr hc)
  rw [← smul_one_mul, logMap_mul this hx, logMap_real, zero_add]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ mixedSpaceOfRealSpace (normAtComplexPlaces a) ∈ A

Tactic:
← hA,

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ mixedSpaceOfRealSpace (normAtComplexPlaces a) ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
x✝ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
hx₁ : mixedSpaceOfRealSpace x ∈ A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
⊢ x ∈ normAtComplexPlaces '' A

Tactic:
← hA,

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
x✝ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
hx₁ : mixedSpaceOfRealSpace x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
⊢ x ∈ normAtComplexPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
rw [Set.mem_ofPred_eq, mixedEmbedding.norm_smul, mul_eq_zero, not_or]

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ ¬|c| ^ Module.finrank ℚ K = 0 ∧ ¬mixedEmbedding.norm x = 0
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
⊢ σ = τ

Tactic:
have : Nat.card (K ≃ₐ[K⁺] K) = 2 :=
    (IsQuadraticExtension.finrank_eq_two K⁺ K) ▸ IsGalois.card_aut_eq_finrank K⁺ K

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : Nat.card Gal(K/↥K⁺) = 2
⊢ σ = τ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ ∃ u, u • x ∈ fundamentalCone K

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := ⋯
⊢ ∃ e, ↑e + logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
· exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := ⋯
⊢ ∃ e, ↑e + logMap x ∈ ZSpan.fundamentalDomain B