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

Goal state before:
pp: case 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 ^ 0
hre : (g • z).re = ↑b + z.re
hb : b = 0
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
hgz

Goal state after:
case 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 ^ 0
hre : (g • z).re = ↑b + z.re
hb : b = 0
⊢ (T ^ 0 = T ∨ T ^ 0 = -T) ∧ z.re = -1 / 2 ∨ (T ^ 0 = T⁻¹ ∨ T ^ 0 = -T⁻¹) ∧ z.re = 1 / 2 ∨ T ^ 0 = 1 ∨ T ^ 0 = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : ↑|↑g 1 1| ≤ 1 + 1 / 2
⊢ |↑g 1 1| ≤ 1

Tactic:
← Int.le_floor

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑g 1 1| ≤ ⌊1 + 1 / 2⌋
⊢ |↑g 1 1| ≤ 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ G2 z = (↑z ^ 2)⁻¹ * G2 (S • z) - -2 * ↑π * I / ↑z

Tactic:
by
  rw [G2_S_action_eq_tsum_G2Term, G2_eq_tsum_G2Term z, ← tsum_G2Term_eq_tsum',
  tsum_G2Term_eq_tsum]

Goal state after:
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 ^ 2

Tactic:
one_pow

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 = 1
Module: Mathlib.NumberTheory.ModularForms.Derivative

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

Tactic:
ext z
  have hLHS : (serreDerivative (k : ℂ) F ∣[k + 2] γ) z =
      (D F ∣[k + 2] γ) z - ↑k * 12⁻¹ * ((EisensteinSeries.E2 ∣[(2 : ℤ)] γ) z * (F ∣[k] γ) z) := by
    grind [ModularForm.SL_slash_apply, serreDerivative_apply, Pi.mul_apply,
      congrFun (ModularForm.mul_slash_SL2 2 k γ EisensteinSeries.E2 F) z]
  have hDz : (D (F ∣[k] γ)) z = (D F ∣[k + 2] γ) z -
      (k * (2 * π * I)⁻¹ * (γ 1 0 / denom γ z) * (F ∣[k] γ) z) := by
    simp [normalizedDerivOfComplex_SL_slash hF]
  have hE2z : (EisensteinSeries.E2 ∣[(2 : ℤ)] γ) z =
      EisensteinSeries.E2 z - 1 / (2 * riemannZeta 2) * EisensteinSeries.D2 γ z := by
    simp [EisensteinSeries.E2_slash_action]
  grind [serreDerivative_apply, EisensteinSeries.D2, riemannZeta_two, I_sq]

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

Goal state before:
pp: ⊢ 1 ^ 3 = 1

Tactic:
one_pow

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

Goal state before:
pp: z : ℍ
N : ℕ
⊢ ↑2 * ∑ k ∈ range N, e2Summand (↑(k + 1)) z + 2 • e2Summand 0 z - e2Summand 0 z =
    2 * riemannZeta 2 + ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)

Tactic:
e2Summand_zero_eq_two_riemannZeta_two

Goal state after:
z : ℍ
N : ℕ
⊢ ↑2 * ∑ k ∈ range N, e2Summand (↑(k + 1)) z + 2 • (2 * riemannZeta 2) - 2 * riemannZeta 2 =
    2 * riemannZeta 2 + ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr.inr
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
⊢ 1 + ↑(if k % 12 = 2 % 12 then (k - 12) / 12 else (k - 12) / 12 + 1) =
    ↑(if k % 12 = 2 % 12 then (k - 12) / 12 + 1 else (k - 12) / 12 + 1 + 1)

Tactic:
split_ifs

Goal state after:
case pos
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
h✝ : k % 12 = 2 % 12
⊢ 1 + ↑((k - 12) / 12) = ↑((k - 12) / 12 + 1)

case neg
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
h✝ : ¬k % 12 = 2 % 12
⊢ 1 + ↑((k - 12) / 12 + 1) = ↑((k - 12) / 12 + 1 + 1)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
⊢ FiniteDimensional ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)

Tactic:
rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]

Goal state after:
k : ℤ
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr.inl
k : ℕ
hk_even : Even ↑k
⊢ ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) < Cardinal.aleph0

Tactic:
split_ifs

Goal state after:
case pos
k : ℕ
hk_even : Even ↑k
h✝ : k ≡ 2 [MOD 12]
⊢ ↑(k / 12) < Cardinal.aleph0

case neg
k : ℕ
hk_even : Even ↑k
h✝ : ¬k ≡ 2 [MOD 12]
⊢ ↑(k / 12 + 1) < Cardinal.aleph0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ x.re ∈ Set.Ioo (-(1 / 2)) (1 / 2)

Tactic:
← interior_Icc

