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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ 1 ≤ (↑b / a).valMinAbs.natAbs

pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (↑b / a).valMinAbs.natAbs < (p / 2).succ

pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (a * ↑(↑b / a).valMinAbs.natAbs).valMinAbs.natAbs = b

Tactic:
· apply Nat.pos_of_ne_zero
      simp only [div_eq_mul_inv, hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hb, not_false_iff,
        valMinAbs_eq_zero, inv_eq_zero, Int.natAbs_eq_zero, Ne, _root_.mul_eq_zero, or_self_iff]

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (↑b / a).valMinAbs.natAbs < (p / 2).succ

case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (a * ↑(↑b / a).valMinAbs.natAbs).valMinAbs.natAbs = b
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑a * ↑x).valMinAbs.natAbs) =
    ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, x)

Tactic:
Finset.sum_eq_multiset_sum,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) +
      ↑(Multiset.map (fun x ↦ (↑a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val).sum =
    ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, x)
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
⊢ IsDiscrete R

Tactic:
by_cases h : IsNontrivial R

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
⊢ IsDiscrete R

case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : ¬IsNontrivial R
⊢ IsDiscrete R
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
h : 1 = -1
⊢ False

Tactic:
CharZero.eq_neg_self_iff

Goal state after:
a : ℤ
h : 1 = 0
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ False

Tactic:
apply (by simp : ¬(0 : ℤ) ≤ -1)

Goal state after:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ 0 ≤ -1
Module: Mathlib.Topology.Algebra.Valued.ValuativeRel

Goal state before:
pp: R✝ : Type u_1
inst✝⁸ : Ring R✝
inst✝⁷ : ValuativeRel R✝
inst✝⁶ : TopologicalSpace R✝
inst✝⁵ : IsValuativeTopology R✝
R : Type u_2
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : IsValuativeTopology R
a✝ : Set R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simpa [← Valuation.restrict_lt_iff_lt_embedding] using
      (valuation R).exists_setOfPred_restrict_le_iff 0 _

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

Goal state before:
pp: case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ε

Tactic:
have hp' := Valuation.integer.v_irreducible_lt_one hp

Goal state after:
case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : v ↑p < 1
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
exact lt_of_le_of_ne (Nat.one_le_iff_ne_zero.mpr hb0) (Ne.symm hb1)

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
a c : A
⊢ a * x * c = a * (x * c)

Tactic:
mul_assoc

Goal state after:
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
a c : A
⊢ a * (x * c) = a * (x * c)
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
a c : A
⊢ (fun x_1 ↦ x * x_1) (a * c) = a * (fun x_1 ↦ x * x_1) c

Tactic:
by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]

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
b a : A
⊢ a * x * b = a * x * b

Tactic:
mul_assoc

Goal state after:
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
b a : A
⊢ a * (x * b) = a * (x * b)
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
b a : A
⊢ (fun x_1 ↦ x * x_1) (a * b) = (fun x_1 ↦ x * x_1) a * b

Tactic:
by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]

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 * (a * x) * y = y * (a * x * y)

Tactic:
mul_assoc

Goal state after:
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 * (a * x * y) = y * (a * x * y)
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: case calc_1
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ n = #𝒜

Tactic:
rw [Finset.card_image_of_injOn, card_Iio]
    simpa using! prod_primeFactors_invOn_squarefree.2.injOn.comp hf.injOn hf'

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
p' : ℕ
k : ℤ
h : ↑(s p') = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
closed_form

Goal state after:
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' + ωb ^ 2 ^ p' = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case left.hH
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ Γ.relIndex (mapGL ℝ).range ≠ 0

Tactic:
exact IsArithmetic.is_commensurable.1

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

Goal state before:
pp: case hK
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ Γ'.relIndex (mapGL ℝ).range ≠ 0

Tactic:
exact IsArithmetic.is_commensurable.1

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ (∃ y ∈ Γ,
      toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) y) =
        toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (g * x * g⁻¹))) ↔
    x ∈ toConjAct g⁻¹ • Γ

Tactic:
toGL_injective.eq_iff,

Goal state after:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ (∃ y ∈ Γ,
      (SpecialLinearGroup.map (Int.castRingHom ℝ)) y = (SpecialLinearGroup.map (Int.castRingHom ℝ)) (g * x * g⁻¹)) ↔
    x ∈ toConjAct g⁻¹ • Γ
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ (m *ᵥ v) ((fun i ↦ i) ⟨0, ⋯⟩) = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [mulVec_eq_sum]

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

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ (m *ᵥ v) ((fun i ↦ i) ⟨1, ⋯⟩) = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [mulVec_eq_sum]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)

