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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det ^ (k - 1) * ↑(↑g).det ^ 2) *
          denom g ↑z ^ (-k + -2)) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))

Tactic:
zpow_add₀ hz,

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det ^ (k - 1) * ↑(↑g).det ^ 2) *
          (denom g ↑z ^ (-k) * denom g ↑z ^ (-2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ z.im * normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = z.im

Tactic:
mul_eq_left₀ z.im_ne_zero

Goal state after:
case inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = 1
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
h : F ∣[k] γ = F
⊢ serreDerivative (↑k) F ∣[k + 2] γ = serreDerivative (↑k) F

Tactic:
grind [serreDerivative_slash_equivariant]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T⁻¹ * S) 1 0
hc : ↑(T⁻¹ * S) 1 0 = 1
hd : ↑(T⁻¹ * S) 1 1 = 0
hz : ρ ∈ 𝒟
hg : (T⁻¹ * S) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S))) ↑ρ) = 1

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

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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
⊢ -(2 * ↑π * I * (2 * ↑π * I) ^ k) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n =
    -(2 * ↑π * I) * ∑' (n : ℕ), (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
simp_rw [← tsum_mul_left]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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
⊢ ∑' (x : ℕ), -(2 * ↑π * I * (2 * ↑π * I) ^ k) * (↑x ^ k * cexp (2 * ↑π * I * ↑z) ^ x) =
    ∑' (x : ℕ), -(2 * ↑π * I) * ((2 * ↑π * I * ↑x) ^ k * cexp (2 * ↑π * I * ↑z) ^ x)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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
⊢ (fun x ↦ -(2 * ↑π * I * (2 * ↑π * I) ^ k) * (↑x ^ k * cexp (2 * ↑π * I * ↑z) ^ x)) = fun x ↦
    -(2 * ↑π * I) * ((2 * ↑π * I * ↑x) ^ k * cexp (2 * ↑π * I * ↑z) ^ x)

Tactic:
ext y

Goal state after:
case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  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
y : ℕ
⊢ -(2 * ↑π * I * (2 * ↑π * I) ^ k) * (↑y ^ k * cexp (2 * ↑π * I * ↑z) ^ y) =
    -(2 * ↑π * I) * ((2 * ↑π * I * ↑y) ^ k * cexp (2 * ↑π * I * ↑z) ^ y)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ ∑'[symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2 = (↑z ^ 2)⁻¹ * G2 (S • z)

Tactic:
apply HasSum.tsum_eq
  rw [hasSum_symmetricIco_int_iff]
  apply (tendsto_double_sum_S_act z).congr (fun x ↦ ?_)
  rw [Summable.tsum_finsetSum]
  exact fun i hi ↦ by simpa using! linear_left_summable (ne_zero z) i le_rfl

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
g : SL(2, ℤ)
hg : g • I = I
⊢ g ∈ {1, -1, S, -S}

Tactic:
have := cases_of_mem_fd_smul_mem_fd I_mem_fd (hg.symm ▸ I_mem_fd)

Goal state after:
case mp
g : SL(2, ℤ)
hg : g • I = I
this :
  (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ I.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ I.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑I‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ I = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ I = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ I = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ I = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ I = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ I = ρ
⊢ g ∈ {1, -1, S, -S}
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr
k : ℕ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑((↑k).toNat / 12) < (qExpansion 1 ⇑f).order
⊢ f = 0

Tactic:
exact sturm_bound_levelOne_nat (mod_cast h)

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ (E hk) z = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n

Tactic:
convert! q_expansion_riemannZeta hk hk2 z using 1
  rw [eisensteinSeries_coeff_identity hk2 (by grind), neg_mul, ← sub_eq_add_neg]

Goal state after:
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
c : ℂ
hc : ⇑(ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range (f - const (f I))) = Function.const ℍ c
this : (ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range (f - const (f I))) I = 0
⊢ c = 0

Tactic:
by simpa [hc]

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 𝓕₂ 𝓕₁
inst✝³ : (i : ι₁) → Monoid (R₁ i)
inst✝² : (i : ι₂) → Monoid (R₂ i)
inst✝¹ : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)
inst✝ : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)
φ : (j : ι₂) → R₁ (f j) →* R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)
x y : Πʳ (i : ι₁), [R₁ i, ↑(B₁ i)]_[𝓕₁]
⊢ mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ (x * y) =
    mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ x * mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ y

Tactic:
ext i
    exact map_mul (φ i) _ _

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)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : S ∈ cofinite
p : ι → Prop
⊢ IsOpen[topologicalSpace R A (𝓟 S)] {f | ∀ (i : ι), p i → ↑f i ∈ A i}

Tactic:
convert!
    isOpen_set_pi (hS.inter_of_left {i | p i}) (fun i _ ↦ hAopen i) |>.preimage continuous_coe

Goal state after:
case e'_3
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : S ∈ cofinite
p : ι → Prop
⊢ {f | ∀ (i : ι), p i → ↑f i ∈ A i} = DFunLike.coe ⁻¹' (Sᶜ ∩ {i | p i}).pi A
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: case e'_3
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : S ∈ cofinite
p : ι → Prop
⊢ {f | ∀ (i : ι), p i → ↑f i ∈ A i} = DFunLike.coe ⁻¹' (Sᶜ ∩ {i | p i}).pi A

Tactic:
ext f

Goal state after:
case e'_3
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : S ∈ cofinite
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ f ∈ {f | ∀ (i : ι), p i → ↑f i ∈ A i} ↔ f ∈ DFunLike.coe ⁻¹' (Sᶜ ∩ {i | p i}).pi A
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)
x : (i : ι) → ↑(A i)
⊢ 𝓝 (structureMap R A cofinite x) = Filter.map (structureMap R A cofinite) (𝓝 x)

Tactic:
rw [isOpenEmbedding_structureMap hAopen |>.map_nhds_eq x]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (∏ x_1, ENNReal.ofReal (x ↑x_1)) *
          (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        ∏ i, volume (Set.Ioo (-π) π) ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume

Tactic:
volume_Ioo,

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (∏ x_1, ENNReal.ofReal (x ↑x_1)) *
          (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        ∏ x, ENNReal.ofReal (π - -π) ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ ↑a ≠ 0

Tactic:
by
  by_contra!
  exact a.prop.1.2 (this.symm ▸ mixedEmbedding.norm.map_zero')

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

Goal state before:
pp: case inr.inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
| inr hr =>

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ (completeBasis K) ↑i =
    ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))))

Tactic:
by
  rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_neg]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
hgs : ∑ i ∈ range n, ζ ^ i = 0
⊢ ↑n = ∑ i ∈ range n, (1 - ζ ^ i)

Tactic:
Finset.sum_sub_distrib,

Goal state after:
n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
hgs : ∑ i ∈ range n, ζ ^ i = 0
⊢ ↑n = ∑ x ∈ range n, 1 - ∑ x ∈ range n, ζ ^ x
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: p✝ : ℕ
A✝ : Type u_1
ζ✝ : A✝
inst✝³ : CommRing A✝
inst✝² : IsDomain A✝
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

Tactic:
have H : (i - j).Coprime p := (coprime_of_lt_prime (by grind) (by grind) hp).symm

Goal state after:
p✝ : ℕ
A✝ : Type u_1
ζ✝ : A✝
inst✝³ : CommRing A✝
inst✝² : IsDomain A✝
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
H : (i - j).Coprime p
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ (span {hζ✝.toInteger - 1}).ramificationIdx ℤ = p - 1

Tactic:
ramificationIdx_span_zeta_sub_one p 0 hζ,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ p ^ 0 * (p - 1) = p - 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
⊢ P.inertiaDeg ℤ = orderOf ↑p

Tactic:
by
  have : IsGalois ℚ K := isGalois {n} ℚ K
  rw [← inertiaDegIn_eq_inertiaDeg 𝒑 P Gal(K/ℚ), inertiaDegIn_eq n K hn hm]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
n : ℕ
h : 1 < n
hfm : f ↑m = ↑m ^ s
⊢ f ↑n = ↑n ^ logb (↑n) (f ↑n)

Tactic:
rw [rpow_logb (by positivity) (by norm_cast; omega)
        (map_pos_of_ne_zero f (by exact_mod_cast ne_zero_of_lt h))]

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : Algebra R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
n : ℕ
⊢ natGenerator v ∣ n ↔ ↑(natGenerator v) ∣ ↑n

Tactic:
exact Int.ofNat_dvd.symm

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)
x : X
⊢ ((contractSnd ν) (f.comp fst * g.comp snd)) x = ν g * f x

Tactic:
mul_comm (ν g) (f 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 = f x * ν g
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
a : Solution₁ d
⊢ ∃ b, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}

Tactic:
refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩) <;>
      simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Goal state after:
case refine_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ a.x < 0

case refine_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 ≤ a.y

case refine_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.x < 0

case refine_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.y ≤ 0

case refine_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ a.y ≤ 0
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
⊢ ∃ ia,
    True ∧
      ∀ x ∈ {x | (ValuativeRel.valuation (WithVal (valuation K v))) x < ↑ia},
        (algebraMap (WithVal (valuation K v)) (WithVal (valuation L w))) x ∈
          {x | (ValuativeRel.valuation (WithVal (valuation L w))) x < ↑γL}

Tactic:
let e := v.asIdeal.ramificationIdx' w.asIdeal

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
⊢ ∃ ia,
    True ∧
      ∀ x ∈ {x | (ValuativeRel.valuation (WithVal (valuation K v))) x < ↑ia},
        (algebraMap (WithVal (valuation K v)) (WithVal (valuation L w))) x ∈
          {x | (ValuativeRel.valuation (WithVal (valuation L w))) x < ↑γL}
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
⊢ πᵥ ≠ 0

Tactic:
by
  have := degree_lt_wf.min_mem _ (setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty hle)
  simp_all [uniformizingPolynomial]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
this : ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
⊢ (∑ a ∈ n.divisors,
      if a ∣ d then ∑ a_1 ∈ n.divisors, if a_1 ∣ d then if d = a.lcm a_1 then f a a_1 d else 0 else 0 else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

Tactic:
ite_sum_zero,

Goal state after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
this : ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
⊢ (∑ x ∈ n.divisors,
      ∑ x_1 ∈ n.divisors, if x ∣ d then if x_1 ∣ d then if d = x.lcm x_1 then f x x_1 d else 0 else 0 else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: weights : ℕ → ℝ
hw : weights 1 = 1
⊢ IsUpperMoebius (lambdaSquared weights)

Tactic:
dsimp only [IsUpperMoebius, lambdaSquared]

Goal state after:
weights : ℕ → ℝ
hw : weights 1 = 1
⊢ ∀ (n : ℕ),
    (if n = 1 then 1 else 0) ≤
      ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms l else 0) =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms (d / l) else 0

Tactic:
simp_rw [← sum_filter, Nat.divisors_filter_dvd_of_dvd prodPrimes_ne_zero hd,
        sum_div_divisors d s.selbergTerms]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ x ∈ s.prodPrimes.divisors,
      ∑ x_1 ∈ s.prodPrimes.divisors,
        ∑ a ∈ s.prodPrimes.divisors,
          if x ∣ x_1.gcd a then (selbergTerms x)⁻¹ * (s.nu x_1 * w x_1) * (s.nu a * w a) else 0) =
    ∑ x ∈ s.prodPrimes.divisors,
      ∑ a ∈ s.prodPrimes.divisors,
        if x ∣ a then
          ∑ a_1 ∈ s.prodPrimes.divisors, if x ∣ a_1 then (selbergTerms x)⁻¹ * (s.nu a * w a * (s.nu a_1 * w a_1)) else 0
        else 0

Tactic:
ite_sum_zero,

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ x ∈ s.prodPrimes.divisors,
      ∑ x_1 ∈ s.prodPrimes.divisors,
        ∑ a ∈ s.prodPrimes.divisors,
          if x ∣ x_1.gcd a then (selbergTerms x)⁻¹ * (s.nu x_1 * w x_1) * (s.nu a * w a) else 0) =
    ∑ x ∈ s.prodPrimes.divisors,
      ∑ x_1 ∈ s.prodPrimes.divisors,
        ∑ x_2 ∈ s.prodPrimes.divisors,
          if x ∣ x_1 then if x ∣ x_2 then (selbergTerms x)⁻¹ * (s.nu x_1 * w x_1 * (s.nu x_2 * w x_2)) else 0 else 0