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

Goal state before:
pp: case mpr.refine_1
a : SL(2, ℤ)
⊢ ((mapGL ℝ) (a * ModularGroup.T * a⁻¹)).IsParabolic

Tactic:
suffices (mapGL ℝ ModularGroup.T).IsParabolic by simpa
      refine ⟨fun ⟨a, ha⟩ ↦ zero_ne_one' ℝ (by simpa [ModularGroup.T] using congr_fun₂ ha 0 1), ?_⟩
      simp [discr_fin_two, trace_fin_two, det_fin_two, ModularGroup.T]
      norm_num

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
x✝ : ∃ x_1 ∈ Γ, (algebraMap ℤ ℝ).mapMatrix ↑x_1 = ↑(upperRightHom x)
g : SL(2, ℤ)
left✝ : g ∈ Γ
hg : (algebraMap ℤ ℝ).mapMatrix ↑g = ↑(upperRightHom x)
⊢ (fun x ↦ x • 1) (↑g 0 1) = x

Tactic:
simpa using congr_fun₂ hg 0 1

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

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
b : Fin 2 → ℤ
⊢ ‖↑(b 0) * ↑z + ↑(b 1)‖ ^ (-k) ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)

Tactic:
exact_mod_cast summand_bound z (show 0 ≤ (k : ℝ) by positivity) b

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
⊢ ∑' (n : ℕ+), ↑↑n ^ k * r ^ ↑n / (1 - r ^ ↑n) = ∑' (n : ℕ+), ↑((σ k) ↑n) * r ^ ↑n

Tactic:
by
  have (m : ℕ) [NeZero m] := tsum_geometric_of_norm_lt_one (ξ := r ^ m)
    (by simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _))
  simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
    ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (f := fun m ↦ n ^ k * (r ^ n) ^ m)]
  have h00 := tsum_prod_pow_eq_tsum_sigma k hr
  rw [Summable.tsum_comm (by apply (summable_prod_mul_pow k hr).prod_symm)] at h00
  rw [← h00]
  exact tsum_congr₂ <| fun b c ↦ by simp [mul_comm c.val b.val, pow_mul]

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

