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

Goal state before:
pp: case inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ⋯
hgz : g = T ^ 1
hre : (g • z).re = ↑b + z.re
hb : b = 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2

Tactic:
hgz,

Goal state after:
case inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ 1
hre : (g • z).re = ↑b + z.re
hb : b = 1
⊢ (T ^ 1 = T ∨ T ^ 1 = -T) ∧ z.re = -1 / 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ⋯
hgz : g = T ^ (-1)
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2

Tactic:
hgz,

Goal state after:
case inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ (-1)
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ (T ^ (-1) = T⁻¹ ∨ T ^ (-1) = -T⁻¹) ∧ z.re = 1 / 2
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
⊢ ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-↑k)

Tactic:
simp_rw [IsBigO, ← Int.cast_neg, Real.rpow_intCast, IsBigOWith, eventually_comap]

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
⊢ ∃ c, ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ c * ‖a.im ^ (-k)‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
e2Summand,

Goal state after:
case e_f
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
a : ℤ
⊢ ∑' (n : ℤ), eisSummand 2 ![a, n] z =
    ∑' (n : ℤ), G2Term z ![a, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑a * ↑z + ↑n) - 1 / (↑a * ↑z + ↑n + 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ G2 z = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]

Tactic:
G2_eq_tsum_G2Term z,

Goal state after:
z : ℍ
⊢ ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n] = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hnorm
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
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
⊢ √1 = ‖1 + ↑ρ‖

Tactic:
show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq],

Goal state after:
case hnorm
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
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
⊢ √1 = ‖-↑ρ ^ 2‖
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
h : F ∣[k] γ = F
⊢ serreDerivative (↑k) F ∣[k + 2] γ = serreDerivative (↑k) F

Tactic:
by
  grind [serreDerivative_slash_equivariant]

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
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
hr : ‖r‖ < 1
⊢ Summable ?m.229

Tactic:
by simpa using (summable_norm_mul_geometric_of_norm_lt_one' hr
    (Asymptotics.isBigO_norm_left.mpr (aux_IsBigO_mul k l p hf)))

Goal state after:
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) * (↑m * ↑z + ↑b - (↑m * ↑z + ↑a)) * (1 / (↑m * ↑z + ↑b)) =
    (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

Tactic:
grind [one_div, add_sub_add_left_eq_sub, mul_inv_rev]

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

Goal state before:
pp: z : ℍ
N : ℕ+
h2 :
  ↑π * (↑π * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }).cot =
    1 / ↑{ 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:
rw [pi_mul_cot_pi_q_exp, ← sub_eq_iff_eq_add', one_div, inv_div, neg_mul, ← h2,
      ← tsum_zero_pnat_eq_tsum_nat
      (by simpa using norm_exp_two_pi_I_lt_one ⟨-N / z, im_pnat_div_pos N z⟩)] at *

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

Goal state before:
pp: case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * τ).re = -π * τ.im * ↑n ^ 2
m : ℕ
hm : n ^ 2 = ↑m
⊢ rexp (↑π * I * ↑n ^ 2 * τ).re = y ^ n ^ 2

Tactic:
rw [this, exp_mul, ← Int.cast_pow, rpow_intCast, hm, zpow_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: this : IsClosed {z | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
x : ℂ
x✝ : x ∈ {z | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
him : 0 ≤ x.im
hre : 1 ≤ ‖x‖
hnorm : |x.re| ≤ 1 / 2
⊢ x.im ≠ 0

Tactic:
by grind [abs_re_eq_norm]

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
have : Filter.Tendsto (fun t : ℝ ↦ t * (x : ℂ)) (𝓝 1) (𝓝 (x : ℂ)) := by
      rw [show 𝓝 (x : ℂ) = 𝓝 ((1 : ℝ) * (x : ℂ)) by simp]
      exact Continuous.tendsto (by fun_prop) _

Goal state after:
case hf
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun t ↦ ↑t * ↑x) (𝓝 1) (𝓝 ↑x)
⊢ Filter.Tendsto (fun x_1 ↦ ↑(↑ofComplex (↑x_1 * ↑x))) (𝓝 1) (𝓝 ↑x)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x))) =
    (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1))

Tactic:
have : ∀ (x : ℕ), (hx : x ∈ range p) → a ^ (x + (p - 1 - x)) = a ^ (p - 1) := by
        intro x hx
        rw [← Nat.add_sub_assoc _ x, Nat.add_sub_cancel_left]
        exact Nat.le_sub_one_of_lt (Finset.mem_range.mp hx)

Goal state after:
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
this : ∀ x ∈ range p, a ^ (x + (p - 1 - x)) = a ^ (p - 1)
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x))) =
    (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1))
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, ↑(B i)]_[𝓕]
hx : IsUnit x
⊢ (∀ (i : ι), IsUnit (x i)) ∧ ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩

Tactic:
simp only [isUnit_iff_exists, RestrictedProduct.ext_iff, ← forall_and] at hx
  simp only [isUnit_iff_exists]
  choose b hb using hx
  exact ⟨Classical.skolem.symm.1 ⟨b, hb⟩, by filter_upwards [x.2, b.2] using
    fun i hx hb ↦ ⟨hx, ⟨b i, hb⟩, by simp_all [← SetLike.coe_eq_coe]⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x : ℤ
hx : Odd x
⊢ x ^ 2 % 4 = 1

Tactic:
unfold Odd at hx

