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
⊢ D (F ∣[k] g) = fun z ↦
    (↑(↑g).det)⁻¹ * (D F ∣[k + 2] g) z - ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F ∣[k] g) z

Tactic:
have hdet : g.det.val = g.val.det := Matrix.GeneralLinearGroup.val_det_apply g

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
⊢ D (F ∣[k] g) = fun z ↦
    (↑(↑g).det)⁻¹ * (D F ∣[k + 2] g) z - ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F ∣[k] g) z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
h0 : (fun n ↦ 1) =O[atTop] fun n ↦ ↑n ^ 1
⊢ SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) ℍₒ

Tactic:
simpa using summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp k 1 (p := 1)
    (by norm_num) h0

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

Goal state before:
pp: case e'_2.a
z : ℂ
m : ℤ
b : ℕ
x✝ : ℤ
a✝ : x✝ ∈ Ico (-↑b) ↑b
⊢ 1 / (↑m * z + ↑x✝) - 1 / (↑m * z + ↑x✝ + 1) = 1 / (↑m * z + ↑x✝) - 1 / (↑m * z + ↑(x✝ + 1))

Tactic:
simp [add_assoc, sub_eq_add_neg]

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

Goal state before:
pp: case e'_3.e'_5
z : ℂ
m : ℤ
b : ℕ
⊢ 1 / (↑m * z - ↑b) = 1 / (↑m * z + ↑(-↑b))

Tactic:
simp [add_assoc, sub_eq_add_neg]

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ (1 / 2) • ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z =
    1 +
      (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n

Tactic:
have HE1 := tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow hk hk2 z

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
⊢ (1 / 2) • ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z =
    1 +
      (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n
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 ℋ)
⊢ ((∏ q, quotientFunc f q) ∣[k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ) =O[atImInfty] 1

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
𝒢 ℋ : 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 ℋ)
⊢ ((∏ q, quotientFunc f q) ∣[k * ↑(Fintype.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ) =O[atImInfty] 1
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ProperlyDiscontinuousSMul (↥H) α
inst✝ : H.IsFiniteRelIndex G
⊢ ProperlyDiscontinuousSMul (↥G) α

Tactic:
rw [Subgroup.properlyDiscontinuousSMul_iff] at hH ⊢

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
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
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
⊢ HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s)
    (mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s)

Tactic:
refine hasSum_mellin_pi_mul₀ (fun _ ↦ by positivity) hpos ?_ ?_

Goal state after:
case refine_1
Γ : 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
⊢ ∀ t ∈ Set.Ioi 0,
    HasSum
      (fun i ↦
        if 2 * ↑i / h Γ = 0 then 0 else (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑i / h Γ) * t)))
      ((weakFEPair hk f).f t - (weakFEPair hk f).f₀)

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
Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ‖(algebraMap K K∞) x‖ = ↑|(Algebra.norm ℚ) x|

Tactic:
by
  simpa [-Rat.cast_abs, norm_def] using! InfinitePlace.prod_eq_abs_norm x

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
⊢ v ∈ {v | (valuation K v) ((algebraMap R K) d) < 1}

Tactic:
Set.mem_ofPred_eq,

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
⊢ (valuation K v) ((algebraMap R K) d) < 1
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}
⊢ ∀ᶠ (i : ι) in cofinite, ∀ (j : n), (x j) i ∈ C j i

Tactic:
simp [-eventually_cofinite]

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)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝³ i] ↑(B i))
inst✝² : (i : ι) → Mul (R i)
inst✝¹ : ∀ (i : ι), MulMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousMul (R i)
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite] fun p ↦ p.1 * p.2

Tactic:
continuous_dom_prod hBopen.out hBopen.out

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝³ i] ↑(B i))
inst✝² : (i : ι) → Mul (R i)
inst✝¹ : ∀ (i : ι), MulMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousMul (R i)
⊢ ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite]
      ((fun p ↦ p.1 * p.2) ∘ Prod.map (inclusion R (fun i ↦ ↑(B i)) hS) (inclusion R (fun i ↦ ↑(B i)) hS))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ (algebraMap (𝓞 K) K) (↑u * x) = ↑y ↔ ↑u * x = y

pp: case I
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective ⇑(mixedEmbedding K)

Tactic:
← RingOfIntegers.ext_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ ↑u * x = y ↔ ↑u * x = y

case I
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective ⇑(mixedEmbedding K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Continuous (measurableEquivRealMixedSpacePolarSpace K).invFun

Tactic:
change Continuous fun x : polarSpace K ↦
      (⟨fun w ↦ x.1 w.val, fun w ↦ ⟨x.1 w.val, x.2 w⟩⟩ : realMixedSpace K)
    fun_prop

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ ¬mixedEmbedding.norm (c • x) = 0
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)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
⊢ |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|

Tactic:
let f : Fin (rank K + 1) ≃ InfinitePlace K :=
    (finSuccEquiv _).trans ((Equiv.optionSubtype _).symm e₁.symm).val

Goal state after:
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)
⊢ |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
⊢ σ = τ

Tactic:
by
  have : Nat.card (K ≃ₐ[K⁺] K) = 2 :=
    (IsQuadraticExtension.finrank_eq_two K⁺ K) ▸ IsGalois.card_aut_eq_finrank K⁺ K
  rw [Nat.card_eq_two_iff' 1] at this
  exact ExistsUnique.unique this
    ((isConj_ne_one_iff hφ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ)
    ((isConj_ne_one_iff hψ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal ψ)

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

Goal state before:
pp: case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ¬mixedEmbedding.norm (ζ • x) = 0
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
x : K
⊢ (complexConj K) x = x ↔ x ∈ K⁺

Tactic:
convert! (IntermediateField.mem_fixedField_iff (⊤ : Subgroup (K ≃ₐ[K⁺] K)) x).symm using 1
  · rw [← zpowers_complexConj_eq_top, Subgroup.forall_mem_zpowers]
    exact (MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy (g := (complexConj K))).symm
  · rw [IsGalois.fixedField_top, IntermediateField.mem_bot]
    aesop

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 ≠ 0
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
⊢ ∃ u, u • x ∈ integerSet K

Tactic:
by
  replace hx : mixedEmbedding.norm x ≠ 0 :=
      (norm_eq_zero_iff' (Set.mem_range_of_mem_image (mixedEmbedding K) _ hx')).not.mpr hx
  obtain ⟨u, hu⟩ := exists_unit_smul_mem hx
  obtain ⟨_, ⟨x, rfl⟩, _, rfl⟩ := hx'
  exact ⟨u, mem_integerSet.mpr ⟨hu, u * x, by simp_rw [unitSMul_smul, ← map_mul]⟩⟩

Goal state after:
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 : ℝ
x✝ : ↑(integerSet K)
⊢ ↑1 • ↑x✝ = ↑x✝

Tactic:
OneMemClass.coe_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
x✝ : ↑(integerSet K)
⊢ 1 • ↑x✝ = ↑x✝
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : (ringOfIntegersComplexConj K) x = x
⊢ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K))

Tactic:
rw [RingOfIntegers.ext_iff, coe_ringOfIntegersComplexConj,
      RingOfIntegers.complexConj_eq_self_iff] at h
    obtain ⟨y, hy⟩ := h
    exact ⟨y, RingOfIntegers.ext_iff.mpr hy⟩

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
x✝ : (𝓞 K)ˣ
⊢ x✝ * ((unitsComplexConj K) x✝)⁻¹ = ↑1 ↔ x✝ ∈ realUnits K

Tactic:
OneMemClass.coe_one,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ : (𝓞 K)ˣ
⊢ x✝ * ((unitsComplexConj K) x✝)⁻¹ = 1 ↔ x✝ ∈ realUnits K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      mixedSpaceOfRealSpace (normAtAllPlaces x) ∉ {x | mixedEmbedding.norm x = 0} ↔
    logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      ¬mixedEmbedding.norm (mixedSpaceOfRealSpace (normAtAllPlaces x)) = 0 ↔
    logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      ¬mixedEmbedding.norm x = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_1.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
case refine_1.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : ¬mixedEmbedding.norm y = 0
⊢ normAtAllPlaces y ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_1.refine_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
case refine_1.refine_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : mixedEmbedding.norm y ≤ 1
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}
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
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ regOfFamily (realFundSystem K) = 2 ^ rank K * regulator ↥K⁺

Tactic:
rw [show (2 : ℝ) ^ rank K = |∏ w : {w : InfinitePlace K⁺ // w ≠ w₀}, 2| by
    rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
    simp]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ regOfFamily (realFundSystem K) = |∏ w, 2| * regulator ↥K⁺
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : LinearIndependent ℝ fun w ↦ completeFamily K ↑w
h : completeFamily K w₀ ∈ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
this : ∑ w, completeFamily K w₀ w = 0
⊢ False

Tactic:
rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : LinearIndependent ℝ fun w ↦ completeFamily K ↑w
h : completeFamily K w₀ ∈ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
this : finrank ℚ K = 0
⊢ False
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
this : IsTotallyReal ↥(algebraMap F K).fieldRange
⊢ (algebraMap F K).comp (algebraMap F K).rangeRestrictFieldEquiv.symm.toRingHom =
    (RingEquiv.refl K).toRingHom.comp (algebraMap (↥(algebraMap F K).fieldRange) K)

Tactic:
ext; simp; rfl

Goal state after:
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, ∏ x_2, (x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_2))) ^ x ↑x_2) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
rw [prod_comm]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ Real.exp (x w₀) ^ finrank ℚ K *
      ∏ y, ∏ x_1, (x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm y))) ^ x ↑y) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI : absNorm I ≠ 1
n : ℕ
ζ : K
hn : 2 ≤ n
hζ : IsPrimitiveRoot ζ n
h : (Ideal.Quotient.mk I) hζ.toInteger = 1
⊢ ¬(absNorm I).Coprime n

Tactic:
by
  intro h₁
  rw [← map_one (Ideal.Quotient.mk I), Ideal.Quotient.eq] at h
  obtain ⟨p, hp, h₂⟩ := Nat.exists_prime_and_dvd hI
  have : Fact (p.Prime) := ⟨hp⟩
  refine hp.not_dvd_one <| h₁ ▸ Nat.dvd_gcd h₂ ?_
  exact hζ.prime_dvd_of_dvd_norm_sub_one hn <|
    Int.dvd_trans (Int.natCast_dvd_natCast.mpr h₂) (absNorm_dvd_norm_of_mem h)

Goal state after:
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 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ (Int.castRingHom (𝓞 K)) ↑p ∈ span {hζ.toInteger - 1}

Tactic:
map_natCast

Goal state after:
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 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ ↑p ∈ span {hζ.toInteger - 1}
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}).inertiaDeg ℤ = 1

Tactic:
exact inertiaDeg_span_zeta_sub_one p 0 hζ

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
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ P.inertiaDeg ℤ = 1

Tactic:
eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ (span {⋯.toInteger - 1}).inertiaDeg ℤ = 1
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} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ P.ramificationIdx ℤ = p - 1

Tactic:
eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ (span {⋯.toInteger - 1}).ramificationIdx ℤ = p - 1