Goal state before:
pp: this :
  (Summable fun n ↦ (1 / 2) ^ (n + 1)) →
    (∀ (k : ℕ), Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
⊢ Summable fun n ↦ (1 / 2) ^ (n + 1)

Tactic:
simpa only [pow_succ'] using (summable_geometric_of_abs_lt_one (by norm_num)).mul_left _

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

Goal state before:
pp: ⊢ IsZeroAtImInfty Δ

Tactic:
apply Tendsto.congr (fun z ↦ (discriminant_eq_q_prod z).symm)
  rw [show (0 : ℂ) = 0 * 1 by ring]
  exact (qParam_tendsto_atImInfty zero_lt_one).mul
    (tendsto_atImInfty_tprod_one_sub_eta_q_pow.congr fun z ↦ by congr 1)

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

Goal state before:
pp: case h.inl.«2»
k : ℕ
ihn :
  ∀ m < 2,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 2
hk : 2 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑2) =
    ↑(if 2 ≡ 2 [MOD 12] then 2 / 12 else 2 / 12 + 1)

Tactic:
simpa [Nat.ModEq] using levelOne_weight_two_rank_zero

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ Summable fun x ↦ eisSummand ↑k ![x.1, x.2] z

Tactic:
refine (finTwoArrowEquiv ℤ).summable_iff.mp <| (summable_eisSummand hk z).congr (fun v ↦ ?_)
  simp [show ![v 0, v 1] = v from List.ofFn_inj.mp rfl]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
x : ℕ
i : ℤ
hi : i ∈ Ico (-↑x) ↑x
⊢ Summable fun n ↦ 1 / (↑n * ↑z + ↑i) ^ 2

Tactic:
by simpa using! linear_left_summable (ne_zero z) i le_rfl

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : S • z = z
⊢ z = I

Tactic:
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

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : I = z ∨ ↑I = -↑z
⊢ z = I
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
⊢ jacobiTheta₂ 0 (τ + 2) = jacobiTheta₂ 0 τ

Tactic:
jacobiTheta₂_add_right

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

Goal state before:
pp: 𝒮ℒ' : Subgroup SL(2, ℝ) := (SpecialLinearGroup.map (Int.castRingHom ℝ)).range
this : ProperlyDiscontinuousSMul ↥𝒮ℒ' ℍ
⊢ ProperlyDiscontinuousSMul ↥(SpecialLinearGroup.mapGL ℝ).range ℍ

Tactic:
simp only [Subgroup.properlyDiscontinuousSMul_iff] at this ⊢

Goal state after:
𝒮ℒ' : 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 ℍ},
    IsCompact K → IsCompact L → {g | g ∈ (SpecialLinearGroup.mapGL ℝ).range ∧ (g • K ∩ L).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A✝ : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i : ι
x : G i
⊢ ∀ᶠ (i_1 : ι) in cofinite, Pi.mulSingle i x i_1 ∈ (fun i ↦ ↑(A i)) i_1

Tactic:
filter_upwards [show {i}ᶜ ∈ Filter.cofinite by simp]

Goal state after:
ι : Type u_1
R : ι → Type u_2
A✝ : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i : ι
x : G i
⊢ ∀ a ∈ {i}ᶜ, Pi.mulSingle i x a ∈ ↑(A a)
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⟩
i : ι
h : x i ∈ B i
hu✝ : IsUnit ⟨x i, h⟩
hu : ↑⋯.unit * ↑hu✝.unit.inv = 1
⊢ ⋯.unit.inv ∈ ↑(B i)

Tactic:
simp [← Units.eq_inv_of_mul_eq_one_left hu]

Goal state after:
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⟩
⊢ IsUnit x

Tactic:
by
  rw [isUnit_iff_exists]
  use .mk (fun i ↦ (hx i).unit.inv) (by
    filter_upwards [hxr] with i ⟨h, hu⟩
    have hu : (hx i).unit.1 * hu.unit.inv = 1 := Subtype.val_inj.2 hu.mul_val_inv
    simp [← Units.eq_inv_of_mul_eq_one_left hu])
  simp [RestrictedProduct.ext_iff]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ Odd y

Tactic:
← even_iff_two_dvd,

Goal state after:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬Even x
hn : Even n
⊢ Odd y
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)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
by
    set S := {i | IsCompact (A i) ∧ x i ∈ A i}
    have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr (hAcompact.and x.2)
    have hSx : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi.2
    have hSA : ∀ i ∈ S, IsCompact (A i) := fun i hi ↦ hi.1
    have := weaklyLocallyCompactSpace_of_principal hS hSA
    rcases exists_inclusion_eq_of_eventually R A hS hSx with ⟨x', hxx'⟩
    rw [← hxx', nhds_eq_map_inclusion hAopen]
    rcases exists_compact_mem_nhds x' with ⟨K, K_compact, hK⟩
    exact ⟨inclusion R A hS '' K, K_compact.image (continuous_inclusion hS), image_mem_map hK⟩

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬2 ∣ x ^ 2

Tactic:
← even_iff_two_dvd,

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬Even (x ^ 2)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
⊢ ∀ (hS : 𝓕₁ ≤ 𝓟 S),
    Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS)

Tactic:
hS

Goal state after:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑(polarCoordReal K).symm

Tactic:
by
  refine measurable_fst.prodMk <| Measurable.comp ?_ measurable_snd
  exact measurable_pi_lambda _
    fun _ ↦ continuous_polarCoord_symm.measurable.comp (measurable_pi_apply _)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) = normAtComplexPlaces (mixedSpaceOfRealSpace x.1)

Tactic:
by
  ext w
  obtain hw | hw := isReal_or_isComplex w
  · simp [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]
  · simp [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ |(of (Subtype.val ∘ ⇑(Basis.restrictScalars ℤ (basisOfIsMaxRank hu)) ∘ ⇑(equivFinRank K).symm)).det| =
    |(of fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))).det|

Tactic:
congr 3 with i

Goal state after:
case pos.e_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
i x✝ : { w // w ≠ w₀ }
⊢ (Subtype.val ∘ ⇑(Basis.restrictScalars ℤ (basisOfIsMaxRank hu)) ∘ ⇑(equivFinRank K).symm) i x✝ =
    (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i))) x✝
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 : polarSpace K) in
      (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π,
      (∏ w, ENNReal.ofReal (x.1 ↑w)) * A.indicator 1 (↑(polarSpaceCoord K).symm x) ∂volume.prod volume =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
setLIntegral_prod

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,
      ∫⁻ (y : { w // w.IsComplex } → ℝ) in Set.univ.pi fun x ↦ Set.Ioo (-π) π,
        (∏ w, ENNReal.ofReal ((x, y).1 ↑w)) * A.indicator 1 (↑(polarSpaceCoord K).symm (x, y)) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

case hf
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)
⊢ AEMeasurable (fun x ↦ (∏ w, ENNReal.ofReal (x.1 ↑w)) * A.indicator 1 (↑(polarSpaceCoord K).symm x))
    ((volume.prod volume).restrict
      ((Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π))
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
φ : K →+* ℂ
σ : Gal(K/↥K⁺)
hσ : ComplexEmbedding.IsConj φ σ
this : ComplexEmbedding.IsConj (Classical.choice ⋯) ⋯.choose
⊢ ComplexEmbedding.IsConj φ (complexConj K)

Tactic:
rwa [isConj_eq_isConj K hσ this] at hσ

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)) *
        ENNReal.ofReal (2 * π) ^ Finset.univ.card ∂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:
Finset.card_univ,

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)) *
        ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } ∂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.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (completeBasis K) w₀ = fun w ↦ ↑w.mult