Goal state after:
case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ x.re ∈ interior (Set.Icc (-(1 / 2)) (1 / 2))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im ≤ τ.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ)
⊢ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

Tactic:
le_div_iff₀ (normSq_denom_pos γ τ.im_ne_zero),

Goal state after:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im * normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ) ≤ τ.im
⊢ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
c✝ : OnePoint ℝ
h : IsCusp c✝ ℋ
γ : GL (Fin 2) ℝ
⊢ γ • OnePoint.infty = c✝ →
    IsBoundedAtImInfty ((SlashInvariantForm.norm ℋ f).toFun ∣[k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ)

Tactic:
rintro rfl
    simp_rw [SlashInvariantForm.norm, IsBoundedAtImInfty, Filter.BoundedAtFilter]
    let := Fintype.ofFinite 𝒬
    rw [Nat.card_eq_fintype_card, ← Finset.card_univ, ModularForm.prod_slash]
    apply Asymptotics.IsBigO.const_smul_left
    rw [show (1 : ℍ → ℝ) = (fun x ↦ ∏ (i : 𝒬), 1) by ext; simp, Finset.prod_fn]
    refine .finsetProd (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)
    simpa using h.of_isFiniteRelIndex_conj hr

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
c✝ : OnePoint ℝ
h : IsCusp c✝ ℋ
γ : GL (Fin 2) ℝ
⊢ γ • OnePoint.infty = c✝ →
    IsBoundedAtImInfty ((SlashInvariantForm.norm ℋ f).toFun ∣[k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ)

Tactic:
by
    rintro rfl
    simp_rw [SlashInvariantForm.norm, IsBoundedAtImInfty, Filter.BoundedAtFilter]
    let := Fintype.ofFinite 𝒬
    rw [Nat.card_eq_fintype_card, ← Finset.card_univ, ModularForm.prod_slash]
    apply Asymptotics.IsBigO.const_smul_left
    rw [show (1 : ℍ → ℝ) = (fun x ↦ ∏ (i : 𝒬), 1) by ext; simp, Finset.prod_fn]
    refine .finsetProd (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)
    simpa using h.of_isFiniteRelIndex_conj hr

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)
S : Set ι
⊢ TopologicalSpace.induced DFunLike.coe inferInstance ≤
    TopologicalSpace.coinduced id (TopologicalSpace.induced DFunLike.coe inferInstance)

Tactic:
@coinduced_id

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
S : Set ι
⊢ TopologicalSpace.induced DFunLike.coe inferInstance ≤ TopologicalSpace.induced DFunLike.coe inferInstance
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
inst✝ : CuspFormClass F Γ k
⊢ Differentiable ℂ (L hk f)

Tactic:
unfold L
  simp only [div_eq_mul_inv]
  fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ Continuous fun a ↦ if hw : w.IsReal then a.1 ⟨w, hw⟩ else (a.2 ⟨w, ⋯⟩).1

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : w.IsReal
⊢ Continuous fun a ↦ a.1 ⟨w, h✝⟩

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : ¬w.IsReal
⊢ Continuous fun a ↦ (a.2 ⟨w, ⋯⟩).1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case e_a
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)
w : InfinitePlace K
x✝ : w ∈ Set.univ
⊢ (if w.IsReal then Set.univ else Set.Ioi 0) =ᵐ[volume] if w.IsReal then Set.univ else Set.Ici 0

Tactic:
split_ifs

Goal state after:
case pos
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)
w : InfinitePlace K
x✝ : w ∈ Set.univ
h✝ : w.IsReal
⊢ Set.univ =ᵐ[volume] Set.univ

case neg
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)
w : InfinitePlace K
x✝ : w ∈ Set.univ
h✝ : ¬w.IsReal
⊢ Set.Ioi 0 =ᵐ[volume] Set.Ici 0
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case refine_2
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |(↑↑0 - ↑↑(f.symm w₂)).negOnePow •
        ((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
            (f.symm w₂).succAbove).det|
⊢ |((reindex e₁ e₁) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i)))))).det| =
    |((reindex g g)
          ((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
            id)).det|

Tactic:
rw [Units.smul_def, abs_zsmul, Int.abs_negOnePow, one_smul] at h

Goal state after:
case refine_2
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
          (f.symm w₂).succAbove).det|
⊢ |((reindex e₁ e₁) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i)))))).det| =
    |((reindex g g)
          ((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
            id)).det|
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
⊢ regOfFamily (realFundSystem K) = 2 ^ rank K * regulator ↥K⁺

Tactic:
let f : {w : InfinitePlace K // w ≠ W₀} ≃ {w : InfinitePlace K⁺ // w ≠ w₀} :=
    (equivInfinitePlace K).subtypeEquiv fun w ↦ by rw [not_iff_not, Equiv.eq_symm_apply]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
⊢ regOfFamily (realFundSystem K) = 2 ^ rank K * regulator ↥K⁺
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inr.inr
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
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
have : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding := ⟨hr⟩

Goal state after:
case inr.inr
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
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
⊢ Module.finrank v.Completion w.Completion = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
⊢ realSpaceToLogSpace (↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x))) = logMap ((mixedEmbedding K) x)

Tactic:
ext w
  simp_rw [realSpaceToLogSpace_apply, sum_expMap_symm_apply hx, expMap_symm_apply,
    logMap, normAtPlace_apply, mul_sub, mul_assoc, norm_eq_norm]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ realSpaceToLogSpace (completeFamily K w₀) = 0

Tactic:
ext
  rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ (algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, ⋯⟩)) ≠ 0

Tactic:
exact coe_ne_zero _

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x : ↥(maximalRealSubfield K)
⊢ (algebraMap F K) ((equivMaximalRealSubfield F K).symm x) = (algebraMap (↥(maximalRealSubfield K)) K) x

Tactic:
simpa using! (equivMaximalRealSubfield_apply F K ((equivMaximalRealSubfield F K).symm x)).symm

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
⊢ ↑expMap (x w₀ • (completeBasis K) w₀) * ↑expMap (∑ i, x ↑i • (completeBasis K) ↑i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
expMap_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMap ((completeBasis K) w₀) ^ x w₀ * ↑expMap (∑ i, x ↑i • (completeBasis K) ↑i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, 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
⊢ (fun i ↦ Real.exp (x w₀) * (∏ i, ↑expMap (x ↑i • (completeBasis K) ↑i)) i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
expMap_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (fun i ↦ Real.exp (x w₀) * (∏ x_1, ↑expMap ((completeBasis K) ↑x_1) ^ x ↑x_1) i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
⊢ (span {↑p, (aeval θ) Q}).inertiaDeg ℤ = (Polynomial.map (Int.castRingHom (ZMod p)) Q).natDegree

Tactic:
inertiaDeg_eq_of_isMaximal (span {(p : ℤ)}),

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
⊢ Module.finrank (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}) =
    (Polynomial.map (Int.castRingHom (ZMod p)) Q).natDegree
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₀
⊢ 1 ^ finrank ℚ K = 1

Tactic:
one_pow

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ 1 = 1
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: case inr
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this✝ : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
this :
  ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_1 : IsDomain A],
    IsPrimitiveRoot ζ p →
      Nat.Prime p →
        NeZero p →
          ∀ i < p,
            ζ ^ i ∈ ↑(nthRootsFinset p 1) →
              ∀ j < p, ζ ^ j ∈ ↑(nthRootsFinset p 1) → ζ ^ i ≠ ζ ^ j → j ≤ i → Associated (ζ - 1) (ζ ^ i - ζ ^ j)
hij : ¬j ≤ i
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

Tactic:
simpa using (this hζ ‹_› ‹_› _ hj ‹_› _ hi ‹_› e.symm (by lia)).neg_right

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
⊢ MeasurableSet (if x✝ = w₀ then Set.Iic 0 else Set.Ico 0 1)

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
h✝ : x✝ = w₀
⊢ MeasurableSet (Set.Iic 0)

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
h✝ : ¬x✝ = w₀
⊢ MeasurableSet (Set.Ico 0 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ interior (paramSet K) ⊆ expMapBasis.source

Tactic:
simp [expMapBasis_source]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : w ∈ Set.univ
⊢ (if w = w₀ then Set.Iic 0 else Set.Icc 0 1) =ᵐ[volume] if w = w₀ then Set.Iio 0 else Set.Ioo 0 1

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : w ∈ Set.univ
h✝ : w = w₀
⊢ Set.Iic 0 =ᵐ[volume] Set.Iio 0

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : w ∈ Set.univ
h✝ : ¬w = w₀
⊢ Set.Icc 0 1 =ᵐ[volume] Set.Ioo 0 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ IsCompact (if w = w₀ then {0} else Set.Icc 0 1)

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
h✝ : w = w₀
⊢ IsCompact {0}

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
h✝ : ¬w = w₀
⊢ IsCompact (Set.Icc 0 1)
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ξ K x = 0
⊢ x = 0

Tactic:
ext ⟨l, r⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ξ K x = 0
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f x ^ c = g x

Tactic:
rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ↑(∏ i, #(Icc (∑ j, ↑B * -(A i j)⁻) (∑ j, ↑B * (A i j)⁺))) = ∏ i, (P i - N i + 1)

Tactic:
Nat.cast_prod

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ∏ i, ↑(#(Icc (∑ j, ↑B * -(A i j)⁻) (∑ j, ↑B * (A i j)⁺))) = ∏ i, (P i - N i + 1)