mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
⊢ ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z * denom (toGL (φ B)) ↑z /
      (denom (toGL (φ A)) ↑(toGL (φ B) • z) * denom (toGL (φ B)) ↑z) =
    (↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z -
          ↑(↑B 1 0) * denom (toGL (φ A)) ↑(toGL (φ B) • z) * denom (toGL (φ B)) ↑z) /
        denom (toGL (φ A)) ↑(toGL (φ B) • z) +
      denom (toGL (φ B)) ↑z * ↑(↑B 1 0)

Tactic:
field_simp [denom_ne_zero A (toGL (φ B) • z)]

Goal state after:
A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
⊢ ↑((↑A * ↑B) 1 0) =
    ↑((↑A * ↑B) 1 0) - denom (toGL (φ A)) ↑(toGL (φ B) • z) * ↑(↑B 1 0) +
      denom (toGL (φ A)) ↑(toGL (φ B) • z) * ↑(↑B 1 0)
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * ↑π * I * (↑n + 1) * z)
⊢ 0 < ((n + 1) • z).im

Tactic:
by
    simpa [(show 0 < (n + 1 : ℝ) by positivity)] using hz

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

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑'[symmetricIcc ℤ] (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))

Tactic:
congr with a
      rw [e2Summand, tsum_eq_of_summable_unconditional
        (summable_right_one_div_linear_sub_one_div_linear_succ z a), ← Summable.tsum_add
        ((G2Term_prod_summable z).prod_factor _)
        (summable_right_one_div_linear_sub_one_div_linear_succ z a)]
      exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat])

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ z.im ≤ (-g • z).im

Tactic:
simpa using hden

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

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * (↑π * I / 12 * E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ }) =
    ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z

Tactic:
← mul_assoc,

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * (↑π * I / 12) * E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } =
    ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ((↑z ^ 2)⁻¹ * (↑π * I / 12)) =
    ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z

Tactic:
← mul_assoc,

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ * (↑π * I / 12) =
    ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / (↑m * ↑z + ↑a) - 1 / (↑m * ↑z + ↑b) = (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

Tactic:
rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div]
  · grind [one_div, add_sub_add_left_eq_sub, mul_inv_rev]
  · simpa using linear_ne_zero z (cd := ![m, a]) (by aesop)
  · simpa using linear_ne_zero z (cd := ![m, b]) (by aesop)

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

Goal state before:
pp: z : ℍ
m : ℤ
⊢ Tendsto (fun N ↦ ∑ b ∈ Ico (-↑N) ↑N, (1 / (↑m * ↑z + ↑b) - 1 / (↑m * ↑z + ↑b + 1))) atTop (𝓝 0)

Tactic:
telescope_aux z m

Goal state after:
z : ℍ
m : ℤ
⊢ Tendsto (fun N ↦ 1 / (↑m * ↑z - ↑N) - 1 / (↑m * ↑z + ↑N)) atTop (𝓝 0)
Module: Mathlib.NumberTheory.Modular

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

Tactic:
suffices S • I = I by simp +contextual [-sl_moeb, or_imp, this]

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ S • I = I
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

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

Tactic:
lift k to ℕ using hk

Goal state after:
case inr
k : ℕ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑((↑k).toNat / 12) < (qExpansion 1 ⇑f).order
⊢ f = 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 (-↑τ)⁻¹ = (-I * ↑τ) ^ (1 / 2) * (1 / (-I * ↑τ) ^ (1 / 2) * jacobiTheta₂ 0 (-1 / ↑τ))

Tactic:
← mul_assoc,

Goal state after:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 (-↑τ)⁻¹ = (-I * ↑τ) ^ (1 / 2) * (1 / (-I * ↑τ) ^ (1 / 2)) * jacobiTheta₂ 0 (-1 / ↑τ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hf
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun t ↦ ↑t * ↑x) (𝓝 1) (𝓝 ↑x)
⊢ (fun t ↦ ↑t * ↑x) =ᶠ[𝓝 1] fun x_1 ↦ ↑(↑ofComplex (↑x_1 * ↑x))

Tactic:
filter_upwards [eventually_gt_nhds zero_lt_one] with a ha

