mathlib-initiative/mathlib-tactics huggingface dataset:
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)⁻¹ * logDeriv η (-↑z)⁻¹ = ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z

Tactic:
logDeriv_eta_eq_E2 (.mk _ z.im_inv_neg_coe_pos),

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)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = ↑z ^ (-1 / 2) * (↑z ^ 2⁻¹)⁻¹ / 2 + ↑π * I / 12 * E2 z

Tactic:
neg_div,

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)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = ↑z ^ (-(1 / 2)) * (↑z ^ 2⁻¹)⁻¹ / 2 + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
⊢ (g • z).im = z.im

Tactic:
by
  wlog hden : z.im ≤ (g • z).im
  · rw [← this (g := g⁻¹) hg (by simpa using hz) (by simpa using le_of_not_ge hden)]
    simp
  wlog hc : 0 ≤ g 1 0
  · -- TODO: `wlog` leaves junk copies of variables in scope
    simpa using @this (-g) z (-g) z hz (by simpa using hg)
      (by simpa using hden) (by simpa using (not_le.mp hc).le)
  rw [im_smul_eq_div_normSq, le_div_iff₀ (normSq_denom_pos _ z.im_ne_zero),
    mul_le_iff_le_one_right z.im_pos, normSq_eq_norm_sq, sq_le_one_iff₀ (norm_nonneg _)] at hden
  have hc : g 1 0 = 0 ∨ g 1 0 = 1 := by grind [abs_c_le_one hz hg]
  rcases hc with hc | hc
  · rcases cases_c_zero hz hg hc with h | h | h | h <;>
    rcases h with ⟨(rfl | rfl), -⟩ <;>
    simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]
  · rw [im_smul_eq_div_normSq, div_eq_iff (normSq_denom_pos _ z.im_ne_zero).ne',
    eq_comm, mul_eq_left₀ z.im_ne_zero]
    rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz hden hc) with hd | hd | hd
    · rcases cases_c_one_d_zero hz hg hden hc hd with
        ⟨rfl, hnm⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
      · simp [normSq_eq_norm_sq, denom, coe_S, hnm]
      · rw [show T⁻¹ * S = ⟨!![-1, -1; 1, 0], by simp⟩ by decide]
        norm_num [ρ, denom, ← pow_two, div_pow]
      · rw [show T * S = ⟨!![1, -1; 1, 0], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]
    · rcases case_c_one_d_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩
      · rw [show S * T = ⟨!![0, -1; 1, 1], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]
      · rw [show T * S * T = ⟨!![1, 0; 1, 1], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]
    · rcases case_c_one_d_neg_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩
      · rw [show S * T⁻¹ = ⟨!![0, -1; 1, -1], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]
      · rw [show T⁻¹ * S * T⁻¹ = ⟨!![-1, 0; 1, -1], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]

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

Goal state before:
pp: p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : (PowerSeries.coeff 0) p4 = 1
hp6_0 : (PowerSeries.coeff 0) p6 = 1
hp4_1 : (PowerSeries.coeff 1) p4 = 240
hp6_1 : (PowerSeries.coeff 1) p6 = -504
hqc4 : c4 • p4 = p ^ 2
hqc6 : c6 • p6 = p ^ 3
⊢ p = 0

Tactic:
simp_all only [PowerSeries.coeff_zero_eq_constantCoeff]

Goal state after:
p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : PowerSeries.constantCoeff p4 = 1
hp6_0 : PowerSeries.constantCoeff p6 = 1
hp4_1 : (PowerSeries.coeff 1) p4 = 240
hp6_1 : (PowerSeries.coeff 1) p6 = -504
hqc4 : c4 • p4 = p ^ 2
hqc6 : c6 • p6 = p ^ 3
⊢ p = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ Summable fun m ↦ 1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)

Tactic:
· simpa using! summable_left_one_div_linear_sub_one_div_linear z (-d) d

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

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

Tactic:
neg_div,

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

Goal state before:
pp: ⊢ IsOpen 𝒟ᵒ

Tactic:
refine .inter (.preimage (by fun_prop) isOpen_Ioi) ?_

