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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
rcases isEmpty_or_nonempty ι
  · simp
  rcases isEmpty_or_nonempty ι'
  · simp
  refine ciSup_le fun j ↦ ?_
  grw [hv.apply_sum_le]
  simp only [map_mul]
  have (f : ι → ℝ) : ⨆ i : ↥Finset.univ, f i.val = ⨆ i, f i :=
    Function.Surjective.iSup_comp (fun i ↦ ⟨⟨i, Finset.mem_univ i⟩, rfl⟩) f
  rw [this fun i ↦ v (A (j, i)) * v (x i)]
  refine ciSup_le fun i ↦ ?_
  gcongr
  · exact Real.iSup_nonneg_of_nonnegHomClass v _
  · exact Finite.le_ciSup_of_le (j, i) le_rfl
  · exact Finite.le_ciSup_of_le i le_rfl

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ Tendsto (fun N ↦ -↑(harmonic (N + 1)) + log (↑N + 1) + 1) atTop (𝓝 (-γ + 1))

Tactic:
refine Tendsto.add ?_ tendsto_const_nhds

Goal state after:
⊢ Tendsto (fun N ↦ -↑(harmonic (N + 1)) + log (↑N + 1)) atTop (𝓝 (-γ))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : Tendsto (fun x ↦ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ (-if n + 1 = 0 then 2 else ↑(harmonic (n + 1)) - log ↑(n + 1)) = -↑(harmonic (n + 1)) + log (↑n + 1)

Tactic:
reduceCtorEq,

Goal state after:
this : Tendsto (fun x ↦ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ (-if False then 2 else ↑(harmonic (n + 1)) - log ↑(n + 1)) = -↑(harmonic (n + 1)) + log (↑n + 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ x / x / x ^ s - ↑n / (x * x ^ s) = x ^ (-s) - ↑n * x ^ (-(s + 1))

Tactic:
div_self (hv x hx).ne',

Goal state after:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 1 / x ^ s - ↑n / (x * x ^ s) = x ^ (-s) - ↑n * x ^ (-(s + 1))
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod ≤
    (map (fun i ↦ ↑(Nat.card ι) * ((⨆ i_1, i (x i_1)) * ⨆ i_1, i (A i_1))) archAbsVal).prod

Tactic:
refine prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _) fun v _ ↦ ?_

Goal state after:
case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
⊢ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1) ≤ ↑(Nat.card ι) * ((⨆ i, v (x i)) * ⨆ i, v (A i))
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type := ⋯
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯
this : NumberField K
⊢ FermatLastTheoremForThreeGen hζ

Tactic:
intro a b c u hc ha hb hcdvd coprime H

Goal state after:
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b c : NumberField.RingOfIntegers K
u : (NumberField.RingOfIntegers K)ˣ
hc : c ≠ 0
ha : ¬hζ.toInteger - 1 ∣ a
hb : ¬hζ.toInteger - 1 ∣ b
hcdvd : hζ.toInteger - 1 ∣ c
coprime : IsCoprime a b
H : a ^ 3 + b ^ 3 = ↑u * c ^ 3
⊢ False
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ ∑ i ∈ s, v (x i) ≤ ∑ _x ∈ s, ∏ i ∈ s, max (v (x i)) 1

Tactic:
gcongr with i hi

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
i : ι
hi : i ∈ s
⊢ v (x i) ≤ ∏ i ∈ s, max (v (x i)) 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inl.inr
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
h : (fun j ↦ constantCoeff (p j)) ≠ 0
⊢ (mulHeight fun j ↦ (eval 0) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight 0 ^ N

Tactic:
· simpa using le_max_of_le_left <| mulHeight_constantCoeff_le_mulHeightBound h

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / (1 - 1)
⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1

Tactic:
rw [sub_self, div_zero, div_one, sub_zero, eq_sub_iff_add_eq] at this

Goal state after:
this : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1
⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous 1

Tactic:
simp [p, isHomogeneous_X, IsHomogeneous.add]

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous 1

Tactic:
simp [p, isHomogeneous_X, IsHomogeneous.add]

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨2, ⋯⟩)).IsHomogeneous 1

Tactic:
simp [p, isHomogeneous_X, IsHomogeneous.add]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case left
⊢ DifferentiableOn ℂ riemannZeta₀ {1}ᶜ

Tactic:
refine .congr (f := fun s ↦ riemannZeta s - (s - 1)⁻¹) ?_ (by simp +contextual [riemannZeta₀])

Goal state after:
case left
⊢ DifferentiableOn ℂ (fun s ↦ riemannZeta s - (s - 1)⁻¹) {1}ᶜ
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (fun s ↦ (riemannZeta s)⁻¹ - (s - 1)) =o[𝓝[≠] 1] fun x ↦ x - 1

Tactic:
apply inv_riemannZeta_sub_sub_isBigO.trans_isLittleO

Goal state after:
⊢ (fun s ↦ (s - 1) ^ 2) =o[𝓝[≠] 1] fun x ↦ x - 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
i : ι
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
hf : 1 ≤ v ↑(x i)
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
exact le_antisymm (ciSup_le (H <| x ·)) <| Finite.le_ciSup_of_le i hf

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

Goal state before:
pp: case base
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n : ℕ
hn₂ : Nat.succ 0 < orderOf χ
⊢ gaussSum χ ψ ^ Nat.succ 0 = gaussSum (χ ^ Nat.succ 0) ψ * ∏ j ∈ Ico 1 (Nat.succ 0), jacobiSum χ (χ ^ j)

Tactic:
simp only [pow_one, le_refl, Ico_eq_empty_of_le, prod_empty, mul_one]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst✝¹ : Module.Finite R S
inst✝ : Free R S
α : S
hα : Function.Surjective ⇑(aeval α)
monic : (minpoly R α).Monic
this✝ : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
φ : AdjoinRoot (minpoly R α) →ₐ[R] S := AdjoinRoot.liftAlgHom (minpoly R α) (Algebra.ofId R S) α ⋯
s : S
p : R[X]
hp : (aeval α) p = s
⊢ φ.toLinearMap ((AdjoinRoot.mk (minpoly R α)) p) = s

Tactic:
by simp [φ, ← aeval_def, hp]

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

Goal state before:
pp: case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this : ↑(toCircle ↑(↑j.val * ↑n)) = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N))
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s

Tactic:
rw [← this, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_zmod_val]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun k 0 = ↑(bernoulli k)

Tactic:
by
  rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ 1 - s ≠ 0

Tactic:
sub_ne_zero,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ 1 ≠ s
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖LSeries (fun x ↦ 1 ↑x) (1 + ↑x) ^ 3 * LSeries (fun x ↦ χ ↑x) (1 + ↑x + I * ↑y) ^ 4 *
        LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
(χ ^ 2).LFunction_eq_LSeries h₂

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖LSeries (fun x ↦ 1 ↑x) (1 + ↑x) ^ 3 * LSeries (fun x ↦ χ ↑x) (1 + ↑x + I * ↑y) ^ 4 *
        LSeries (fun x ↦ (χ ^ 2) ↑x) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Module: Mathlib.NumberTheory.LSeries.ZetaZeros

Goal state before:
pp: ⊢ IsDiscrete riemannZetaZeros

Tactic:
simpa using (mem_codiscrete'.mp compl_riemannZetaZeros_mem_codiscrete).2

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

Goal state before:
pp: case inr.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑b | a') = J(↑(b % (4 * a)) % ↑a' | a')

Tactic:
mod_left b,

Goal state after:
case inr.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑b % ↑a' | a') = J(↑(b % (4 * a)) % ↑a' | a')
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries (fun n ↦ ↑(f n)) ↑s) (𝓝[>] 1) (𝓝 ↑l)

Tactic:
refine LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div (f := fun n ↦ f n)
    (hf.ofReal.congr fun _ ↦ ?_) fun s hs ↦ ?_
  · simp
  · refine LSeriesSummable_of_sum_norm_bigO_and_nonneg ?_ hf' zero_le_one hs
    exact isBigO_atTop_natCast_rpow_of_tendsto_div_rpow (by simpa)

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

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

Tactic:
by
    simp only [subgroupOfEquivOfLe, Topology.IsInducing.subtypeVal.isOpen_iff,
      exists_exists_and_eq_and]
    simpa [Set.ext_iff] using fun s ↦ exists_congr
      fun t ↦ and_congr_right fun _ ↦ ⟨fun aux g hgh ↦ aux g (hHK hgh) hgh, by grind⟩

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
inst✝ : DiscreteTopology G
⊢ IsCyclic G

Tactic:
nontriviality G
  exact LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered.mpr fun h ↦
    have := h.subsingleton_of_discreteTopology; false_of_nontrivial_of_subsingleton G

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

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
⊢ (fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯)
      ((fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p) (mk K w hw)) =
    mk K w hw

Tactic:
| h w hw =>

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

Goal state before:
pp: c : OnePoint ℝ
g : SL(2, ℤ)
hgp : ((mapGL ℝ) g).IsParabolic
hgc : (mapGL ℝ) g • c = c
⊢ OnePoint.map Rat.cast ((mapGL ℚ) g).parabolicFixedPoint = ((mapGL ℝ) g).parabolicFixedPoint

Tactic:
simp [GeneralLinearGroup.parabolicFixedPoint, apply_ite]

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

Goal state before:
pp: case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map Rat.cast ((mapGL ℚ) a • ∞) =
    OnePoint.map Rat.cast ((mapGL ℚ) a • ∞)

Tactic:
· rw [← Rat.coe_castHom, ← (Rat.castHom ℝ).algebraMap_toAlgebra]
      simp [OnePoint.map_smul, mul_smul, smul_infty_eq_self_iff, ModularGroup.T]

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
have : f (γ • z) = f z * denom γ z ^ k := by
    simpa [slash_def, σ, mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ (denom_ne_zero _ _)),
      Subgroup.HasDetOne.det_eq hγ] using congr_fun (slash_action_eqn f γ hγ) z
  rw [this, denom, mul_comm]

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : j ∈ toConjAct g⁻¹ • Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g

