mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
⊢ HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s)
    (mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s)

Tactic:
]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
⊢ HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s)
    (mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this✝ : ModularFormClass
  (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range
    (0 *
      ↑(Nat.card
          (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))))
  (Matrix.SpecialLinearGroup.mapGL ℝ).range 0 :=
  Eq.mpr
    (id
      (congrArg
        (fun _a ↦
          ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range _a)
            (Matrix.SpecialLinearGroup.mapGL ℝ).range 0)
        (zero_mul
          ↑(Nat.card
              (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range)))))
    inferInstance
this : (ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range (f - const (f I))) I = 0
hc : f = const (f I)
⊢ Function.const ℍ (f I) = Function.const ℍ (f I)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : (Ideal.Quotient.mk (span {p})) x = (Ideal.Quotient.mk (span {p})) y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)

Tactic:
]

Goal state after:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : (Ideal.Quotient.mk (span {p})) x = (Ideal.Quotient.mk (span {p})) y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ ↑n * x ^ (n - 1) ↔ p ∣ ↑n * x ^ (n - 1)

pp: R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ y - x

Tactic:
]

Goal state after:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ y - x
Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing

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

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K∞
hx : ∃ x_1, ¬IsUnit (x x_1)
⊢ ‖x‖ = 0
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x))) =
    (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1))

Tactic:
]

Goal state after:
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
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x))) =
    (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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 ∈ range p
⊢ a ^ (p - 1) = a ^ (p - 1)

pp: 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 ∈ range p
⊢ x ≤ p - 1

Tactic:
]

Goal state after:
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 ∈ range p
⊢ x ≤ p - 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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
this : ∀ x ∈ range p, a ^ (x + (p - 1 - x)) = a ^ (p - 1)
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1))

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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
⊢ (Ideal.Quotient.mk (span {s})) ((range p).sum ?m.849) + (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, ↑p * b * a ^ (p - 2) * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))

pp: 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 ∈ range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x = ?m.849 x

pp: 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 := ⋯
⊢ ℕ → R

Tactic:
]

Goal state after:
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 ∈ range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x = ↑p * b * a ^ (p - 2) * ↑x
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case zero
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
hx : 0 ∈ range p
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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
⊢ x.succ - 1 + (p - 1) - (x + 1) = p - 2

Tactic:
]

Goal state after:
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
⊢ x.succ - 1 + (p - 1) - (x + 1) = p - 2
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
this : x.succ - 1 + (p - 1 - x.succ) = p - 2
⊢ a ^ (p - 2) * ↑p * b * ↑(x + 1) = ↑p * b * a ^ (p - 2) * ↑(x + 1)

Tactic:
]

Goal state after:
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
this : x.succ - 1 + (p - 1 - x.succ) = p - 2
⊢ a ^ (p - 2) * ↑p * b * ↑(x + 1) = ↑p * b * a ^ (p - 2) * ↑(x + 1)
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: v : InfinitePlace ℚ
x : ℚ
⊢ ↑|x| = ↑|x|

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
r : ℝ
hr : Complex.ofRealHom r = v.embedding x
⊢ (star v.embedding) x = v.embedding x

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
r : ℝ
hr : Complex.ofRealHom r = v.embedding x
⊢ (star v.embedding) x = v.embedding x
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange = ⊤

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange = ⊤
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) ↑p ^ 2 *
      ((Ideal.Quotient.mk (span {s})) b *
        ((Ideal.Quotient.mk (span {s})) (a ^ (p - 2)) * (Ideal.Quotient.mk (span {s})) ↑((p - 1) / 2))) =
    0

Tactic:
]

Goal state after:
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
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) ↑p ^ 2 *
      ((Ideal.Quotient.mk (span {s})) b *
        ((Ideal.Quotient.mk (span {s})) (a ^ (p - 2)) * (Ideal.Quotient.mk (span {s})) ↑((p - 1) / 2))) =
    0
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ (extensionEmbeddingOfIsReal hv).fieldRange = ?m.18

pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed ↑?m.18

pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ Subfield ℝ

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed ↑(extensionEmbeddingOfIsReal hv).fieldRange
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝² : Field K
v : InfinitePlace K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
w : InfinitePlace L
x : WithAbs ↑v
⊢ (algebraMap (WithAbs ↑v) (↑w).Completion) x =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }.toCompletion

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
v : InfinitePlace K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
w : InfinitePlace L
x : WithAbs ↑v
⊢ (algebraMap (WithAbs ↑v) (↑w).Completion) x =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }.toCompletion
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: case hp
K : Type u_1
inst✝⁶ : Field K
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝³ : Algebra v.Completion w.Completion
inst✝² : IsScalarTower K v.Completion w.Completion
inst✝¹ : ContinuousSMul v.Completion w.Completion
inst✝ : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ IsClosed {x | ((extensionEmbedding w).comp (algebraMap v.Completion w.Completion)) x = (extensionEmbedding v) x}

Tactic:
exact isClosed_eq
        ((isometry_extensionEmbedding w).continuous.comp
          (continuous_algebraMap v.Completion w.Completion))
        (isometry_extensionEmbedding v).continuous

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

Goal state before:
pp: case refine_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : ↑k + 1 < s.re
⊢ mellin (fun x ↦ (weakFEPair hk f).f x - (weakFEPair hk f).f₀) s =
    mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : ¬p ∣ ↑n
⊢ emultiplicity p (x - y) = emultiplicity p (x - y)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)) = 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)) = 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ ↑p ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ ↑p ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ y
⊢ ¬↑p ^ (1 + 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ y
⊢ ¬↑p ^ (1 + 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ^ 2 ∣ ∑ i ∈ range p, (y + ↑p * k) ^ i * y ^ (p - ↑1 - i)

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ^ 2 ∣ ∑ i ∈ range p, (y + ↑p * k) ^ i * y ^ (p - ↑1 - i)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ∣ y ^ (p - 1)

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ∣ y ^ (p - 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (x - y) + 1 = emultiplicity (↑p) (x - y) + 1

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst✝¹ : (i : ι₁) → SetLike (S₁ i) (R₁ i)
inst✝ : (j : ι₂) → SetLike (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
x : Πʳ (i : ι₁), [R₁ i, A₁ i]_[𝓕₁]
⊢ ∀ᶠ (i : ι₂) in 𝓕₂, (fun j ↦ φ j (x (f j))) i ∈ (fun j ↦ A₂ j) i

Tactic:
by
  filter_upwards [hf.eventually x.2, hφ] using fun _ h1 h2 ↦ h2 h1

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (x - y) = emultiplicity (↑p) (x - y)

Tactic:
]

Goal state after:
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)
S : Set ι
⊢ TopologicalSpace.induced DFunLike.coe inferInstance ≤ TopologicalSpace.induced DFunLike.coe inferInstance

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ emultiplicity (↑p) ((x ^ p ^ a) ^ p - (y ^ p ^ a) ^ p) = emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) + 1

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ emultiplicity (↑p) ((x ^ p ^ a) ^ p - (y ^ p ^ a) ^ p) = emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) + 1
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
]

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hxy
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ ↑p ∣ (∑ i ∈ range (p ^ a), x ^ i * y ^ (p ^ a - 1 - i)) * (x - y)

Tactic:
]

Goal state after:
case succ.hxy
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ ↑p ∣ (∑ i ∈ range (p ^ a), x ^ i * y ^ (p ^ a - 1 - i)) * (x - y)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

Tactic:
]

Goal state after:
case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (↑2 ^ s * ↑π ^ s / Gamma s * ↑(h Γ) ^ (-s))

Tactic:
]

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (↑2 ^ s * ↑π ^ s / Gamma s * ↑(h Γ) ^ (-s))
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, ↑(B i)]_[𝓕]
hx : ∀ (i : ι), IsUnit (x i)
hxr : ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩
⊢ ∃ b, x * b = 1 ∧ b * x = 1

Tactic:
]

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, ↑(B i)]_[𝓕]
hx : ∀ (i : ι), IsUnit (x i)
hxr : ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩
⊢ ∃ b, x * b = 1 ∧ b * x = 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) (x - y) + ↑(multiplicity p (n + 1)) = emultiplicity (↑p) (x - y) + ↑(multiplicity p (n + 1))

pp: case succ.hxy
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ↑p ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)

pp: case succ.hx
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ x ^ p ^ multiplicity p (n + 1)

pp: case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ ↑k

Tactic:
]

Goal state after:
case succ.hxy
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ↑p ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)

case succ.hx
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ x ^ p ^ multiplicity p (n + 1)

case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ ↑k