mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ ((-1) ^ k * ↑k !)⁻¹ * (-(2 * ↑π * I) ^ (k + 1) * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)) =
    (-2 * ↑π * I) ^ (k + 1) / ↑k ! * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)

Tactic:
show (-2 * π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * π * I) ^ (k + 1) by rw [← neg_pow]; ring

Goal state after:
case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ ((-1) ^ k * ↑k !)⁻¹ * (-(2 * ↑π * I) ^ (k + 1) * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)) =
    (-1) ^ (k + 1) * (2 * ↑π * I) ^ (k + 1) / ↑k ! * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)
Module: Mathlib.NumberTheory.Modular

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

Tactic:
have hc : g 1 0 = 0 ∨ g 1 0 = 1 := by grind [abs_c_le_one hz hg]

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 0 ∨ ↑g 1 0 = 1
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
H0 :
  (fun n ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑n / ↑z - ↑↑m) + 1 / (-↑↑n / ↑z + ↑↑m))) = fun n ↦
    -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n
⊢ Tendsto (fun x ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑x / ↑z - ↑↑m) + 1 / (-↑↑x / ↑z + ↑↑m))) atTop (𝓝 (-2 * ↑π * I / ↑z))

Tactic:
rw [H0]

Goal state after:
z : ℍ
H0 :
  (fun n ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑n / ↑z - ↑↑m) + 1 / (-↑↑n / ↑z + ↑↑m))) = fun n ↦
    -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n
⊢ Tendsto
    (fun n ↦ -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n)
    atTop (𝓝 (-2 * ↑π * I / ↑z))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n ↦ cexp (↑π * I * ↑↑n ^ 2 * τ) + cexp (↑π * I * ↑(-↑n) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
rw [← hasSum_nat_add_iff' 1] at this

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n ↦ cexp (↑π * I * ↑↑(n + 1) ^ 2 * τ) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ) -
      ∑ i ∈ Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * τ) + cexp (↑π * I * ↑(-↑i) ^ 2 * τ)))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
a : ℝ
ha : 0 < a
ha' : a ∈ Set.Iio 1
⊢ |(↑(↑ofComplex (↑a * ↑x))).re| < 1 / 2

Tactic:
ofComplex_apply_of_im_pos (by simpa using mul_pos ha x.coe_im_pos)

Goal state after:
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
a : ℝ
ha : 0 < a
ha' : a ∈ Set.Iio 1
⊢ |(↑{ coe := ↑a * ↑x, coe_im_pos := ⋯ }).re| < 1 / 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun t ↦ ↑t * ↑x) (𝓝 1) (𝓝 ↑x)
a : ℝ
ha : 0 < a
⊢ ↑a * ↑x = ↑(↑ofComplex (↑a * ↑x))

Tactic:
ofComplex_apply_of_im_pos (by simpa using mul_pos ha x.coe_im_pos)

Goal state after:
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun t ↦ ↑t * ↑x) (𝓝 1) (𝓝 ↑x)
a : ℝ
ha : 0 < a
⊢ ↑a * ↑x = ↑{ coe := ↑a * ↑x, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous

Goal state before:
pp: 𝒮ℒ' : Subgroup SL(2, ℝ) := (SpecialLinearGroup.map (Int.castRingHom ℝ)).range
this : ∀ {K L : Set ℍ}, IsCompact K → IsCompact L → {g | g ∈ 𝒮ℒ' ∧ (g • K ∩ L).Nonempty}.Finite
K L : Set ℍ
hK : IsCompact K
hL : IsCompact L
γ : SL(2, ℤ)
hγ : ((SpecialLinearGroup.mapGL ℝ) γ • K ∩ L).Nonempty
⊢ (SpecialLinearGroup.map (Int.castRingHom ℝ)) γ ∈ 𝒮ℒ'

Tactic:
by simp [𝒮ℒ']

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
this : x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (∏ i ∈ range (d + 1), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_1
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ 2 ^ 1 ∣ x ^ 2 ^ i + y ^ 2 ^ i

pp: case refine_2
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ i + y ^ 2 ^ i

Tactic:
· rw [pow_one, ← even_iff_two_dvd]
    exact hx_odd.pow.add_odd hy_odd.pow

Goal state after:
case refine_2
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ i + y ^ 2 ^ i
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) ≠ 0

Tactic:
rw [norm_unit]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ 1 ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : x ∈ fundamentalCone K
hy : ∀ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x
⊢ logMap x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
exact hx.1

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ logMap x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
exact hx.1

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ logMap (u • x) ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
logMap_unit_smul u hx

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ (logEmbedding K) (Additive.ofMul u) + logMap x ∈
    ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
⊢ 0 = |(of fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))).det|

Tactic:
det_eq_zero_of_not_linearIndependent_rows,

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
⊢ 0 = |0|

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
⊢ ¬LinearIndependent ℝ fun i ↦ of (fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))) i
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case left
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ logMap x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
exact hx.1

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
exact hx.1

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : mixedSpace K
ha : a ∈ integerSet K
⊢ ∃! x, (mixedEmbedding K) ↑x = a

