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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hunion :
  {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
⊢ #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q}) + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q =
    p / 2 * (q / 2)

Tactic:
sum_Ico_eq_card_lt,

Goal state after:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hunion :
  {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
⊢ #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q}) +
      #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    p / 2 * (q / 2)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Finite 𝓀[K]

Tactic:
← Set.finite_univ_iff

Goal state after:
case mp
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Set.univ.Finite
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : a % 4 = 0
⊢ fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

pp: case ind.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
⊢ (if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
    else
      if ha1 : a = 1 then if flip = true then -1 else 1
      else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
· rw [IH (a / 4) (a.div_lt_self ha0 (by decide)) hb2 hb1]
    simp only [Int.natCast_ediv, Nat.cast_ofNat, div_four_left (a := a) (mod_cast ha4) hb2]

Goal state after:
case ind.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
⊢ (if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
    else
      if ha1 : a = 1 then if flip = true then -1 else 1
      else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * (↑t ^ (-↑s) / ↑t) - l * ↑t ^ (-↑s) = S t * (↑t ^ (-↑s) / ↑t) - l * (↑t * (↑t ^ (-↑s) / ↑t))

Tactic:
mul_div_cancel₀ _ ht

Goal state after:
case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * (↑t ^ (-↑s) / ↑t) - l * ↑t ^ (-↑s) = S t * (↑t ^ (-↑s) / ↑t) - l * ↑t ^ (-↑s)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ↑↑z < v w
⊢ ¬v.restrict w = v.restrict 0

Tactic:
v.restrict_inj

Goal state after:
case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ↑↑z < v w
⊢ ¬v w = v 0
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
⊢ ∀ {x_1 y : A}, (y ∈ Set.range fun x_2 ↦ x * x_2) → x_1 * y ∈ Set.range fun x_2 ↦ x * x_2

Tactic:
rintro a _ ⟨c, rfl⟩; exact ⟨a * c, 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 := ⋯
y : A
hy : x * y = 1
⊢ ↑(⟨x, hx1✝⟩ * ⟨y, ⋯⟩) = ↑1

Tactic:
exact hy

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

Tactic:
mul_one

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 = y * a
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).coeff ↑d‖ ≤ ↑(n.choose ↑d) * ↑B

Tactic:
apply le_trans <| (p.map (castRingHom ℂ)).norm_coeff_le_choose_mul_mahlerMeasure d

Goal state after:
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.choose ↑d) * (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑(n.choose ↑d) * ↑B
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this : ω ^ ((q + 1) / 4) * 1 = -ωb ^ ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ ω ^ ((q + 1) / 4) + ωb ^ ((q + 1) / 4) = 0

Tactic:
mul_one

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this : ω ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ ω ^ ((q + 1) / 4) + ωb ^ ((q + 1) / 4) = 0
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
h : ↑g 1 0 = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

Tactic:
simp [parabolicFixedPoint, smul_infty_eq_ite, h]

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

Goal state before:
pp: case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
h : ¬↑g 1 0 = 0
⊢ g • ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

Tactic:
simp [parabolicFixedPoint, smul_infty_eq_ite, h]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)).FiniteIndex

Tactic:
constructor
  let t := (toConjAct <| g.map <| Rat.castHom ℝ)⁻¹
  suffices (t • 𝒮ℒ ⊓ 𝒮ℒ).relIndex 𝒮ℒ ≠ 0 by
    rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]
  obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g 1
  rw [Gamma_one_top, ← MonoidHom.range_eq_map] at hN'
  suffices Γ(N) ≤ (t • 𝒮ℒ ⊓ 𝒮ℒ).comap (mapGL ℝ) by
    have _ : NeZero N := ⟨hN⟩
    simpa only [index_comap] using! (finiteIndex_of_le this).index_ne_zero
  intro k hk
  simpa [mem_pointwise_smul_iff_inv_smul_mem] using!
    hN' <| smul_mem_pointwise_smul _ _ _ ⟨k, hk, rfl⟩

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
x✝ : Fin 2 → ℝ
⊢ ↑(Function.eval 0 x✝) * ↑z + ↑(Function.eval 1 x✝) * 1 = ↑(x✝ 0) * ↑z + ↑(x✝ 1)

Tactic:
mul_one

Goal state after:
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
x✝ : Fin 2 → ℝ
⊢ ↑(Function.eval 0 x✝) * ↑z + ↑(Function.eval 1 x✝) = ↑(x✝ 0) * ↑z + ↑(x✝ 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ c 0 * 1 = c 0

Tactic:
mul_one

Goal state after:
case «0»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ c 0 = c 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
⊢ MDiff (f ∣[k] g)

Tactic:
by
  refine g.det_ne_zero.lt_or_gt.elim (fun hg ↦ ?_) (hf.slash_of_pos k)
  rw [show g = J * (J * g) by simp [← mul_assoc, ← sq], SlashAction.slash_mul]
  exact (hf.slashJ k).slash_of_pos _ (by simpa using hg)

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

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ IsZeroAtImInfty (⇑f ∣[k] g)

Tactic:
by
  rw [← OnePoint.isZeroAt_infty_iff, SL_slash, ← OnePoint.IsZeroAt.smul_iff]
  apply zero_at_cusps f
  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff']
  exact ⟨g, by simp [mapGL]⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
use -(g 0 1)
    suffices g = -T ^ (-(g 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]
    ext i j; fin_cases i <;> fin_cases j <;>
      simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Goal state after:
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))) γ)))
⊢ (fun v ↦ ⟨↑v ᵥ* ↑γ, ⋯⟩) ((fun v ↦ ⟨↑v ᵥ* ↑γ⁻¹, ⋯⟩) v) = v

Tactic:
by simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]

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
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
z : ℂ
hz : z ∈ Complex.im ⁻¹' Ioi 0
⊢ DifferentiableAt ℂ (f ∘ ↑ofComplex) z

Tactic:
by
            simpa using (UpperHalfPlane.mdifferentiableAt_iff.mp <| hfhol ⟨z, hz⟩)

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

Goal state before:
pp: n : ℕ
z : ℂ
⊢ eta_q n z = cexp (2 * ↑π * I * z) ^ (n + 1)

Tactic:
by
  simp [eta_q, Periodic.qParam]

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

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F + G) = D F + D G

Tactic:
by
  ext z
  have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
  have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
  simp only [normalizedDerivOfComplex, Pi.add_apply]
  rw [show (F + G) ∘ ofComplex = F ∘ ofComplex + G ∘ ofComplex from rfl,
    deriv_add hFz hGz, mul_add]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inl.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 : ρ ∈ 𝒟
hg : (S * T) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T))) ↑ρ) = 1

Tactic:
rw [show S * T = ⟨!![0, -1; 1, 1], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]

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

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) ((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • qExpansion 1 ⇑(E hk)) -
      (PowerSeries.coeff 0) (qExpansion 1 ⇑f) =
    0

pp: case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

pp: case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

pp: case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

pp: case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

Tactic:
PowerSeries.coeff_smul,

Goal state after:
case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • (PowerSeries.coeff 0) (qExpansion 1 ⇑(E hk)) -
      (PowerSeries.coeff 0) (qExpansion 1 ⇑f) =
    0

case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
this :
  Tendsto
    (((fun s ↦ ∑ x ∈ s, (↑z ^ 2)⁻¹ * e2Summand x { coe := (-↑z)⁻¹, coe_im_pos := ⋯ }) ∘ fun N ↦ Ico (-N) N) ∘ Nat.cast)
    atTop
    (𝓝
      (∑'[{ filter := Filter.map (fun N ↦ Ico (-N) N) (Filter.map Nat.cast atTop) }] (x : ℤ),
        (↑z ^ 2)⁻¹ * e2Summand x { coe := (-↑z)⁻¹, coe_im_pos := ⋯ }))
N : ℕ
⊢ (((fun s ↦ ∑ x ∈ s, (↑z ^ 2)⁻¹ * e2Summand x { coe := (-↑z)⁻¹, coe_im_pos := ⋯ }) ∘ fun N ↦ Ico (-N) N) ∘ Nat.cast)
      N =
    ∑' (n : ℤ), ∑ m ∈ Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2

Tactic:
simpa [e2Summand, eisSummand, ← mul_sum] using! aux_sum_Ico_S_identity z N

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
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0

Tactic:
rcases lt_or_ge k 12 with hk12 | hk12

Goal state after:
case h.inl
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
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : k < 12
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0

case h.inr
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
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun z_1 ↦ (↑z_1.1 ^ k)⁻¹ * eisSummand (↑k) (↑z_1.2) z

Tactic:
exact summable_mul_of_summable_norm (f := fun (n : ℕ) ↦ ((n : ℂ) ^ k)⁻¹)
      (g := fun (v : gammaSet 1 1 0) ↦ eisSummand k v z) (by simp [hk1])
      ((summable_norm_eisSummand hk2 z).subtype _)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ x ∈ closure (closure 𝒟ᵒ)

Tactic:
apply mem_closure_of_frequently_of_tendsto (b := 𝓝[>] 0)
    (f := fun t : ℝ≥0 ↦ ⟨x + t * Complex.I, by
      simpa using! add_pos_of_pos_of_nonneg x.coe_im_pos t.property⟩)

Goal state after:
case h
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ ∃ᶠ (x_1 : ℝ≥0) in 𝓝[>] 0, { coe := ↑x + ↑↑x_1 * Complex.I, coe_im_pos := ⋯ } ∈ closure 𝒟ᵒ

case hf
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ { coe := ↑x + ↑↑t * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: case e_6
z : ℍ
⊢ discriminant z = 1 / 1728 * (E₄ z ^ 3 - E₆ z ^ 2)

Tactic:
grind [discriminant_eq_E₄_cube_sub_E₆_sq z]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))⁻¹ =
    (Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
      (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) ModularGroup.S⁻¹))

Tactic:
simp only [ModularGroup.S_inv, ← map_inv]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)) =
    (Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
      (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S)))
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)
p : ι → Prop
⊢ IsOpen[⨆ S, ⨆ (hS : cofinite ≤ 𝓟 S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S))]
    {f | ∀ (i : ι), p i → ↑f i ∈ A i}

Tactic:
isOpen_iSup_iff,

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
p : ι → Prop
⊢ ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
    IsOpen[TopologicalSpace.coinduced (inclusion R A i_1) (topologicalSpace R A (𝓟 i))]
      {f | ∀ (i : ι), p i → ↑f i ∈ A i}
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)
⊢ IsOpen[⨆ S, ⨆ (hS : cofinite ≤ 𝓟 S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S))]
    {f | ∀ (i : ι), ↑f i ∈ A i}

Tactic:
isOpen_iSup_iff,

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
⊢ ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
    IsOpen[TopologicalSpace.coinduced (inclusion R A i_1) (topologicalSpace R A (𝓟 i))] {f | ∀ (i : ι), ↑f i ∈ A i}