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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑↑a * ↑x).val}) = (-1) ^ ((∑ x ∈ Ico 1 (p / 2).succ, x * a / p) % 2)

Tactic:
neg_one_pow_eq_pow_mod_two,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ (-1) ^ (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑↑a * ↑x).val}) % 2) = (-1) ^ ((∑ x ∈ Ico 1 (p / 2).succ, x * a / p) % 2)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
rw [hb, zero_right]
    exact one_ne_zero

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

Goal state before:
pp: case succ
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
ih : Finite ((↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1)) ⧸ Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1))

Tactic:
suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
      .of_ideal_quotient (.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))

Goal state after:
case succ
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
ih : Finite ((↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1)) ⧸ Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))
⊢ Finite ↥(Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
⊢ fastJacobiSymAux a b flip ha0 = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
induction a using Nat.strongRecOn generalizing b flip with

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ x * y * a * y = y * x * a * y

Tactic:
rw [hx1]

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (x * a) * y = y * (a * x) * y

Tactic:
rw [hx1]

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

Goal state before:
pp: case refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : CompactSpace ↥𝒪[K]
⊢ CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]

Tactic:
have : IsDiscreteValuationRing 𝒪[K] := isDiscreteValuationRing_of_compactSpace
    refine ⟨complete_of_compact, by assumption, ?_⟩
    rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete,
        totallyBounded_iff_finite_residueField] at h
    exact h.left

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
by
  dsimp [lucasLehmerResidue]
  rw [sZMod_eq_sMod p]
  constructor
  · -- We want to use that fact that `0 ≤ s_mod p (p-2) < 2^p - 1`
    -- and `lucas_lehmer_residue p = 0 → 2^p - 1 ∣ s_mod p (p-2)`.
    intro h
    apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _
      (by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h) <;> clear h
    · exact sMod_nonneg _ (by positivity) _
    · exact sMod_lt _ (by positivity) _
  · intro h
    rw [h]
    simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p : ℕ
hp : 2 ≤ p
n✝ : ℕ
a✝ : ↑(sModNat (2 ^ p - 1) n✝) = sMod p n✝
⊢ ↑(sModNat (2 ^ p - 1) (n✝ + 1)) = sMod p (n✝ + 1)

Tactic:
have : 2 ^ 2 ≤ 2 ^ p := Nat.pow_le_pow_right (by lia) hp

Goal state after:
case succ
p : ℕ
hp : 2 ≤ p
n✝ : ℕ
a✝ : ↑(sModNat (2 ^ p - 1) n✝) = sMod p n✝
this : 2 ^ 2 ≤ 2 ^ p
⊢ ↑(sModNat (2 ^ p - 1) (n✝ + 1)) = sMod p (n✝ + 1)
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
simp [𝒢.relindex_adjoinNegOne_eq_two hG]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ∞ = ↑c

Tactic:
refine ⟨fun hg ↦ (g.det_ne_zero ?_).elim, fun hg ↦ (infty_ne_coe _ hg).elim⟩

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ↑g 1 0 * c + ↑g 1 1 = 0
hg : ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0
⊢ (↑g).det = 0
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
⊢ f (h +ᵥ τ) = f τ

Tactic:
by
  rw [← congr_fun (slash_action_eqn f _ <| Γ.mem_strictPeriods_iff.mp hH) τ]
  suffices GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ by
    simp_rw [slash_def, this]
    simp [σ, denom, GeneralLinearGroup.val_det_apply, denom]
  ext
  simp [σ, num, denom, coe_vadd, UpperHalfPlane.coe_smul, num, add_comm]

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.periods.relIndex 𝒢.strictPeriods ≠ 0

Tactic:
· 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
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)

Tactic:
have := ((differentiableOn_cuspFunction_ball hh hfper hfhol hfbdd).mono
    (Metric.closedBall_subset_ball hR')).circleIntegral_one_div_sub_center_pow_smul hR n

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  ∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z =
    (2 * ↑π * Complex.I / ↑n.factorial) • iteratedDeriv n (cuspFunction h f) 0
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 0
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
have had := g.det_coe

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : (↑g).det = 1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

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

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
⊢ ⇑f = 0

Tactic:
· exact (lt_irrefl _ hk).elim

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
⊢ ⇑f = 0
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case ha
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 τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ 0 ≤ F

pp: case h₁
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 τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ (g • τ).im ≤ max τ.im (1 / τ.im)

Tactic:
· rw [← div_le_iff₀ (by positivity)] at hF𝒟
    exact le_trans (by positivity) hF𝒟

Goal state after:
case h₁
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 τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ (g • τ).im ≤ max τ.im (1 / τ.im)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
γ : SL(2, ℤ)
v : ↑(gammaSet N r (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))
this :
  ↑v ᵥ* ↑γ⁻¹ ∈
    gammaSet N r
      (a ᵥ*
        ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ *
            (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ⁻¹))
⊢ ↑v ᵥ* ↑γ⁻¹ ∈ gammaSet N r a

Tactic:
simpa only [SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom,
        map_inv, mul_inv_cancel, SpecialLinearGroup.coe_one, vecMul_one]

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
rw [abs_le]

Goal state after:
case right
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ -(1 / 2) ≤ (g • z).re ∧ (g • z).re ≤ 1 / 2
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') τ‖

Tactic:
← norm_norm

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') τ‖‖
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') τ‖

Tactic:
← norm_norm

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') τ‖‖
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: x : ↥(divisorsAntidiagonal 1)
h : (↑x).1 * (↑x).2 = 1 ∧ 1 ≠ 0
⊢ divisorsAntidiagonalFactors 1 x = (1, 1)

Tactic:
simp only [mul_eq_one, ne_eq, one_ne_zero, not_false_eq_true, and_true] at h

Goal state after:
x : ↥(divisorsAntidiagonal 1)
h : (↑x).1 = 1 ∧ (↑x).2 = 1
⊢ divisorsAntidiagonalFactors 1 x = (1, 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case e_f
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
a : ℤ
⊢ ∑' (n : ℤ), eisSummand 2 ![a, n] z =
    ∑' (b : ℤ), (G2Term z ![(a, b).1, (a, b).2] + (1 / (↑a * ↑z + ↑b) - 1 / (↑a * ↑z + ↑b + 1)))

Tactic:
exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat])

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

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ D (F - G) z = (D F - D G) z

Tactic:
simp only [normalizedDerivOfComplex, Pi.sub_apply]

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv ((F - G) ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z - (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
⊢ ↑g 1 0 = 0 ∨ ↑g 1 0 = 1

Tactic:
grind [abs_c_le_one hz hg]

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

Goal state before:
pp: case hf.hg
⊢ DifferentiableOn ℂ η upperHalfPlaneSet

Tactic:
exact fun x hx ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hx).differentiableWithinAt

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

Goal state before:
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:
· apply DifferentiableOn.comp (t := upperHalfPlaneSet)
    · exact fun x hx ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hx).differentiableWithinAt
    · exact DifferentiableOn.div (by fun_prop) (by fun_prop)
        (fun x hx ↦ ne_zero (⟨x, hx⟩ : ℍ))
    · exact fun y hy ↦ by grind [im_pnat_div_pos 1 (⟨y, hy⟩ : ℍ)]

Goal state after:
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.LevelOne.DimensionFormula

Goal state before:
pp: f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
⊢ qExpansion 1 ⇑f = 0

Tactic:
by
  obtain ⟨c4, hc4⟩ : ∃ c4, c4 • E₄ = f.mul f :=
    (finrank_eq_one_iff_of_nonzero' E₄ (E_ne_zero _ ⟨2, rfl⟩)).mp
      (Module.rank_eq_one_iff_finrank_eq_one.mp levelOne_weight_four_rank_one) _
  obtain ⟨c6, hc6⟩ : ∃ c6, c6 • E₆ = (f.mul f).mul f :=
    (finrank_eq_one_iff_of_nonzero' E₆ (E_ne_zero _ ⟨3, rfl⟩)).mp
      (Module.rank_eq_one_iff_finrank_eq_one.mp levelOne_weight_six_rank_one) _
  have hqc4 : c4 • qExpansion 1 (E₄ : ℍ → ℂ) = qExpansion 1 (f : ℍ → ℂ) ^ 2 := by
    rw [pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
      show (c4 • E₄ : ℍ → ℂ) = (f.mul f) from congrArg DFunLike.coe hc4]
  have hqc6 : c6 • qExpansion 1 E₆ = qExpansion 1 (f : ℍ → ℂ) ^ 3 := by
    rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
      show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
  exact eq_zero_of_pow_eq_smul (E_qExpansion_coeff_zero _ ⟨2, rfl⟩)
    (E_qExpansion_coeff_zero _ ⟨3, rfl⟩) E₄_qExpansion_coeff_one E₆_qExpansion_coeff_one hqc4 hqc6

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
⊢ ↑g 1 0 = 0 ∨ ↑g 1 0 = 1

Tactic:
grind [abs_c_le_one hz hg]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ+
h2 :
  ↑π * I -
        2 * ↑π * I *
          (cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ 0 +
            ∑' (n : ℕ+), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ ↑n) -
      ↑z / -↑↑N =
    ↑π * I -
        2 * ↑π * I *
          (cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ 0 +
            ∑' (n : ℕ+), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ ↑n) -
      ↑z / -↑↑N
⊢ 2 / ↑z *
        (↑π * I -
            2 * ↑π * I *
              (cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ 0 +
                ∑' (n : ℕ+), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ ↑n) -
          ↑z / -↑↑N) -
      (-(2 * ↑π) * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N

Tactic:
field [ne_zero z]

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z
⊢ 1 < (↑k).re

Tactic:
by norm_cast; grind

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
this : (E hk) τ = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n
⊢ (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)

Tactic:
rw [this, ← tsum_pnat_eq_tsum_succ (f := fun n ↦ (σ (k - 1) n : ℂ) * cexp (2 * π * I * τ) ^ n)]

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
this : (E hk) τ = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n
⊢ 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n - 1 =
    β * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : SlashInvariantFormClass F 𝒢 k
inst✝ : 𝒢.IsFiniteRelIndex ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ (let this := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
      ∑ q, quotientFunc f q) ∣[k]
      h =
    let this := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
    ∑ q, quotientFunc f q

Tactic:
let := Fintype.ofFinite 𝒬
    simpa [SlashAction.sum_slash, quotientFunc_smul f hh]
      using Equiv.sum_comp (MulAction.toPerm (_ : ℋ)) _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K∞
hx : ¬IsUnit x
⊢ ‖x‖ = 0

Tactic:
by
  rw [Pi.isUnit_iff, not_forall] at hx
  obtain ⟨v, hv⟩ := hx
  exact Finset.prod_eq_zero_iff.2 ⟨v, Finset.mem_univ v, by simpa [isUnit_iff_ne_zero] using hv⟩

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Continuous fun x ↦ (fun w ↦ if hw : w.IsReal then x.1 ⟨w, hw⟩ else (x.2 ⟨w, ⋯⟩).1, fun w ↦ (x.2 w).2)

Tactic:
refine .prodMk (continuous_pi fun w ↦ ?_) (by fun_prop)

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ Continuous fun a ↦ if hw : w.IsReal then a.1 ⟨w, hw⟩ else (a.2 ⟨w, ⋯⟩).1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : realMixedSpace K
w : { w // w.IsReal }
⊢ ((homeoRealMixedSpacePolarSpace K) x).1 ↑w = x.1 w

Tactic:
simp_rw [homeoRealMixedSpacePolarSpace_apply, dif_pos w.prop]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ Units.rank ↥K⁺ = Units.rank K

Tactic:
by
  rw [Units.rank, Units.rank, card_infinitePlace_eq_card_infinitePlace K]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ (∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b) ↔ ∃ ζ, ↑ζ • ↑a = ↑b

Tactic:
refine ⟨fun ⟨u, h⟩ ↦  ⟨⟨unitsNonZeroDivisorsEquiv u, ?_⟩, by simpa using h⟩,
    fun ⟨⟨u, _⟩, h⟩ ↦ ⟨unitsNonZeroDivisorsEquiv.symm u, by simpa using h⟩⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
u : (↥(𝓞 K)⁰)ˣ
h : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
⊢ unitsNonZeroDivisorsEquiv u ∈ torsion K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
⊢ { a // ↑(preimageOfMemIntegerSet ↑a) ∈ ↑J } ≃ { I // ↑J ∣ ↑↑I.1 }

Tactic:
convert! Equiv.subtypeEquivOfSubtype (p := fun I ↦ J.1 ∣ I.1) (integerSetEquivNorm K n)
      rw [integerSetEquivNorm_apply_fst, dvd_span_singleton]

Goal state after: