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

Goal state before:
pp: ⊢ IsOpen 𝒟ᵒ

Tactic:
refine .inter (.preimage (by fun_prop) isOpen_Ioi) ?_
  exact isOpen_lt (f := fun z : ℍ ↦ |z.re|) (by fun_prop) continuous_const

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
⊢ HasSum (fun m ↦ c m • 𝕢 1 ↑τ ^ m) ((E hk) τ)

Tactic:
have hS : Summable fun n : ℕ ↦ (σ (k - 1) (n + 1) : ℂ) * cexp (2 * π * I * τ) ^ (n + 1) :=
    (summable_nat_add_iff 1).mpr (summable_sigma_mul_cexp_pow (by omega) τ)

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ HasSum (fun m ↦ c m • 𝕢 1 ↑τ ^ m) ((E hk) τ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ ‖↑x‖ ∈ Set.Ioi 1

Tactic:
← interior_Ici

Goal state after:
case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ ‖↑x‖ ∈ interior (Set.Ici 1)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ 1 = fun x ↦ ∏ i, 1

Tactic:
ext; simp

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
this :
  f (↑ofComplex (I * ↑t⁻¹)) =
    I ^ k * ↑t ^ k *
      (f
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
            ↑ofComplex (I * ↑t)) *
        ↑(↑ofComplex (I * ↑t)) ^ (-k))
⊢ f (↑ofComplex (I * ↑(1 / t))) =
    (I ^ k * ↑(t ^ ↑k)) •
      (fun τ ↦
          (σ (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))
                (f
                  (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
                    τ)) *
              ↑|↑(Matrix.GeneralLinearGroup.det
                        (Matrix.SpecialLinearGroup.toGL
                          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))| ^
                (k - 1) *
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
                ↑τ ^
              (-k))
        (↑ofComplex (I * ↑t))

Tactic:
by
      simpa [σ, denom]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
i : ℕ
⊢ ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)

Tactic:
calc
      ↑p ^ 2 ∣ (↑p * b) ^ 2 := by simp only [mul_pow, dvd_mul_right]
      _ ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) := by
        simp only [sq_dvd_add_pow_sub_sub (↑p * b) a i, ← sub_sub]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) 0) } = 0

Tactic:
ext; simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) 1) } = 1

Tactic:
ext; simp

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

Goal state before:
pp: case refine_2
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
⊢ Summable fun i ↦ ‖(PowerSeries.coeff i) (qExpansion (h Γ) ⇑f)‖ / (2 * ↑i / h Γ) ^ s.re

Tactic:
· -- show summability of Dirichlet series
    simp_rw [mul_comm (2 : ℝ), mul_div_assoc,
      Real.mul_rpow (Nat.cast_nonneg _) (show 0 ≤ 2 / h Γ by positivity), ← div_div]
    apply Summable.div_const
    apply summable_of_isBigO_nat (Real.summable_nat_rpow.mpr <| show r - s.re < -1 by linarith)
    simp only [Real.rpow_sub' (Nat.cast_nonneg _) (show r - s.re ≠ 0 by linarith)]
    apply IsBigO.mul _ (isBigO_refl _ _)
    simpa using hcoeff.norm_left

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

Goal state before:
pp: ι : Type u_1
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 : ι
⊢ DFunLike.coe ∘ mulSingle A i = Pi.mulSingle i

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
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 : ι
⊢ mulSingle A i 1 = 1

Tactic:
ext; simp

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)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
⊢ ⟨fun i ↦ ↑(x i), ⋯⟩ * ⟨fun i ↦ ↑(x i)⁻¹, ⋯⟩ = 1

Tactic:
ext; simp

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)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
⊢ ⟨fun i ↦ ↑(x i)⁻¹, ⋯⟩ * ⟨fun i ↦ ↑(x i), ⋯⟩ = 1

Tactic:
ext; simp

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

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

Tactic:
by
    rw [le_principal_iff, mem_cofinite] at hS
    classical
    have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
    choose K K_compact hK using this
    set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def
    have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
    set U : Set (Π i, R i) := Sᶜ.pi K
    have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
    have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦ by
      dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i hi
    refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
    · refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact
      simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]
      exact inter_subset_left
    · simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
ha₀ : ∀ (v : HeightOneSpectrum R), a v ≠ 0
ha : {v | Valued.v (a v) ≠ 1}.Finite
⊢ IsUnit a

Tactic:
rw [isUnit_iff]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
ha₀ : ∀ (v : HeightOneSpectrum R), a v ≠ 0
ha : {v | Valued.v (a v) ≠ 1}.Finite
⊢ (∀ (v : HeightOneSpectrum R), a v ≠ 0) ∧ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, Valued.v (a v) = 1
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
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 : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr (hAcompact.and x.2)

Goal state after:
ι : 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 : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
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 : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, x i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 (inclusion R A hS x')

Tactic:
nhds_eq_map_inclusion hAopen

Goal state after:
ι : 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 : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, x i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ ∃ s, IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ mixedEmbedding.norm (u • x) = mixedEmbedding.norm x

Tactic:
rw [unitSMul_smul, map_mul, norm_unit, one_mul]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ logMap 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ logMap 1 = 0

Tactic:
ext; simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) = (logEmbedding K) (Additive.ofMul u)

Tactic:
ext; simp

Goal state after:
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
⊢ complexConj K ^ 2 = 1

Tactic:
ext; simp

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 : 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)
⊢ (logEmbedding K) (Additive.ofMul u) = 0

Tactic:
refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_

Goal state after:
case refine_1
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)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ Submodule.span ℤ (Set.range ⇑B)

case refine_2
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)
⊢ ⟨(logEmbedding K) (Additive.ofMul u), ?refine_1⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

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)
⊢ ⟨0, ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B
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)ˣ
⊢ (∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑↑u) ↔ ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u

Tactic:
Units.coe_coe

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u) ↔ ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
Module: Mathlib.NumberTheory.NumberField.CMField

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

Tactic:
by
  ext
  rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]

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 : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w // w.IsReal }
⊢ {x | x ↑w ≠ 0}ᶜ = {x | x ↑w = 0}

Tactic:
ext; simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑((Trans.trans (Trans.trans ((integerSetEquiv K).subtypeEquiv ⋯) Equiv.prodSubtypeFstEquivSubtypeProd)
              (Equiv.prodCongrLeft fun x ↦
                Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n))
            a).1 =
    Ideal.span {↑(preimageOfMemIntegerSet ↑a)}

Tactic:
Equiv.prodSubtypeFstEquivSubtypeProd,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑((Trans.trans
              (Trans.trans ((integerSetEquiv K).subtypeEquiv ⋯)
                { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, (↑x).2), invFun := fun x ↦ ⟨(↑x.1, x.2), ⋯⟩, left_inv := ⋯,
                  right_inv := ⋯ })
              (Equiv.prodCongrLeft fun x ↦
                Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n))
            a).1 =
    Ideal.span {↑(preimageOfMemIntegerSet ↑a)}
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 : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w // w.IsReal }
⊢ volume {x | x ↑w = 0} = 0

Tactic:
exact realSpace.volume_eq_zero w.1

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ indexRealUnits K = 2 ↔ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤

Tactic:
by
  suffices (∃ u : (𝓞 K)ˣ, Subgroup.zpowers (unitsMulComplexConjInv K u) = ⊤) ↔
      (unitsMulComplexConjInv K).range.index = 1 by
    rw [this]
    have h_eq := indexRealUnits_mul_eq K
    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · rwa [h, Nat.mul_eq_left two_ne_zero] at h_eq
    · rwa [h, mul_one] at h_eq
  refine ⟨fun ⟨u, hu⟩ ↦ Subgroup.index_eq_one.mpr (top_le_iff.mp ?_), fun h ↦ ?_⟩
  · refine le_of_eq_of_le ?_ ((Subgroup.zpowers u).map_le_range (unitsMulComplexConjInv K))
    rw [MonoidHom.map_zpowers, ← hu]
  · obtain ⟨ζ, hζ⟩ := exists_zpow_surjective (torsion K)
    rw [Subgroup.index_eq_one, MonoidHom.range_eq_top] at h
    obtain ⟨u, rfl⟩ := h ζ
    exact ⟨u, (Subgroup.eq_top_iff' _).mpr hζ⟩

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

Goal state before:
pp: 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 : IsRamified K w
H : w.IsComplex ∧ v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
⊢ (algebraMap ℝ ℂ).comp (ringEquivRealOfIsReal ⋯).toRingHom =
    (ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)

Tactic:
ext; simp

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

Goal state before:
pp: 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
hl : w.embedding.comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
⊢ (algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom =
    (ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)

Tactic:
ext; simp

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

Goal state before:
pp: case 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
hv : v = w.comap (algebraMap K L)
h : IsRamified K w
⊢ v.mult * Module.finrank v.Completion w.Completion = w.mult

Tactic:
h.finrank_eq_two v,

Goal state after:
case 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
hv : v = w.comap (algebraMap K L)
h : IsRamified K w
⊢ v.mult * 2 = w.mult
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
⊢ (algebraMap F K).comp (CMExtension.equivMaximalRealSubfield F K).symm.toRingHom =
    (RingEquiv.refl K).toRingHom.comp (algebraMap (↥(maximalRealSubfield K)) K)

Tactic:
ext; simp

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
⊢ φ.comp (algebraMap ℚ K) = ψ.comp (algebraMap ℚ K)

Tactic:
ext; simp

Goal state after:
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 θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
⊢ (algebraMap (ZMod p) ((ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})).comp
      (Int.quotientSpanNatEquivZMod p).toRingHom =
    (RingEquiv.toRingHom ?m.136).comp (algebraMap (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}))

Tactic:
ext; simp

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

Goal state before:
pp: case hx
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ (algebraMap F K) 1 = 1

Tactic:
map_one

Goal state after:
case hx
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ 1 = 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
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝⁴ : IsAbelianGalois ℚ K
this✝³ : NeZero m
this✝² : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝¹ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
⊢ 𝒑.inertiaDegIn (𝓞 ↥Fₘ) * Pₘ.inertiaDegIn (𝓞 K) = orderOf ↑p ∧
    𝒑.ramificationIdxIn (𝓞 ↥Fₚ) * Pₚ.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
Nat.eq_one_of_mul_eq_one_left this,

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
this✝³ : NeZero m
this✝² : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝¹ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
⊢ 𝒑.inertiaDegIn (𝓞 ↥Fₘ) * 1 = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 ↥Fₚ) * Pₚ.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)