Tactic:
obtain ⟨_, ⟨x, rfl⟩⟩ := mem_integerSet.mp ha

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
ha : (mixedEmbedding K) ↑x ∈ integerSet K
left✝ : (mixedEmbedding K) ↑x ∈ fundamentalCone K
⊢ ∃! x_1, (mixedEmbedding K) ↑x_1 = (mixedEmbedding K) ↑x
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
⊢ IsUnit ↑u

Tactic:
exact u.isUnit

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ realUnits K = (unitsMulComplexConjInv K).ker

pp: case e'_3
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 = (Subgroup.map (unitsMulComplexConjInv K) (torsion K)).index

Tactic:
· rw [unitsMulComplexConjInv_ker]

Goal state after:
case e'_3
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 = (Subgroup.map (unitsMulComplexConjInv K) (torsion K)).index
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔ span {Polynomial.map (Int.castRingHom (ZMod p)) Q}

Tactic:
rw [← span_insert, span_pair_comm, span_pair_eq_span_left_iff_dvd.mpr]
    simp only [Multiset.mem_toFinset] at hQ
    exact ((Polynomial.mem_normalizedFactors_iff h₀).mp hQ).2.2

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
this : NeZero ↑n
⊢ IsPrimitiveRoot (root P) n

Tactic:
simpa [← isRoot_cyclotomic_iff] using! (isRoot_root P).dvd
      (by simpa using! map_dvd (algebraMap K (AdjoinRoot P)) hP)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) ≡ 1 [MOD n]

Tactic:
← natCast_eq_natCast_iff

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ ↑((p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯)) = ↑1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p

Tactic:
have : IsGalois ℚ K := isGalois {m} ℚ K
  obtain ⟨⟨P, _, _⟩⟩ := 𝒑.nonempty_primesOver (S := 𝓞 K)
  rw [inertiaDegIn_eq_inertiaDeg 𝒑 P Gal(K/ℚ), inertiaDeg_eq_of_not_dvd p K P hm]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: case refine_1
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
this : IsGalois ℚ K
⊢ ↑((galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P)) ⊆ ↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn))

pp: case refine_2
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
this : IsGalois ℚ K
⊢ Fintype.card ↑↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) ≤
    Fintype.card ↑↑((galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P))

Tactic:
· rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ

Goal state after:
case refine_2
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
this : IsGalois ℚ K
⊢ Fintype.card ↑↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) ≤
    Fintype.card ↑↑((galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P))
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
s : ℝ
⊢ (∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) / ∑' (𝔭 : ↑univ), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s) ≤ 1

Tactic:
tsum_univ fun 𝔭 : HeightOneSpectrum (𝓞 K) ↦ (𝔭.asIdeal.absNorm : ℝ) ^ (-s)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
s : ℝ
⊢ (∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) /
      ∑' (x : HeightOneSpectrum (𝓞 K)), ↑(Ideal.absNorm x.asIdeal) ^ (-s) ≤
    1
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f 1 = f (↑a * ↑p ^ k + ↑b * ↑m ^ k)

Tactic:
rw_mod_cast [bezout]

Goal state after:
f : AbsoluteValue ℚ ℝ
p m : ℕ
hpm : ¬p ∣ m
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hm : f ↑m < 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
bezout : a * ↑(p ^ k) + b * ↑(m ^ k) = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f 1 = f ↑1
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
H : 1 ≤ ↑n
⊢ 1 ≤ ↑n * max 1 ‖A‖

Tactic:
exact one_le_mul_of_one_le_of_one_le H <| le_max_left ..

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
⊢ a *ᵥ ξ K x = 0

Tactic:
by
  funext k; simp only [Pi.zero_apply]; rw [eq_comm]
  have lin_0 : ∀ u, ∑ r, ∑ l, (a' K a k l r u * x (l, r) : 𝓞 K) = 0 := by
    intro u
    have hξ := ξ_ne_0 K x hxl
    rw [Ne, funext_iff, not_forall] at hξ
    rcases hξ with ⟨l, hξ⟩
    rw [funext_iff] at hmulvec0
    specialize hmulvec0 ⟨k, u⟩
    simp only [Fintype.sum_prod_type, mulVec, dotProduct, asiegel] at hmulvec0
    rw [sum_comm] at hmulvec0
    exact mod_cast hmulvec0
  have : 0 = ∑ u, (∑ r, ∑ l, a' K a k l r u * x (l, r) : 𝓞 K) * (newBasis K) u := by
    simp only [lin_0, zero_mul, sum_const_zero]
  have : 0 = ∑ r, ∑ l, x (l, r) * ∑ u, a' K a k l r u * (newBasis K) u := by
    conv at this => enter [2, 2, u]; rw [sum_mul]
    rw [sum_comm] at this
    rw [this]; congr 1; ext1 r
    conv => enter [1, 2, l]; rw [sum_mul]
    rw [sum_comm]; congr 1; ext1 r
    rw [mul_sum]; congr 1; ext1 r
    ring
  rw [sum_comm] at this
  rw [this]; congr 1; ext1 l
  rw [ξ, mul_sum]; congr 1; ext1 l
  rw [← lin_1]; ring

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
⊢ ‖replicateCol Unit (x - y)‖ ≤ (↑n * max 1 ‖A‖) ^ e

Tactic:
norm_le_iff n_mul_norm_A_pow_e_nonneg

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
⊢ ∀ (i : β) (j : Unit), ‖replicateCol Unit (x - y) i j‖ ≤ (↑n * max 1 ‖A‖) ^ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
⊢ ∃ N, ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t

Tactic:
simpa using! tendsto_def.mp hf t t.mem_nhds_one

Goal state after:
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: case e_6
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
y : Y
⊢ μ { toFun := fun x ↦ (f.comp fst • g.comp snd) (x, y), continuous_toFun := ⋯ } = μ (g y • f)

Tactic:
congr 1 with x

Goal state after:
case e_6.e_6
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
y : Y
x : X
⊢ { toFun := fun x ↦ (f.comp fst • g.comp snd) (x, y), continuous_toFun := ⋯ } x = (g y • f) x
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
⊢ μ ((contractSnd ν) (f.comp fst • g.comp snd)) = μ (ν g • f)

Tactic:
congr 1 with x

Goal state after:
case e_6
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
x : X
⊢ ((contractSnd ν) (f.comp fst • g.comp snd)) x = (ν g • f) x
Module: Mathlib.NumberTheory.PowModTotient

Goal state before:
pp: x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ (k % φ n + k / φ n * φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n

Tactic:
pow_add_mul_totient_mod_eq hn h,

Goal state after:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ (k % φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ (d * (a.y * b.y)) ^ 2 < (1 + d * a.y ^ 2) * (1 + d * b.y ^ 2)

Tactic:
←
    sub_pos

Goal state after:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < (1 + d * a.y ^ 2) * (1 + d * b.y ^ 2) - (d * (a.y * b.y)) ^ 2
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
this✝ :
  ‖↑((Polynomial.aeval z) (Polynomial.derivative F)) *
        (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)))‖ ≤
    1
this : (Polynomial.aeval z) (Polynomial.derivative F) * -z1 = -(Polynomial.aeval z) F
⊢ { q // (Polynomial.aeval z') F = q * z1 ^ 2 }

Tactic:
exact ⟨q, by simpa [sub_eq_add_neg, neg_mul_eq_mul_neg, this, hz'] using hq⟩

Goal state after: