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

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
⊢ Summable fun x ↦ ‖eisSummand k x z‖

Tactic:
apply ((summable_one_div_norm_rpow hk').mul_left <| r z ^ (-k : ℝ)).of_nonneg_of_le
    (fun _ ↦ norm_nonneg _)

Goal state after:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : 2 < ↑k
⊢ ∀ (b : Fin 2 → ℤ), ‖eisSummand k b z‖ ≤ r z ^ (-↑k) * ‖b‖ ^ (-↑k)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ ↑{ coe := (-↑ρ)⁻¹, coe_im_pos := ⋯ } = ↑(T • ρ)

Tactic:
modular_T_smul,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ ↑{ coe := (-↑ρ)⁻¹, coe_im_pos := ⋯ } = ↑(1 +ᵥ ρ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
⊢ ↑{ coe := (-↑ρ)⁻¹, coe_im_pos := ⋯ } = ↑(T • ρ)

Tactic:
modular_T_smul,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
⊢ ↑{ coe := (-↑ρ)⁻¹, coe_im_pos := ⋯ } = ↑(1 +ᵥ ρ)
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ Δ (ModularGroup.T • z) *
      (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) 1 0) *
            ↑z +
          ↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) 1
              1)) ^
        (-12) =
    Δ z

Tactic:
modular_T_smul,

Goal state after:
z : ℍ
⊢ Δ (1 +ᵥ z) *
      (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) 1 0) *
            ↑z +
          ↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) 1
              1)) ^
        (-12) =
    Δ z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
⊢ (fun n ↦ f n * (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑(n ^ (l + k))

Tactic:
by
  have h0 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =O[atTop] fun n ↦ ((n ^ k) : ℝ) := by
    have h1 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =
        fun n : ℕ ↦ ((2 * π * I / p) ^ k) * n ^ k := by
      ext z
      ring
    simpa [h1] using isBigO_ofReal_right.mp (Asymptotics.isBigO_const_mul_self
      ((2 * π * I / p) ^ k) (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)) atTop)
  push_cast
  convert! hf.mul h0
  ring

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

Goal state before:
pp: k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
⊢ ∃ u,
    Summable u ∧
      ∀ (n : ℕ), ∀ k_1 ∈ K, ‖(f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) k_1‖ ≤ u n

Tactic:
have : CompactSpace K := isCompact_univ_iff.mp (isCompact_iff_isCompact_univ.mp hKc)

Goal state after:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
⊢ ∃ u,
    Summable u ∧
      ∀ (n : ℕ), ∀ k_1 ∈ K, ‖(f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) k_1‖ ≤ u n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ HasSum (fun x ↦ e2Summand x z)
    (2 * riemannZeta 2 - 8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n) (symmetricIcc ℤ)

Tactic:
by
  simpa [HasSum, -symmetricIcc_filter, symmetricIcc_eq_map_Icc_nat, Function.comp_def,
    G2_partial_sum_eq] using! (aux_G2_tendsto z).const_add _

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
have : T • z ≠ z := by
    apply_fun UpperHalfPlane.re
    simp [-sl_moeb, re_T_smul]

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

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ ¬↑(T • ρ) = ↑ρ

Tactic:
modular_T_smul,

Goal state after:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ ¬↑(1 +ᵥ ρ) = ↑ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ+
h2 :
  ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n -
      (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ })⁻¹ =
    ∑' (n : ℕ+),
      (1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } - ↑↑n) + 1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } + ↑↑n))
⊢ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑N / ↑z - ↑↑m) + 1 / (-↑↑N / ↑z + ↑↑m)) -
      (-2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N

Tactic:
inv_div,

Goal state after:
z : ℍ
N : ℕ+
h2 :
  ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n - ↑z / -↑↑N =
    ∑' (n : ℕ+),
      (1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } - ↑↑n) + 1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } + ↑↑n))