Goal state after:
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun t ↦ ↑t * ↑x) (𝓝 1) (𝓝 ↑x)
a : ℝ
ha : 0 < a
⊢ ↑a * ↑x = ↑(↑ofComplex (↑a * ↑x))
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
⊢ f { coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    I ^ k * ↑t ^ k *
      (↑{ coe := I * ↑t, coe_im_pos := ⋯ } ^ (-k) *
        f
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
            { coe := I * ↑t, coe_im_pos := ⋯ }))

Tactic:
← mul_assoc,

Goal state after:
Γ : 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
⊢ f { coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    I ^ k * ↑t ^ k * ↑{ coe := I * ↑t, coe_im_pos := ⋯ } ^ (-k) *
      f
        (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
          { coe := I * ↑t, coe_im_pos := ⋯ })
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 Γ
h : G.Commensurable H
this✝ : (G ⊓ H).IsFiniteRelIndex H
this : (G ⊓ H).IsFiniteRelIndex G
⊢ ProperlyDiscontinuousSMul (↥G) α ↔ ProperlyDiscontinuousSMul (↥H) α

Tactic:
calc ProperlyDiscontinuousSMul G α ↔ ProperlyDiscontinuousSMul ↑(G ⊓ H) α :=
    (properlyDiscontinuousSMul_iff_of_isFiniteRelIndex inf_le_left).symm
  _ ↔ ProperlyDiscontinuousSMul H α :=
    properlyDiscontinuousSMul_iff_of_isFiniteRelIndex inf_le_right

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

pp: case succ
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
x : ℕ
hx : x + 1 ∈ range p
⊢ a ^ (x + 1 - 1 + (p - 1 - (x + 1))) * ↑p * b * ↑(x + 1) = ↑p * b * a ^ (p - 2) * ↑(x + 1)

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

Goal state after:
case succ
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
x : ℕ
hx : x + 1 ∈ range p
⊢ a ^ (x + 1 - 1 + (p - 1 - (x + 1))) * ↑p * b * ↑(x + 1) = ↑p * b * a ^ (p - 2) * ↑(x + 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
⊢ emultiplicity (↑p) (x ^ n - y ^ n) = emultiplicity (↑p) (x - y) + emultiplicity p n

Tactic:
by
  rcases n with - | n
  · simp only [emultiplicity_zero, add_top, pow_zero, sub_self]
  have h : FiniteMultiplicity _ _ := Nat.finiteMultiplicity_iff.mpr ⟨hp.ne_one, n.succ_pos⟩
  simp only [Nat.succ_eq_add_one] at h
  rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩
  conv_lhs => rw [hk, pow_mul, pow_mul]
  rw [Nat.prime_iff_prime_int] at hp
  rw [emultiplicity_pow_sub_pow_of_prime hp,
    emultiplicity_pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx, h.emultiplicity_eq_multiplicity]
  · rw [← geom_sum₂_mul]
    exact dvd_mul_of_dvd_right hxy
  · exact fun h => hx (hp.dvd_of_dvd_pow h)
  · rw [Int.natCast_dvd_natCast]
    rintro ⟨c, rfl⟩
    refine hpn ⟨c, ?_⟩
    rwa [pow_succ, mul_assoc]

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
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite

Tactic:
simp_rw [valuation_lt_one_iff_dvd]

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
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
⊢ {v | v.asIdeal ∣ Ideal.span {d}}.Finite
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
this : x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
⊢ (x ^ 2 ^ d + y ^ 2 ^ d) * ((∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)) =
    (∏ x_1 ∈ range d, (x ^ 2 ^ x_1 + y ^ 2 ^ x_1)) * (x ^ 2 ^ d + y ^ 2 ^ d) * (x - y)

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
this : x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
⊢ ((x ^ 2 ^ d + y ^ 2 ^ d) * ∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y) =
    (∏ x_1 ∈ range d, (x ^ 2 ^ x_1 + y ^ 2 ^ x_1)) * (x ^ 2 ^ d + y ^ 2 ^ d) * (x - 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)
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:
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.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hxy
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ 2 ∣ x ^ 2 ^ multiplicity 2 (n + 1) - y ^ 2 ^ multiplicity 2 (n + 1)

Tactic:
simpa only [even_iff_two_dvd] using hx_odd.pow.sub_odd hy_odd.pow

Goal state after:
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)ˣ
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))

Tactic:
change _ ↔ Finite ((unitLattice K).toAddSubgroup ⧸ (span ℤ (Set.range _)).toAddSubgroup)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K).toAddSubgroup ⧸
        (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup)
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)ˣ
⊢ (unitsComplexConj K) u = u ↔ u ∈ realUnits K

Tactic:
simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) K]

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
⊢ (Nat.card ↥(torsion K)).gcd 2 = 2

Tactic:
Nat.gcd_eq_right_iff_dvd

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 ∣ Nat.card ↥(torsion K)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
hS : ∃ n ∈ S, 2 < n
inst✝ : IsCyclotomicExtension S ℚ K
this : Algebra.IsIntegral ℚ K
⊢ IsCMField K

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := hS

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
⊢ IsCMField K
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₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) =
    Real.exp (x w₀) •
      Real.exp (if w₀ = w₀ then 0 else x w₀) • fun w ↦
        ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i

Tactic:
if_pos rfl,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) =
    Real.exp (x w₀) •
      Real.exp 0 • fun w ↦
        ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ : Fin (rank K)
x✝ : { w // w ≠ w₀ }
⊢ (basisOfIsMaxRank ⋯) i✝ x✝ = (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) i✝ x✝

Tactic:
rw [Basis.ofZLatticeBasis_apply, basisOfIsMaxRank_apply, logEmbedding_fundSystem]

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₀) • fun w ↦
    ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i

Tactic:
enter [2, w, 2, i]
    rw [if_neg i.prop]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
i : { w // w ≠ w₀ }
| w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ Real.exp (if w₀ = w₀ then 0 else x w₀) ^ finrank ℚ K = 1

Tactic:
if_pos rfl,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ Real.exp 0 ^ finrank ℚ K = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun w ↦
          ((if w₀ = w₀ then 0 else x w₀) • (completeBasis K) w₀ +
              ∑ i, (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i)
            ↑w)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
if_pos rfl,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun w ↦
          (0 • (completeBasis K) w₀ + ∑ i, (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i) ↑w)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
⊢ (↑(nthRootsFinset p 1)).Pairwise fun η₁ η₂ ↦ Associated (ζ - 1) (η₁ - η₂)

Tactic:
intro η₁ hη₁ η₂ hη₂ e

Goal state after:
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ ↑(nthRootsFinset p 1)
η₂ : A
hη₂ : η₂ ∈ ↑(nthRootsFinset p 1)
e : η₁ ≠ η₂
⊢ Associated (ζ - 1) (η₁ - η₂)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
⊢ (Real.exp (if w₀ = w₀ then Real.log c else y w₀) •
      ↑expMapBasis fun i ↦ if i = w₀ then 0 else if i = w₀ then Real.log c else y i) =
    (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y)

Tactic:
if_pos rfl,

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
⊢ (Real.exp (Real.log c) • ↑expMapBasis fun i ↦ if i = w₀ then 0 else if i = w₀ then Real.log c else y i) =
    (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 ^ nrComplexPlaces K)⁻¹ *
      (2 ^ nrComplexPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)) =
    2 ^ nrRealPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
← mul_assoc,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 ^ nrComplexPlaces K)⁻¹ *
        (2 ^ nrComplexPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K) *
      ENNReal.ofReal (regulator K) =
    2 ^ nrRealPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 ^ nrComplexPlaces K)⁻¹ *
        (2 ^ nrComplexPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K) *
      ENNReal.ofReal (regulator K) =
    2 ^ nrRealPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
← mul_assoc,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 ^ nrComplexPlaces K)⁻¹ * 2 ^ nrComplexPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K *
      ENNReal.ofReal (regulator K) =
    2 ^ nrRealPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case refine_2
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ ↑1 ≤
    emultiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))

Tactic:
rw [ENat.natCast_one]
    exact Order.one_le_iff_pos.mpr <| emultiplicity_pos_of_dvd h₂.2.2

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

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p

Tactic:
obtain ⟨⟨P, _, _⟩⟩ := 𝒑.nonempty_primesOver (S := 𝓞 K)

Goal state after:
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left✝ : P.IsPrime
right✝ : P.LiesOver 𝒑
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
⊢ 𝒑.ramificationIdxIn (𝓞 K) = 1

Tactic:
obtain ⟨⟨P, _, _⟩⟩ := 𝒑.nonempty_primesOver (S := 𝓞 K)

Goal state after:
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left✝ : P.IsPrime
right✝ : P.LiesOver 𝒑
⊢ 𝒑.ramificationIdxIn (𝓞 K) = 1