Goal state after:
⊢ IsOpen fun z ↦ Real.lt✝ |z.re| (1 / 2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
⊢ IsCompact (truncatedFundamentalDomain y)

Tactic:
rw [isEmbedding_coe.isCompact_iff, coe_truncatedFundamentalDomain,
    Metric.isCompact_iff_isClosed_bounded]
  constructor
  · -- show closed
    apply (isClosed_le continuous_const Complex.continuous_im).inter
    apply (isClosed_le Complex.continuous_im continuous_const).inter
    apply (isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const).inter
    exact isClosed_le continuous_const continuous_norm
  · -- show bounded
    refine (Metric.isBounded_iff_subset_closedBall 0).mpr ⟨√((1 / 2) ^ 2 + y ^ 2), fun z hz ↦ ?_⟩
    simp only [mem_closedBall_zero_iff]
    refine le_of_sq_le_sq ?_ (by positivity)
    rw [Real.sq_sqrt (by positivity), Complex.norm_eq_sqrt_sq_add_sq, Real.sq_sqrt (by positivity)]
    apply add_le_add
    · rw [sq_le_sq, abs_of_pos <| one_half_pos (α := ℝ)]
      exact hz.2.2.1
    · rw [sq_le_sq₀ hz.1 (hz.1.trans hz.2.1)]
      exact hz.2.1

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
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
⊢ ∑ i ∈ range p, (Ideal.Quotient.mk (span {s})) ((a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) * a ^ (p - 1 - i)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x)))

Tactic:
by
      ring_nf
      simp_rw [← map_sum, sum_add_distrib, map_add]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
by
  intro hx
  unfold Odd at hx
  rcases hx with ⟨_, rfl⟩
  ring_nf
  rw [add_assoc, ← add_mul, Int.add_mul_emod_self_right]
  decide

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto f (Filter.map (fun p ↦ (inclusion R A hS p.1, id p.2)) (𝓝 (x', y))) (𝓝 (f (inclusion R A hS x', y)))