⊢ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑N / ↑z - ↑↑m) + 1 / (-↑↑N / ↑z + ↑↑m)) -
      (-2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ ρ = S • T • ρ

Tactic:
modular_T_smul,

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ ρ = S • (1 +ᵥ ρ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
by
  have := hasSum_jacobiTheta₂_term 0 hτ
  simp_rw [jacobiTheta₂_term, mul_zero, zero_add, ← jacobiTheta_eq_jacobiTheta₂] at this
  have := this.nat_add_neg
  rw [← hasSum_nat_add_iff' 1] at this
  simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_natCast, Nat.cast_zero, neg_zero,
    Int.cast_zero, sq (0 : ℂ), mul_zero, zero_mul, neg_sq, ← mul_two,
    Complex.exp_zero, add_sub_assoc, (by norm_num : (1 : ℂ) - 1 * 2 = -1), ← sub_eq_add_neg,
    Nat.cast_add, Nat.cast_one] at this
  convert! this.div_const 2 using 1
  simp_rw [mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

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

Goal state before:
pp: ⊢ (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (modularForm CuspForm.discriminant) =
    (1 / 1728) •
      ((DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 4) E₄ ^ 3 -
        (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 6) E₆ ^ 2)

Tactic:
simp only [ModularForm.directSum_of_pow]
  change DirectSum.of (ModularForm 𝒮ℒ) 12 CuspForm.discriminant = (1 / 1728 : ℂ) •
    (DirectSum.of (ModularForm 𝒮ℒ) 12 (E₄.pow 3) - DirectSum.of (ModularForm 𝒮ℒ) 12 (E₆.pow 2))
  rw [← map_sub (DirectSum.of (ModularForm 𝒮ℒ) 12), ← DirectSum.of_smul]
  congr 1
  ext z
  change ModularForm.discriminant z = (1 / 1728 : ℂ) * (E₄ z ^ 3 - E₆ z ^ 2)
  grind [discriminant_eq_E₄_cube_sub_E₆_sq z]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * x ^ (n - 1)

Tactic:
by
  rw [geom_sum₂_comm, dvd_geom_sum₂_iff_of_dvd_sub]; simpa using h.neg_right

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x : WithAbs ↑v
⊢ ‖(v.embedding.comp (WithAbs.equiv ↑v).toRingHom) x‖ = ‖x‖

Tactic:
by
    simpa using! v.norm_embedding_eq (WithAbs.equiv v.1 x)

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

Goal state before:
pp: v : InfinitePlace ℚ
x : ℚ
⊢ ‖↑x‖ = ↑|x|

Tactic:
← (WithAbs.equiv v.1).apply_symm_apply x,

Goal state after:
v : InfinitePlace ℚ
x : ℚ
⊢ ‖↑((WithAbs.equiv ↑v) ((WithAbs.equiv ↑v).symm x))‖ = ↑|(WithAbs.equiv ↑v) ((WithAbs.equiv ↑v).symm x)|
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (x ^ p ^ 0 - y ^ p ^ 0) = emultiplicity (↑p) (x - y) + ↑0

Tactic:
rw [Nat.cast_zero, add_zero, pow_zero, pow_one, pow_one]

Goal state after:
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 : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n

Tactic:
← sub_neg_eq_add

Goal state after:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - -y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ i + y ^ 2 ^ i

Tactic:
rcases i with - | i

Goal state after:
case refine_2.zero
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ 0 + y ^ 2 ^ 0

case refine_2.succ
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ ↑(padicValNat p (x ^ n - y ^ n)) = ↑(padicValNat p (x - y) + padicValNat p n)

Tactic:
Nat.cast_add

Goal state after:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ ↑(padicValNat p (x ^ n - y ^ n)) = ↑(padicValNat p (x - y)) + ↑(padicValNat p n)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ ↑(padicValNat p (x ^ n + (y + 1) ^ n)) = ↑(padicValNat p (x + (y + 1)) + padicValNat p n)

Tactic:
Nat.cast_add

Goal state after:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ ↑(padicValNat p (x ^ n + (y + 1) ^ n)) = ↑(padicValNat p (x + (y + 1))) + ↑(padicValNat p n)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫ (x : mixedSpace K), f x

Tactic:
rw [← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).integral_comp
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding, ← integral_comp_polarCoordReal_symm,
    polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq, Function.comp_def]

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 y : (𝓞 K)ˣ),
    ⟨x * y * ((unitsComplexConj K) (x * y))⁻¹, ⋯⟩ =
      ⟨x * ((unitsComplexConj K) x)⁻¹, ⋯⟩ * ⟨y * ((unitsComplexConj K) y)⁻¹, ⋯⟩

Tactic:
intro _

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ : (𝓞 K)ˣ
⊢ ∀ (y : (𝓞 K)ˣ),
    ⟨x✝ * y * ((unitsComplexConj K) (x✝ * y))⁻¹, ⋯⟩ =
      ⟨x✝ * ((unitsComplexConj K) x✝)⁻¹, ⋯⟩ * ⟨y * ((unitsComplexConj K) y)⁻¹, ⋯⟩
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 : ℝ
⊢ (a : Quotient (MulAction.orbitRel ↥(Units.torsion K) ↑(integerSet K))) →
    ↥(Units.torsion K) ⧸ MulAction.stabilizer (↥(Units.torsion K)) a.out ≃ ↥(Units.torsion K)

Tactic:
intro _

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a✝ : Quotient (MulAction.orbitRel ↥(Units.torsion K) ↑(integerSet K))
⊢ ↥(Units.torsion K) ⧸ MulAction.stabilizer (↥(Units.torsion K)) a✝.out ≃ ↥(Units.torsion K)
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

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

Tactic:
intro _

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

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

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

Tactic:
Equiv.prod_comp f (fun w ↦ (w (u _) ^ (mult w))),

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

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

Goal state before:
pp: case inl
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 : IsUnramified K w
⊢ (w.comap (algebraMap K L)).mult * 1 = w.mult

Tactic:
h.eq,

Goal state after:
case inl
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 : IsUnramified K w
⊢ w.mult * 1 = w.mult
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
⊢ regulator K / regulator ↥K⁺ = 2 ^ rank K * (2 ^ rank K * regulator ↥K⁺ / regulator K)⁻¹

Tactic:
inv_div,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ regulator K / regulator ↥K⁺ = 2 ^ rank K * (regulator K / (2 ^ rank K * regulator ↥K⁺))
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ (InfinitePlace.mk (W.embedding.comp (algebraMap (↥L) K))).IsReal

Tactic:
isReal_mk_iff

Goal state after:
K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ ComplexEmbedding.IsReal (W.embedding.comp (algebraMap (↥L) K))
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' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (b : InfinitePlace K),
    ¬b = w' →
      (if h : b = w' then ∑ x, ↑x.mult else ∑ x, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨b, ⋯⟩))))) = 0

Tactic:
intro _

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
b✝ : InfinitePlace K
⊢ ¬b✝ = w' →
    (if h : b✝ = w' then ∑ x, ↑x.mult else ∑ x, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨b✝, ⋯⟩))))) = 0
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : (absNorm P).Coprime (torsionOrder K)
this : P.IsMaximal
⊢ torsionOrder K ∣ absNorm P - 1

Tactic:
let _ := Ideal.Quotient.field P

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : (absNorm P).Coprime (torsionOrder K)
this : P.IsMaximal
x✝ : Field (𝓞 K ⧸ P) := Quotient.field P
⊢ torsionOrder K ∣ absNorm P - 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
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Prime (hζ.toInteger - 1)

Tactic:
exact hζ.zeta_sub_one_prime

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
⊢ y w₀ ≤ 0

Tactic:
by simpa using hy w₀ (Set.mem_univ _)

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

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

Tactic:
ofReal_mul zero_le_two,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (ENNReal.ofReal 2 * ENNReal.ofReal Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) * (↑(finrank ℚ K))⁻¹) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)