Tactic:
completeBasis,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯) w₀ = fun w ↦ ↑w.mult
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:
completeBasis,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ (basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯) ↑i =
    ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : Fin (rank K)
⊢ ↑((basisUnitLattice K) x✝) = (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) x✝

Tactic:
Basis.ofZLatticeBasis_apply

Goal state after:
case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : Fin (rank K)
⊢ ↑((basisUnitLattice K) x✝) = ↑((basisUnitLattice K) x✝)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
by
  simp_rw [expMapBasis_apply', Pi.smul_def, smul_eq_mul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq, ← prod_pow]
  rw [prod_comm]
  simp_rw [Real.rpow_pow_comm (apply_nonneg _ _), Real.finsetProd_rpow _ _
    fun _ _ ↦ pow_nonneg (apply_nonneg _ _) _, prod_eq_abs_norm, Units.norm, Rat.cast_one,
    Real.one_rpow, prod_const_one, mul_one]

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

Goal state before:
pp: case refine_2
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)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
this : root P ^ (p ^ f) ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = root P
⊢ ↑(unitOfCoprime (p ^ f) ⋯ ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P))) = ↑1

Tactic:
rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_one]

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

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x_1, Real.exp ((↑x_1.mult)⁻¹ * (completeBasis K).equivFun.symm x x_1) =
    (∏ w, ↑expMapBasis x w ^ w.mult) * (∏ w, ↑expMapBasis x ↑w)⁻¹

Tactic:
prod_eq_prod_mul_prod,

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∏ w, Real.exp ((↑(↑w).mult)⁻¹ * (completeBasis K).equivFun.symm x ↑w)) *
      ∏ w, Real.exp ((↑(↑w).mult)⁻¹ * (completeBasis K).equivFun.symm x ↑w) =
    ((∏ w, ↑expMapBasis x ↑w ^ (↑w).mult) * ∏ w, ↑expMapBasis x ↑w ^ (↑w).mult) * (∏ w, ↑expMapBasis x ↑w)⁻¹
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
S : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) S ∈ monicFactorsMod θ p
⊢ (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) S, hQ⟩)).ramificationIdx
      ℤ =
    multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) S) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
rw [ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : (I.rootsOfUnityMapQuot n) ⟨ζ, hζ✝⟩ = 1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
⊢ False

Tactic:
let μ : K := ζ.val

Goal state after:
K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : (I.rootsOfUnityMapQuot n) ⟨ζ, hζ✝⟩ = 1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := ↑↑ζ
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: 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))
this✝ : IsGalois ℚ K
this : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))
⊢ span {hζ.toInteger - 1} ^ Finset.univ.card = span {hζ.toInteger - 1} ^ Module.finrank ℚ K

Tactic:
Finset.card_univ,

Goal state after:
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))
this✝ : IsGalois ℚ K
this : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))
⊢ span {hζ.toInteger - 1} ^ Fintype.card (𝓞 K ≃ₐ[ℤ] 𝓞 K) = span {hζ.toInteger - 1} ^ Module.finrank ℚ K
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) ^ (p - 1)) ↑p

Tactic:
by
  rw [← eval_one_cyclotomic_prime (R := 𝓞 K) (p := p),
    cyclotomic_eq_prod_X_sub_primitiveRoots hζ.toInteger_isPrimitiveRoot, eval_prod]
  simp only [eval_sub, eval_X, eval_C]
  rw [← Nat.totient_prime hp.out, ← hζ.toInteger_isPrimitiveRoot.card_primitiveRoots,
    ← Finset.prod_const]
  refine Associated.prod _ _ _ fun η hη ↦ ?_
  have hη' : IsPrimitiveRoot (η : K) p :=
    (isPrimitiveRoot_of_mem_primitiveRoots hη).map_of_injective RingOfIntegers.coe_injective
  simpa using (associated_sub_one_of_isPrimitiveRoot p hζ hη').neg_right

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
⊢ IsBounded (normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K)

Tactic:
obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
C : ℝ
hC : ∀ x ∈ ↑expMapBasis '' paramSet K, ‖x‖ ≤ C
⊢ IsBounded (normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K)
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', house α

Tactic:
by gcongr; apply norm_embedding_le_house

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

Goal state before:
pp: case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
      (↑(torsionOrder K) * √|↑(discr K)|) =
    Finset.univ.card •
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|))

Tactic:
Finset.card_univ,

Goal state after:
case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
      (↑(torsionOrder K) * √|↑(discr K)|) =
    Fintype.card (ClassGroup (𝓞 K)) •
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|))