Tactic:
tendsto_map'_iff

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto (f ∘ fun p ↦ (inclusion R A hS p.1, id p.2)) (𝓝 (x', y)) (𝓝 (f (inclusion R A hS 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)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto f (Filter.map (fun p ↦ (id p.1, inclusion R A hS p.2)) (𝓝 (y, x'))) (𝓝 (f (y, inclusion R A hS x')))

Tactic:
tendsto_map'_iff

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto (f ∘ fun p ↦ (id p.1, inclusion R A hS p.2)) (𝓝 (y, x')) (𝓝 (f (y, inclusion R A hS x')))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ ((homeoRealMixedSpacePolarSpace K).symm x✝ ∈ Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target) ↔
    x✝ ∈ (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π

Tactic:
homeoRealMixedSpacePolarSpace_symm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ ((fun w ↦ x✝.1 ↑w, fun w ↦ (x✝.1 ↑w, x✝.2 w)) ∈ Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target) ↔
    x✝ ∈ (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
this : mixedEmbedding.norm (c • 1) ≠ 0
⊢ logMap (c • x) = logMap x

Tactic:
rw [← smul_one_mul, logMap_mul this hx, logMap_real, zero_add]

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
hx : x ∈ fundamentalCone K
hy : ∀ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x
⊢ y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
rw [Set.mem_preimage, logMap_eq_of_normAtPlace_eq hy]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : x ∈ fundamentalCone K
hy : ∀ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x
⊢ logMap x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ regOfFamily u = |(of fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))).det|

Tactic:
rw [regOfFamily_of_isMaxRank hu, ZLattice.covolume_eq_det _
      (((basisOfIsMaxRank hu).restrictScalars ℤ).reindex (equivFinRank K)), Basis.coe_reindex]
    congr 3 with i
    simp [basisOfIsMaxRank_apply hu]

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
c : ℝ
hc : c ≠ 0
⊢ c • x ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ smul_mem_of_mem h hc⟩
  convert! smul_mem_of_mem h (inv_ne_zero hc)
  rw [eq_inv_smul_iff₀ hc]

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
⊢ Units.rank ↥K⁺ = Units.rank K

Tactic:
rw [Units.rank, Units.rank, card_infinitePlace_eq_card_infinitePlace K]

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)ˣ
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| =
    ↑1 * |(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| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|

Tactic:
Int.cast_one,

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)
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| =
    1 * |(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| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case hf
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ AEMeasurable (fun x ↦ (∏ w, ENNReal.ofReal (x.1 ↑w)) * A.indicator 1 (↑(polarSpaceCoord K).symm x))
    ((volume.prod volume).restrict
      ((Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π))

Tactic:
exact (Measurable.mul (by fun_prop)
      <| measurable_const.indicator <| hm.preimage (measurable_polarSpaceCoord_symm K)).aemeasurable

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✝² x✝¹ : ↥(torsion K)
x✝ : ↑(integerSet K)
⊢ (↑x✝² * ↑x✝¹) • ↑x✝ = ↑x✝² • ↑x✝¹ • ↑x✝

Tactic:
mul_smul

Goal state after:
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✝ : NumberField K
x✝ : ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
u : (𝓞 K)ˣ
hu : Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
⊢ ⊤ = Subgroup.map (unitsMulComplexConjInv K) (Subgroup.zpowers u)

Tactic:
rw [MonoidHom.map_zpowers, ← hu]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult - ↑(↑x✝).mult * ↑(∑ x, x.mult) * (↑(finrank ℚ K))⁻¹ = 0 x✝

Tactic:
sum_mult_eq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult - ↑(↑x✝).mult * ↑(finrank ℚ K) * (↑(finrank ℚ K))⁻¹ = 0 x✝
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
⊢ (algebraMap v.Completion w.Completion).comp (RingEquiv.quotientBot v.Completion).toRingHom =
    (RingEquiv.quotientBot w.Completion).toRingHom.comp (algebraMap (v.Completion ⧸ ⊥) (w.Completion ⧸ ⊥))

Tactic:
by ext; simp [RingHom.algebraMap_toAlgebra]

Goal state after:
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 : ↑(∑ x, x.mult) = 0
⊢ False

Tactic:
sum_mult_eq,

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.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
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |↑(∑ x, x.mult)| *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|

Tactic:
sum_mult_eq,

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
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |↑(finrank ℚ K)| *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|
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₀) ^ ∑ i, i.mult) *
      ∏ x_1, (∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
sum_mult_eq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1, (∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
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)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
refine dvd_antisymm
    (orderOf_dvd_iff_pow_eq_one.mpr <| AlgEquiv.coe_toAlgHom_injective <| pB.algHom_ext ?_)
    (orderOf_dvd_iff_pow_eq_one.mpr <| Units.ext ?_)

Goal state after:
case refine_1
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)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ ↑(frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) ^ orderOf (unitOfCoprime (p ^ f) ⋯)) pB.gen = ↑1 pB.gen

case refine_2
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)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ ↑(unitOfCoprime (p ^ f) ⋯ ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P))) = ↑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₀
⊢ (∑ x_1, x ↑x_1 • if x_1 = ⟨w, hw⟩ then ↑1 else ↑0) ∈ Set.Ico 0 1 ↔ x w ∈ Set.Ico 0 1

Tactic:
Int.cast_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1, x ↑x_1 • if x_1 = ⟨w, hw⟩ then 1 else ↑0) ∈ Set.Ico 0 1 ↔ x w ∈ Set.Ico 0 1
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
⊢ ζ - 1 ∣ ↑n

Tactic:
have key : (n : A) = ∑ i ∈ range n, (1 - ζ ^ i) := by
    have hgs : ∑ i ∈ range n, ζ ^ i = 0 := by
      have := geom_sum_mul ζ n
      rw [hζ, sub_self] at this
      exact (mul_eq_zero.1 this).resolve_right fun h ↦ hζ1 (sub_eq_zero.1 h)
    rw [Finset.sum_sub_distrib, hgs, sub_zero, Finset.sum_const, card_range, nsmul_eq_mul, mul_one]
  rw [key]
  refine Finset.dvd_sum fun i _ ↦ ?_
  have h : ζ - 1 ∣ ζ ^ i - 1 := by simpa using sub_dvd_pow_sub_pow ζ 1 i
  rwa [← dvd_neg, neg_sub] at h

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
⊢ |(fderiv_expMap ((completeBasis K).equivFun.symm x) ∘SL ↑(completeBasis K).equivFunL.symm).det| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
det,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |LinearMap.det ↑(fderiv_expMap ((completeBasis K).equivFun.symm x) ∘SL ↑(completeBasis K).equivFunL.symm)| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K