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

Goal state before:
pp: case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma1 N

Tactic:
Gamma1,

Goal state after:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Subgroup.map ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⊤
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: N : ℕ
⊢ Gamma1 N ≤ Gamma0 N

Tactic:
intro x HA
  simp only [Gamma0_mem, Gamma1_mem] at *
  exact HA.2.2

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

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ (mapGL ℝ).range
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0

Tactic:
suffices Γ(N) ≤ (t • 𝒮ℒ ⊓ 𝒮ℒ).comap (mapGL ℝ) by
    have _ : NeZero N := ⟨hN⟩
    simpa only [index_comap] using! (finiteIndex_of_le this).index_ne_zero

Goal state after:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ (mapGL ℝ).range
⊢ Γ(N) ≤ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ IsCusp c (ConjAct.toConjAct h • 𝒢)

Tactic:
suffices (ConjAct.toConjAct h • 𝒢).IsFiniteRelIndex ℋ from hc.of_isFiniteRelIndex
  constructor
  rw [← ℋ.conjAct_pointwise_smul_eq_self (ℋ.le_normalizer hh), 𝒢.relIndex_pointwise_smul]
  exact 𝒢.relIndex_ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
hG : DiscreteTopology ↥𝒢
H : Set (GL (Fin 2) R) := ↑𝒢 ∩ Set.range ⇑upperRightHom
⊢ DiscreteTopology ↥𝒢.strictPeriods

Tactic:
have hH : DiscreteTopology H := hG.of_subset Set.inter_subset_left

Goal state after:
R : Type u_1
inst✝² : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
hG : DiscreteTopology ↥𝒢
H : Set (GL (Fin 2) R) := ↑𝒢 ∩ Set.range ⇑upperRightHom
hH : DiscreteTopology ↑H
⊢ DiscreteTopology ↥𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case succ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih : ⇑(f.pow n) = ⇑f ^ n
⊢ ⇑(f.pow (n + 1)) = ⇑f ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih : ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩
⊢ ⟨(n + 1) • k, GradedMonoid.GMonoid.gnpow (n + 1) f⟩ = ⟨↑(n + 1) * k, f.pow (n + 1)⟩

Tactic:
| succ n ih =>

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

Goal state before:
pp: case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ petersson k ⇑f ⇑f' =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
apply IsBigO.of_norm_left

Goal state after:
case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖petersson k (⇑f) (⇑f') x‖) =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
γ : SL(2, ℤ)
v : ↑(gammaSet N r a)
⊢ (fun v ↦ ⟨↑v ᵥ* ↑γ⁻¹, ⋯⟩) ((fun v ↦ ⟨↑v ᵥ* ↑γ, ⋯⟩) v) = v

Tactic:
by simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_cancel,
    SpecialLinearGroup.coe_one, vecMul_one]

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