Tactic:
rw [map_inv, Γ.mem_inv_pointwise_smul_iff, toConjAct_smul] at hj

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : g * j * g⁻¹ ∈ Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: ⊢ (mapGL ℝ).range.strictWidthInfty = 1

Tactic:
simpa [MonoidHom.range_eq_map] using strictWidthInfty_eq_one_of_T_mem (mem_top _)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ n = 0

Tactic:
suffices |(n : ℝ)| < 1 by
    rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this
  have h₁ := hz.2
  have h₂ := hg.2
  rw [re_T_zpow_smul] at h₂
  calc
    |(n : ℝ)| ≤ |z.re| + |z.re + (n : ℝ)| := abs_add' (n : ℝ) z.re
    _ < 1 / 2 + 1 / 2 := add_lt_add h₁ h₂
    _ = 1 := add_halves 1

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
⊢ ‖(⇑{ toFun := eisensteinSeries a k, slash_action_eq' := ⋯ } ∣[k] A) z‖ ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
SlashInvariantForm.coe_mk,

Goal state after:
N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
⊢ ‖(eisensteinSeries a k ∣[k] A) z‖ ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)
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| - |z.re| ≤ 1 / 2
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
grw [sub_le_iff_le_add, hz.2, add_halves, ← Int.cast_abs, ← Int.cast_one, Int.cast_le,
    Int.abs_le_one_iff] at this

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 = 0 ∨ b = 1 ∨ b = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ∑ i ∈ (↑b).divisors, ‖↑(↑b / i)‖ ^ k * ‖r‖ ^ (i * (↑b / i)) ≤ ∑ x ∈ (↑b).divisors, ‖↑↑b‖ ^ k * ‖r ^ ↑b‖

Tactic:
gcongr with i hi

Goal state after:
case hab
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
i : ℕ
hi : i ∈ (↑b).divisors
⊢ ‖↑(↑b / i)‖ ≤ ‖↑↑b‖

case h₂
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
i : ℕ
hi : i ∈ (↑b).divisors
⊢ ‖r‖ ^ (i * (↑b / i)) ≤ ‖r ^ ↑b‖
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ c.IsZeroAt (⇑f) k

Tactic:
by
  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
  rw [isZeroAt_iff_forall_SL2Z hc]
  intro γ _
  rw [show (⇑f ∣[k] γ) = ⇑f from f.slash_action_eq' _ ⟨γ, rfl⟩]
  exact isZeroAtImInfty_of_valueAtInfty_eq_zero f <| by
    rwa [← qExpansion_coeff_zero one_pos
      (ModularFormClass.analyticAt_cuspFunction_zero f one_pos one_mem_strictPeriods_SL)
      (periodic_comp_ofComplex f one_mem_strictPeriods_SL)]

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
hSre : (S • z).re = -z.re
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : |↑(↑g 0 0)| - |z.re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
sub_le_iff_le_add

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
hSre : (S • z).re = -z.re
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : |↑(↑g 0 0)| ≤ 1 / 2 + |z.re|
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
hρ : z = ρ
⊢ (-↑ρ)⁻¹ = ↑(1 +ᵥ ρ)

Tactic:
coe_vadd,

Goal state after:
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
hρ : z = ρ
⊢ (-↑ρ)⁻¹ = ↑1 + ↑ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
have := G2Term_summable z
    rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at this
    exact this.prod

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
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
this✝ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ √1 = ‖↑(1 +ᵥ ρ)‖

Tactic:
coe_vadd,

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
this✝ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ √1 = ‖↑1 + ↑ρ‖
Module: Mathlib.NumberTheory.Modular

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

Tactic:
coe_vadd,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
⊢ (-↑ρ)⁻¹ = ↑1 + ↑ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
⊢ ∑' (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Goal state after:
case inl
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (c : ↑(gammaSet 1 0 0)), eisSummand (↑k) (↑c) z =
    ∑' (c : { x // x ∈ gammaSet 1 1 0 }), (↑(0, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(0, c).2) z

case inr
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
hb : b ≠ 0
⊢ ∑' (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: ⊢ qExpansion 1 ⇑E₄CubeSubE₆SqForm =
    qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ - qExpansion 1 ⇑E₆ * qExpansion 1 ⇑E₆

Tactic:
by
  simp only [E₄CubeSubE₆SqForm, FunLike.coe_sub, coe_mcast,
    ModularForm.qExpansion_sub one_pos one_mem_strictPeriods_SL,
    ModularForm.qExpansion_pow one_pos one_mem_strictPeriods_SL]
  ring

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

Goal state before:
pp: case e_6
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ ↑{ coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    num (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
        ↑{ coe := I * ↑t, coe_im_pos := ⋯ } /
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
        ↑{ coe := I * ↑t, coe_im_pos := ⋯ }

Tactic:
simp [num, denom, div_eq_mul_inv, mul_comm]

Goal state after: