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

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
⊢ g = 1 ∨ g = -1

Tactic:
by
  have : T • z ≠ z := by
    apply_fun UpperHalfPlane.re
    simp [-sl_moeb, re_T_smul]
  have : T⁻¹ • z ≠ z := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
  have : (z : ℂ) ≠ -I := by grind [neg_im, coe_I, Complex.I_im, z.coe_im_pos]
  have : S • z ≠ z := by
    contrapose hzI
    rw [UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, ← mul_one (_ : ℂ)⁻¹,
      inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr z.ne_zero), neg_mul, ← neg_eq_iff_eq_neg, ← I_sq,
      ← sq, sq_eq_sq_iff_eq_or_eq_neg, ← coe_I, ← UpperHalfPlane.ext_iff] at hzI
    grind
  all_goals grind [cases_of_mem_fd_smul_mem_fd hz (hg ▸ hz), SL_neg_smul]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
h : 1 +ᵥ ρ ∈ 𝒟ᵒ
⊢ (1 +ᵥ ρ).re = 1 / 2

Tactic:
norm_num [← coe_re, coe_vadd, ρ]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

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

Tactic:
simp_rw [mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

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

Goal state before:
pp: ⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄CubeSubE₆SqForm) = 1728

Tactic:
rw [E₄CubeSubE₆SqForm_qExpansion_eq]
  norm_num [PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ, E₄_qExpansion_coeff_one,
    E₆_qExpansion_coeff_one, E_qExpansion_coeff_zero _ ⟨2, rfl⟩,
    E_qExpansion_coeff_zero _ ⟨3, rfl⟩]

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
⊢ ∃ c, ⇑f = Function.const ℍ c

Tactic:
have : ModularForm.norm 𝒮ℒ (f - .const (f I)) I = 0 := by
    simpa [Finset.prod_eq_zero_iff, QuotientGroup.exists_mk] using ⟨1, by simp⟩

Goal state after:
𝒢 : 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, ⇑f = Function.const ℍ c
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ∃ c, ⇑f = Function.const ℍ c

Tactic:
by
  -- Consider the norm of `f - (f I)`. This must be a constant, since it's a weight 0 level 1 form.
  let : ModularFormClass (ModularForm 𝒮ℒ (0 * Nat.card (𝒮ℒ ⧸ 𝒢.subgroupOf 𝒮ℒ))) 𝒮ℒ 0 := by
    rw [zero_mul]; infer_instance
  obtain ⟨c, hc⟩ := ModularFormClass.levelOne_weight_zero_const
    (ModularForm.norm 𝒮ℒ (f - .const (f I)))
  -- But the constant must be 0, since `f - f I` vanishes at `I`.
  have : ModularForm.norm 𝒮ℒ (f - .const (f I)) I = 0 := by
    simpa [Finset.prod_eq_zero_iff, QuotientGroup.exists_mk] using ⟨1, by simp⟩
  obtain rfl : c = 0 := by simpa [hc]
  -- So `f - f I` has zero norm, hence it's the zero form.
  simp only [Function.const_zero, FunLike.coe_zero_iff, norm_eq_zero_iff, sub_eq_zero] at hc
  exact ⟨f I, by rw [hc, ModularForm.coe_const, Function.const_apply]⟩

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

Tactic:
rw [Nat.cast_zero, mul_zero, mul_zero]

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

Goal state before:
pp: case ofCompletion.ofCompletion
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
toCompletion✝¹ toCompletion✝ : (↑v).Completion
h : { toCompletion := toCompletion✝¹ }.toCompletion = { toCompletion := toCompletion✝ }.toCompletion
⊢ { toCompletion := toCompletion✝¹ } = { toCompletion := toCompletion✝ }

Tactic:
exact congrArg ofCompletion h

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 + 1) - y ^ p ^ (a + 1)) = emultiplicity (↑p) (x - y) + ↑(a + 1)

Tactic:
rw [Nat.cast_add, Nat.cast_one, ← add_assoc, ← h_ind, pow_succ, pow_mul, pow_mul]
    apply emultiplicity_pow_prime_sub_pow_prime hp hp1
    · rw [← geom_sum₂_mul]
      exact dvd_mul_of_dvd_right hxy _
    · exact fun h => hx (hp.dvd_of_dvd_pow h)

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

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] := fun j ↦ mk (fun i ↦ (x j) i) ⋯
hxx' : Pi.map (fun j ↦ inclusion (A j) (C j) hS) x' = x
⊢ Tendsto f (𝓝 (Pi.map (fun j ↦ inclusion (A j) (C j) hS) x')) (𝓝 (f (Pi.map (fun j ↦ inclusion (A j) (C j) hS) x')))

Tactic:
nhds_pi,

Goal state after:
ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] := fun j ↦ mk (fun i ↦ (x j) i) ⋯
hxx' : Pi.map (fun j ↦ inclusion (A j) (C j) hS) x' = x
⊢ Tendsto f (Filter.pi fun i ↦ 𝓝 (Pi.map (fun j ↦ inclusion (A j) (C j) hS) x' i))
    (𝓝 (f (Pi.map (fun j ↦ inclusion (A j) (C j) hS) x')))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (Subgroup.toAddSubgroup (Subgroup.closure (⇑(QuotientGroup.mk' (torsion K)) '' Set.range u)))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (Set.range (⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))).index ≠
      0

Tactic:
toAddSubgroup_closure,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (AddSubgroup.closure (⇑Additive.toMul ⁻¹' ⇑(QuotientGroup.mk' (torsion K)) '' Set.range u))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (Set.range (⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))).index ≠
      0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * (normAtPlace ↑x✝) x) -
        Real.log (↑1 * mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)

Tactic:
Rat.cast_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * (normAtPlace ↑x✝) x) -
        Real.log (1 * mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
⊢ Setoid.ker (integerSetToAssociates K) = MulAction.orbitRel ↥(torsion K) ↑(integerSet K)

Tactic:
ext a b

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
⊢ (Setoid.ker (integerSetToAssociates K)) a b ↔ (MulAction.orbitRel ↥(torsion K) ↑(integerSet K)) a b
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
⊢ { a // ↑(preimageOfMemIntegerSet ↑a) ∈ ↑J } ≃ { I // ↑J ∣ ↑↑I.1 }

Tactic:
by
      convert! Equiv.subtypeEquivOfSubtype (p := fun I ↦ J.1 ∣ I.1) (integerSetEquivNorm K n)
      rw [integerSetEquivNorm_apply_fst, dvd_span_singleton]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
i✝ : Fin (rank K)
⊢ Real.log ↑1 = 0

pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
i✝ : Fin (rank K)
⊢ ∀ x ∈ Finset.univ, (f x) ((algebraMap (𝓞 K) K) ↑(u i✝)) ^ (f x).mult ≠ 0

Tactic:
Rat.cast_one,

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
i✝ : Fin (rank K)
⊢ Real.log 1 = 0

case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
i✝ : Fin (rank K)
⊢ ∀ x ∈ Finset.univ, (f x) ((algebraMap (𝓞 K) K) ↑(u i✝)) ^ (f x).mult ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : { w // w ≠ w₀ }
⊢ Real.log ↑1 = 0

Tactic:
Rat.cast_one,

Goal state after:
case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : { w // w ≠ w₀ }
⊢ Real.log 1 = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ |((LinearMap.toMatrix (completeBasis K) (completeBasis K)) ↑↑(completeBasis K).equivFunL.symm).det| =
    ↑(finrank ℚ K) * regulator K

Tactic:
← Matrix.det_transpose,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ |((LinearMap.toMatrix (completeBasis K) (completeBasis K)) ↑↑(completeBasis K).equivFunL.symm).transpose.det| =
    ↑(finrank ℚ K) * regulator K
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)
⊢ NeZero ↑n

Tactic:
suffices NeZero (n : K) by
        simpa using! NeZero.of_injective (algebraMap K (AdjoinRoot P)).injective

Goal state after:
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)
⊢ NeZero ↑n
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ Real.exp (x w₀) ^ finrank ℚ K * ∏ x_1, ↑1 ^ x ↑x_1 = Real.exp (x w₀) ^ finrank ℚ K

Tactic:
Rat.cast_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ Real.exp (x w₀) ^ finrank ℚ K * ∏ x_1, 1 ^ x ↑x_1 = Real.exp (x w₀) ^ finrank ℚ K
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)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ P * A = P * (C P.leadingCoeff⁻¹ * C P.leadingCoeff) * A

Tactic:
simp [← C_mul, leadingCoeff_ne_zero.mpr hPirr.ne_zero]

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

Goal state before:
pp: case hp
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : (span {hζ.toInteger - 1}).IsPrime
hp0 : 𝒑 ≠ ⊥
⊢ map (algebraMap ℤ (𝓞 K)) 𝒑 ≠ ⊥

Tactic:
exact map_ne_bot_of_ne_bot hp0

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (primitiveRoots p (𝓞 K)).card) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))

Tactic:
← Finset.prod_const

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated (∏ _x ∈ primitiveRoots p (𝓞 K), (hζ.toInteger - 1)) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: 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
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ↑((galEquivZMod n K) σ) = ↑(ZMod.unitOfCoprime p hn ^ i)
h₀ : IsPrimitiveRoot ((Ideal.Quotient.mk P) hζ.toInteger) n
h₁ :
  ((IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩)
      ((Ideal.Quotient.mk P) hζ.toInteger) =
    (Ideal.Quotient.mk P) (σ • hζ.toInteger)
⊢ (fun x ↦ ZMod.unitOfCoprime p hn ^ x) ↑i = (galEquivZMod n K) σ

Tactic:
← Units.ext_iff,

Goal state after:
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
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : (galEquivZMod n K) σ = ZMod.unitOfCoprime p hn ^ i
h₀ : IsPrimitiveRoot ((Ideal.Quotient.mk P) hζ.toInteger) n
h₁ :
  ((IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩)
      ((Ideal.Quotient.mk P) hζ.toInteger) =
    (Ideal.Quotient.mk P) (σ • hζ.toInteger)
⊢ (fun x ↦ ZMod.unitOfCoprime p hn ^ x) ↑i = (galEquivZMod n K) σ
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
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
have : IsAbelianGalois ℚ K := IsCyclotomicExtension.isAbelianGalois {n} ℚ K

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this : IsAbelianGalois ℚ K
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    (2 ^ nrRealPlaces K).toReal * (↑NNReal.pi ^ nrComplexPlaces K).toReal * (ENNReal.ofReal (regulator K)).toReal /
        (↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)

Tactic:
ENNReal.toReal_pow,

Goal state after:
case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    ENNReal.toReal 2 ^ nrRealPlaces K * (↑NNReal.pi ^ nrComplexPlaces K).toReal *
          (ENNReal.ofReal (regulator K)).toReal /
        (↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    ENNReal.toReal 2 ^ nrRealPlaces K * (↑NNReal.pi ^ nrComplexPlaces K).toReal *
          (ENNReal.ofReal (regulator K)).toReal /
        (↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)

Tactic:
ENNReal.toReal_pow,

Goal state after:
case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    ENNReal.toReal 2 ^ nrRealPlaces K * (↑NNReal.pi).toReal ^ nrComplexPlaces K *
          (ENNReal.ofReal (regulator K)).toReal /
        (↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)