Goal state before:
pp: N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ ∑' (x : ↑(gammaSet N 1 a)), eisSummand k (↑x) (γ • z) =
    (∑' (x : ↑(gammaSet N 1 (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))), eisSummand k (↑x) z) *
      denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ k

Tactic:
eisSummand_SL2_apply,

Goal state after:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ ∑' (x : ↑(gammaSet N 1 a)),
      denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ k *
        eisSummand k (↑x ᵥ* ↑γ) z =
    (∑' (x : ↑(gammaSet N 1 (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))), eisSummand k (↑x) z) *
      denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ k
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case neg
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
z : ℂ
H : ¬z = 0
⊢ cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z

Tactic:
· simp [cuspFunction, Periodic.cuspFunction, H]

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

Goal state before:
pp: case succ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h ⇑(f.pow n) = qExpansion h ⇑f ^ n
⊢ qExpansion h ⇑(f.pow (n + 1)) = qExpansion h ⇑f ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: ⊢ Function.LeftInverse (fun x ↦ ⟨⟨↑x.1 * ↑x.2, ⋯⟩, ⟨(↑x.1, ↑x.2), ⋯⟩⟩) fun x ↦ divisorsAntidiagonalFactors x.fst x.snd

Tactic:
rintro ⟨n, ⟨k, l⟩, h⟩

Goal state after:
n : ℕ+
k l : ℕ
h : (k, l) ∈ (↑n).divisorsAntidiagonal
⊢ (fun x ↦ ⟨⟨↑x.1 * ↑x.2, ⋯⟩, ⟨(↑x.1, ↑x.2), ⋯⟩⟩) ((fun x ↦ divisorsAntidiagonalFactors x.fst x.snd) ⟨n, ⟨(k, l), h⟩⟩) =
    ⟨n, ⟨(k, l), h⟩⟩
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : (PowerSeries.coeff 0) (qExpansion 1 ⇑g) = 1
⊢ (f - (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • g).IsCuspForm

Tactic:
by
  rw [isCuspForm_iff_coeffZero_eq_zero, FunLike.coe_sub,
    ModularForm.qExpansion_sub one_pos one_mem_strictPeriods_SL, FunLike.coe_smul,
    ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL, map_sub, PowerSeries.coeff_smul]
  simp [hg]

Goal state after:
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 = 0
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
have hb : g 0 1 = -1 := by
    simpa [-SpecialLinearGroup.det_coe, det_fin_two, hd, hc, neg_eq_iff_eq_neg] using g.property
  have hz' : ‖(z : ℂ)‖ = 1 :=
    le_antisymm (by simpa [denom, hc, hd] using hg') (one_le_normSq_iff.mp hz.1)
  have hg' : g = T ^ g 0 0 * S := by
    ext i j
    simp only [coe_mul, coe_S, coe_T_zpow, Matrix.mul_fin_two, mul_zero, mul_one, zero_add,
      one_mul, add_zero, zero_mul]
    fin_cases i <;> fin_cases j <;> tauto
  rw [hg', mul_smul] at hg
  have hSre : re (S • z) = -z.re := by
    rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]
  have := hg.2
  rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, add_comm, coe_re, hSre] at this
  have := (abs_sub_abs_le_abs_add _ _).trans this
  rw [abs_neg, sub_le_iff_le_add] at this
  rcases lt_or_eq_of_le hz.2 with hzre | hzre
  · have := this.trans_lt ((add_lt_add_iff_left _).mpr hzre)
    rw [add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_lt] at this
    grind [Int.abs_lt_one_iff, zpow_zero]
  · rw [hzre, add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_le,
      Int.abs_le_one_iff] at this
    rcases this with h | h | h <;> simp only [h, Int.cast_zero, zero_add, Int.cast_one] at this
    · grind [zpow_zero]
    · rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre <;> [skip; norm_num [hzre] at this]
      rw [h, zpow_one] at hg'
      refine .inr <| .inr ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) ?_⟩
      simp [hz', show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_ρ]
    · rw [abs_eq (by norm_num)] at hzre
      rcases hzre with hzre | hzre <;> [norm_num [hzre] at this; skip]
      rw [h, zpow_neg_one] at hg'
      exact .inr <| .inl ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) (by rw [hz', norm_ρ])⟩

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

Goal state before:
pp: z : ℍ
⊢ Summable fun m ↦ G2Term z m - δ m

Tactic:
G2Term,

Goal state after:
z : ℍ
⊢ Summable fun m ↦ ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1))⁻¹ + δ m - δ m
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
⊢ HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z

Tactic:
simpa using hasDerivAt_denom_zpow g (-k) z

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:
by
  simp_all only [PowerSeries.coeff_zero_eq_constantCoeff]
  let D := (c4 • p4) ^ 3 - (c6 • p6) ^ 2
  have hD0 : D.coeff 0 = c4 ^ 3 - c6 ^ 2 := by simp [D, hp4_0, hp6_0]
  have hD1 : D.coeff 1 = 720 * c4 ^ 3 + 1008 * c6 ^ 2 := by
    simp [D, pow_succ, PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ]
    grind
  grind [pow_eq_zero_iff, zero_smul]

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

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ∑' (m : ℤ), (1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)) =
    -(2 / ↑↑d) +
      ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑d) + 1 / (-↑↑m * ↑z + -↑↑d) - 1 / (↑↑m * ↑z + ↑↑d) - 1 / (-↑↑m * ↑z + ↑↑d))

Tactic:
by
  rw [eq_neg_add_iff_add_eq (b := 2 / (d : ℂ)), tsum_int_eq_zero_add_tsum_pnat]
  · simp only [Int.cast_zero, zero_mul, zero_sub, one_div, zero_add, Int.cast_natCast, Int.cast_neg,
      neg_mul]
    ring_nf
    rw [← Summable.tsum_add]
    · grind
    · apply (summable_pnat_iff_summable_nat.mpr ((summable_int_iff_summable_nat_and_neg.mp
        (summable_left_one_div_linear_sub_one_div_linear z (-d) d)).1)).congr
      grind [Int.cast_natCast]
    · apply (summable_pnat_iff_summable_nat.mpr ((summable_int_iff_summable_nat_and_neg.mp
        (summable_left_one_div_linear_sub_one_div_linear z (-d) d)).2)).congr
      grind [Int.cast_neg, Int.cast_natCast, neg_mul, one_div]
  · 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 (-↑τ)⁻¹ = (-I * ↑τ) ^ (1 / 2) / (-I * ↑τ) ^ (1 / 2) * jacobiTheta₂ 0 (-1 / ↑τ)

Tactic:
div_self h1,

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
i : ℕ
⊢ ↑p ^ 2 ∣ (↑p * b) ^ 2

Tactic:
simp only [mul_pow, dvd_mul_right]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)

Tactic:
rw [show (2 ^ (1 + 1) : ℤ) = 4 by simp, Int.dvd_iff_emod_eq_zero, Int.add_emod,
      this _ hx_odd, this _ hy_odd]

Goal state after:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬(1 + 1) % 4 = 0
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inr
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
· simp only [Nat.sub_eq_zero_iff_le.mpr hyx,
      Nat.sub_eq_zero_iff_le.mpr (pow_le_pow_left' hyx n), emultiplicity_zero,
      top_add, add_top]

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)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (Subgroup.toAddSubgroup
            (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))))).index ≠
      0 ↔
    (span ℤ (⇑(logEmbeddingEquiv K) '' Set.range (⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0

Tactic:
← LinearEquiv.coe_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (Subgroup.toAddSubgroup
            (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))))).index ≠
      0 ↔
    (span ℤ (⇑↑(logEmbeddingEquiv K) '' Set.range (⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠
      0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) (u • x) ≠ 0

Tactic:
rw [unitSMul_smul, map_mul]

Goal state after:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) * (normAtPlace w) x ≠ 0
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
⊢ ζ • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
rw [Set.mem_ofPred_eq, unitSMul_smul, map_mul, norm_unit, one_mul]
    exact hx.2

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h : Function.Surjective ⇑(unitsMulComplexConjInv K)
ζ : ↥(torsion K)
hζ : Function.Surjective fun x ↦ ζ ^ x
⊢ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤

Tactic:
obtain ⟨u, rfl⟩ := h ζ

Goal state after:
case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h : Function.Surjective ⇑(unitsMulComplexConjInv K)
u : (𝓞 K)ˣ
hζ : Function.Surjective fun x ↦ (unitsMulComplexConjInv K) u ^ x
⊢ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
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 : ℝ
J : ↥(Ideal (𝓞 K))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : (fun a ↦ ⟨idealSetMap K J a, ⋯⟩) x✝¹ = (fun a ↦ ⟨idealSetMap K J a, ⋯⟩) x✝
⊢ x✝¹ = x✝

Tactic:
simp_rw [Subtype.ext_iff, idealSetMap_apply] at h
        rwa [Subtype.ext_iff]

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 * ↑(finrank ℚ K) * (↑(finrank ℚ K))⁻¹ = 0 x✝

Tactic:
mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult - ↑(↑x✝).mult = 0 x✝
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 : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm) Q ∈
    {d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ))}

Tactic:
rw [← primesOverSpanEquivMonicFactorsModAux_symm_apply]

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsModAux✝ ?A).symm ⟨Q, ?hQ⟩) ∈
    {d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ))}

case A
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ ℤ[X]

case hQ
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ Q ∈ (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) ?A)).toFinset
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
⊢ (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})

Tactic:
rw [← Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span hp hQ]

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
⊢ (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩)).LiesOver
    (span {↑p})
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
⊢ (span {↑p, (aeval θ) Q}).IsMaximal

Tactic:
rw [← Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span hp hQ]

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
⊢ (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩)).IsMaximal
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 •
            (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦
              ↑((basisUnitLattice K) (equivFinRank.symm x_1)) i)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
Finsupp.coe_finsetSum,

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

Goal state before:
pp: n i j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
this : ∀ {j : ℕ}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1)
⊢ Associated (ζ ^ j - 1) (ζ ^ i - 1)

Tactic:
by
    grind [Associated.trans, Associated.symm]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : 0 < n
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * ↑n)) = (↑n)⁻¹

Tactic:
have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * ↑n)) = (↑n)⁻¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K)
h₂ : MeasurableSet (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
⊢ volume (normAtAllPlaces ⁻¹' compactSet K) = volume (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))

Tactic:
volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₁,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K)
h₂ : MeasurableSet (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' compactSet K, ∏ w, ENNReal.ofReal (x ↑w) =
    volume (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : ℤ
⊢ house ↑x = ↑|x|

Tactic:
simp only [house, map_intCast, Pi.intCast_def, pi_norm_const, Complex.norm_intCast, Int.cast_abs]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
⊢ ∃ σ, 1 ≤ ‖σ ↑α‖

Tactic:
by
  obtain ⟨w, hw⟩ : ∃ w : InfinitePlace K, 1 ≤ w α := by
    by_contra! h_neg
    let w₀ := Classical.arbitrary (InfinitePlace K)
    have h_ge_one : 1 ≤ w₀ α := InfinitePlace.one_le_of_lt_one hα0 (fun z _ ↦ h_neg z)
    exact (h_neg w₀).not_ge h_ge_one
  use w.embedding
  rwa [InfinitePlace.norm_embedding_eq]

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * max 1 ‖A‖ * ↑B = ∑ x, max 1 ‖A‖ * ↑B
j : β
a✝ : j ∈ univ
⊢ ↑((A i j)⁺ + (A i j)⁻) ≤ max 1 ‖A‖

Tactic:
posPart_add_negPart (A i j),

Goal state after:
case hbc
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * max 1 ‖A‖ * ↑B = ∑ x, max 1 ‖A‖ * ↑B
j : β
a✝ : j ∈ univ
⊢ ↑|A i j| ≤ max 1 ‖A‖