Goal state after:
x : ℤ
hx : ∃ k, x = 2 * k + 1
⊢ x ^ 2 % 4 = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝² x✝¹ : (𝓞 K)ˣ
x✝ : mixedSpace K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝² * (algebraMap (𝓞 K) K) ↑x✝¹) * x✝ =
    (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝²) * ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝¹) * x✝)

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
x✝² x✝¹ : (𝓞 K)ˣ
x✝ : mixedSpace K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝²) * (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝¹) * x✝ =
    (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝²) * ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝¹) * 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 ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * x) = mixedEmbedding.norm x

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) * mixedEmbedding.norm x = mixedEmbedding.norm x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult * (Real.log ((normAtPlace ↑w) (x * y)) - Real.log (mixedEmbedding.norm (x * y)) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑w).mult * (Real.log ((normAtPlace ↑w) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) +
      ↑(↑w).mult * (Real.log ((normAtPlace ↑w) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult *
      (Real.log ((normAtPlace ↑w) x * (normAtPlace ↑w) y) -
        Real.log (mixedEmbedding.norm (x * y)) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑w).mult * (Real.log ((normAtPlace ↑w) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) +
      ↑(↑w).mult * (Real.log ((normAtPlace ↑w) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult *
      (Real.log ((normAtPlace ↑w) x * (normAtPlace ↑w) y) -
        Real.log (mixedEmbedding.norm (x * y)) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑w).mult * (Real.log ((normAtPlace ↑w) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) +
      ↑(↑w).mult * (Real.log ((normAtPlace ↑w) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult *
      (Real.log ((normAtPlace ↑w) x * (normAtPlace ↑w) y) -
        Real.log (mixedEmbedding.norm x * mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑w).mult * (Real.log ((normAtPlace ↑w) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) +
      ↑(↑w).mult * (Real.log ((normAtPlace ↑w) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ) * x)) -
        Real.log (mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ) * x)) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * (normAtPlace ↑x✝) x) -
        Real.log (mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * mixedEmbedding.norm x) *
          (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ 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)ˣ
⊢ regOfFamily u ≠ 0 → IsMaxRank u

Tactic:
simpa using (fun hu ↦ regOfFamily_eq_zero hu).mt

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
w : InfinitePlace K
x : K
⊢ ‖(starRingEnd ℂ) (w.embedding x)‖ = w x

Tactic:
Complex.norm_conj,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
⊢ ‖w.embedding x‖ = w x
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
⊢ ¬mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ) * x) = 0

Tactic:
map_mul,

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 ((mixedEmbedding K) ((algebraMap (𝓞 K) 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✝¹ x✝ : K
⊢ (complexConj K) (x✝¹ * x✝) = (complexConj K) x✝ * (complexConj K) x✝¹

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x✝¹ x✝ : K
⊢ (complexConj K) x✝¹ * (complexConj K) x✝ = (complexConj K) x✝ * (complexConj K) x✝¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ (mixedEmbedding K)
      ↑(↑(preimageOfMemIntegerSet ⟨u • (mixedEmbedding K) ↑↑x, hu⟩) * ↑↑(unitsNonZeroDivisorsEquiv.symm u⁻¹)) =
    (mixedEmbedding K) ↑↑x

Tactic:
map_mul,

Goal state after:
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(preimageOfMemIntegerSet ⟨u • (mixedEmbedding K) ↑↑x, hu⟩)) *
      (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑(unitsNonZeroDivisorsEquiv.symm u⁻¹)) =
    (mixedEmbedding K) ↑↑x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ (∃ u, (mixedEmbedding K) ↑(↑↑u * ↑(preimageOfMemIntegerSet a)) = (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet b)) ↔
    ∃ ζ, ↑(ζ • a) = ↑b

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ (∃ u,
      (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) *
          (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(preimageOfMemIntegerSet a)) =
        (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet b)) ↔
    ∃ ζ, ↑(ζ • a) = ↑b
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card ↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} * torsionOrder K = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}

Tactic:
torsionOrder,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card ↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} * Nat.card ↥(Units.torsion K) =
    Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ mixedEmbedding.norm ↑↑((idealSetEquiv K J) a) = mixedEmbedding.norm ↑a

Tactic:
idealSetEquiv_apply

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ mixedEmbedding.norm ↑a = mixedEmbedding.norm ↑a
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } * torsionOrder K =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }

Tactic:
torsionOrder,

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } * Nat.card ↥(Units.torsion K) =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }
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
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
⊢ E = maximalRealSubfield K

Tactic:
refine le_antisymm (IsTotallyReal.le_maximalRealSubfield E) ?_

Goal state after:
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
⊢ maximalRealSubfield K ≤ E
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
⊢ ComplexEmbedding.IsReal (W.embedding.comp (algebraMap (↥L) K))

Tactic:
exact ComplexEmbedding.IsConj.isReal_comp
     (σ := IsGaloisGroup.mulEquivAlgEquiv (Subgroup.zpowers σ) L K ⟨σ, Subgroup.mem_zpowers σ⟩)
      (hσ W.embedding)

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : w = w₀
⊢ (completeBasis K) w i = ↑i.mult

Tactic:
rw [hw, completeBasis_apply_of_eq]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
this : NeZero ↑n
⊢ NeZero ↑n

Tactic:
simpa using! NeZero.of_injective (algebraMap K (AdjoinRoot P)).injective

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ ↑(finrank ℚ K) * regOfFamily (fundSystem K) =
    |(Matrix.of fun i w ↦
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|

Tactic:
finrank_mul_regOfFamily_eq_det

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ |(Matrix.of fun i w ↦
          if h : i = ?w' then ↑w.mult
          else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (?e ⟨i, h⟩))))).det| =
    |(Matrix.of fun i w ↦
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|

case w'
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ InfinitePlace K

case e
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ { w // w ≠ ?w' } ≃ Fin (rank K)