Tactic:
by_cases h₀ : w 1 = 0

Goal state after:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
h₀ : w 1 = 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)

case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
h₀ : ¬w 1 = 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)
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:
by_cases h₀ : w 1 = 0

Goal state after:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 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

case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 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
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case empty
β : Type u_1
G : Type u_2
α : Type u_3
ι : Type u_4
inst✝² : Monoid G
inst✝¹ : AddCommGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : ι → α
⊢ (∑ i ∈ ∅, a i) ∣[k] g = ∑ i ∈ ∅, a i ∣[k] g

Tactic:
| empty =>

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

Goal state before:
pp: case e'_1.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ f (γ • z) * denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ (-k) =
    ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (γ • z)

Tactic:
simp only [mul_comm (f _), denom, zpow_neg]
    rfl

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

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : atImInfty.BoundedAtFilter f
⊢ atImInfty.BoundedAtFilter (f ∣[k] g)

Tactic:
BoundedAtFilter,

Goal state after:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : f =O[atImInfty] 1
⊢ (f ∣[k] g) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.SlashActions

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

Tactic:
| empty =>

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

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : (fun x ↦ ‖f x‖) =O[atImInfty] 1
⊢ (fun x ↦ ‖(f ∣[k] g) x‖) =O[atImInfty] 1

Tactic:
suffices (fun x ↦ (‖g.det.val ^ (k - 1)‖ * ‖g 1 1 ^ (-k)‖) * ‖f (g • x)‖) =O[atImInfty] 1 by
    simpa [ModularForm.slash_def, denom, hg, mul_assoc, mul_comm ‖f _‖]

Goal state after:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : (fun x ↦ ‖f x‖) =O[atImInfty] 1
⊢ (fun x ↦ ‖↑(GeneralLinearGroup.det g) ^ (k - 1)‖ * ‖↑g 1 1 ^ (-k)‖ * ‖f (g • x)‖) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

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

Tactic:
by
  constructor
  · obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
    simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using! fun hfc ↦ ⟨γ, rfl, hfc⟩
  · rintro ⟨γ, rfl, b⟩
    simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using! b

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsZeroAtImInfty ((ModularForm.translate f g).toFun ∣[k] γ)

Tactic:
rw [SlashInvariantForm.toFun_eq_coe, ModularForm.toSlashInvariantForm_coe,
      ModularForm.coe_translate, ← SlashAction.slash_mul, ← isZeroAt_infty_iff,
      ← OnePoint.IsZeroAt.smul_iff]
    apply CuspFormClass.zero_at_cusps f
    simpa [mul_smul, hγ] using hc.smul g

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

Goal state before:
pp: case neg
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
⊢ v = r • divIntMap (↑r) v

Tactic:
· ext i
    simp_all [Pi.smul_apply, divIntMap, ← Int.mul_ediv_assoc _ (gammaSet_div_gcd hv i)]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.left
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
cases abs_cases ((g • z).re + 1) <;> cases abs_cases (g • z).re <;> linarith

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : IsBigOWith C (comap UpperHalfPlane.im (𝓝 0)) ⇑f fun τ ↦ τ.im ^ (-e)
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖(PowerSeries.coeff x) (qExpansion Γ.strictWidthInfty ⇑f)‖ ≤ c * ‖↑x ^ e‖

Tactic:
rw [IsBigOWith, eventually_comap] at hC

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖(PowerSeries.coeff x) (qExpansion Γ.strictWidthInfty ⇑f)‖ ≤ c * ‖↑x ^ e‖
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: case refine_1
z : ℂ
hz : z ∈ ℍₒ
⊢ ∀ (i : ℕ), 1 + -eta_q i z ≠ 0

Tactic:
exact fun i ↦ by simpa using! one_sub_eta_q_ne_zero i hz

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

Goal state before:
pp: case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
⊢ 2 * ((I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n) =
    -(8 * (↑π ^ 2 * ∑' (n : ℕ+), cexp (↑z * (I * ↑π) * 2) ^ ↑n * (cexp (↑z * (I * ↑π) * 2) ^ (a * ↑n) * ↑↑n)))

Tactic:
← tsum_mul_left,

Goal state after:
case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
⊢ ∑' (x : ℕ+), 2 * ((I * (↑π * 2)) ^ 2 * (cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑x * ↑↑x)) =
    -∑' (x : ℕ+), 8 * (↑π ^ 2 * (cexp (↑z * (I * ↑π) * 2) ^ ↑x * (cexp (↑z * (I * ↑π) * 2) ^ (a * ↑x) * ↑↑x)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

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

Tactic:
rw [iteratedDerivWithin_const_sub hk, iteratedDerivWithin_fun_neg,
      iteratedDerivWithin_const_mul (by simpa using z.2) (isOpen_upperHalfPlaneSet.uniqueDiffOn)]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ -(2 * ↑π * I * iteratedDerivWithin k (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z) =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z

case hf
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ContDiffWithinAt ℂ (↑k) (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: ⊢ (qExpansion 1 Δ).order = 1

Tactic:
by
  refine PowerSeries.order_eq_nat.mpr
    ⟨discriminant_qExpansion_coeff_one ▸ one_ne_zero, fun i hi ↦ ?_⟩
  obtain rfl : i = 0 := by lia
  simpa using CuspFormClass.qExpansion_coeff_zero CuspForm.discriminant one_pos
    one_mem_strictPeriods_SL

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

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

Tactic:
← tsum_mul_left,

Goal state after:
z : ℍ
N : ℕ
n : ℤ
hn : n ∈ Ico (-↑N) ↑N
⊢ ∑' (x : ℤ), (↑z ^ 2)⁻¹ * ((-(↑n * (↑z)⁻¹) + ↑x) ^ 2)⁻¹ = ∑' (b : ℤ), ((↑b * ↑z + ↑n) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (c : ℤ), eisSummand ↑k ![(0, c).1, (0, c).2] z +
      ↑2 * ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
mul_assoc

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (c : ℤ), eisSummand ↑k ![(0, c).1, (0, c).2] z +
      ↑2 * ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case hf
z : ℍ
d : ℕ+
this : Summable fun n ↦ cotTerm (-↑↑d / ↑z) n
⊢ Summable fun m ↦ 1 / (-↑↑d / ↑z - ↑↑m) + 1 / (-↑↑d / ↑z + ↑↑m)

Tactic:
simp only [cotTerm, one_div] at *

Goal state after:
case hf
z : ℍ
d : ℕ+
this : Summable fun n ↦ (-↑↑d / ↑z - (↑n + 1))⁻¹ + (-↑↑d / ↑z + (↑n + 1))⁻¹
⊢ Summable fun m ↦ (-↑↑d / ↑z - ↑↑m)⁻¹ + (-↑↑d / ↑z + ↑↑m)⁻¹
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ 𝒟 = closure 𝒟ᵒ

Tactic:
by
  refine subset_antisymm ?_ (isClosed_fd.closure_subset_iff.mpr fdo_subset_fd)
  intro x ⟨hx, hx'⟩
  rw [one_le_normSq_iff] at hx
  rcases lt_or_eq_of_le hx with hx | hx
  · exact mem_closure_of_one_lt_norm hx hx'
  · exact mem_closure_of_arc hx.symm hx'

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

Goal state before:
pp: case refine_1
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hn : ModularForm.norm ℋ f = 0
⊢ ⇑f = 0

Tactic:
contrapose! hn
    exact norm_ne_zero ℋ hn

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
⊢ (mixedEmbedding K) x = (ringEquiv_mixedSpace K) ((algebraMap K K∞) x)

Tactic:
ext v <;> simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K∞
v : InfinitePlace K
hv : ¬IsUnit (x v)
⊢ ‖x v‖ ^ v.mult = 0

Tactic:
by simpa [isUnit_iff_ne_zero] using hv

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
x : ℕ
hx : x + 1 ∈ range p
⊢ a ^ (x + 1 - 1 + (p - 1 - (x + 1))) * ↑p * b * ↑(x + 1) = ↑p * b * a ^ (p - 2) * ↑(x + 1)

Tactic:
have : x.succ - 1 + (p - 1 - x.succ) = p - 2 := by
          rw [← Nat.add_sub_assoc (Nat.le_sub_one_of_lt (Finset.mem_range.mp hx))]
          exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)
        rw [this]
        ring1

Goal state after: