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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ 1 / h *
      (1 / Real.exp (↑n * (-2 * Real.pi * (↑x + 1 / ↑n * I).im / h)) *
        ‖f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }‖) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * ↑n ^ e))

Tactic:
gcongr

Goal state after:
case a
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := ⋯
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := ⋯
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ -2 * Real.pi / h ≤ ↑n * (-2 * Real.pi * (↑x + 1 / ↑n * I).im / h)

case h₂
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := ⋯
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := ⋯
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ ‖f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }‖ ≤ C * ↑n ^ e
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case h₂
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := ⋯
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := ⋯
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ ‖f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }‖ ≤ C * ↑n ^ e

Tactic:
grw [hn' _ (by simp [← UpperHalfPlane.coe_im])]
      simp [← UpperHalfPlane.coe_im, Real.rpow_neg_eq_inv_rpow, hne]

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ↑(↑b).divisors.card * ‖↑↑b‖ ^ k * ‖r‖ ^ ↑b ≤ ‖↑↑b‖ * ‖↑↑b‖ ^ k * ‖r‖ ^ ↑b

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ↑(↑b).divisors.card ≤ ‖↑↑b‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
⊢ ↑(↑(A * B) 1 0) * denom (toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B)) ↑z =
    ↑(↑A 1 0) * ↑(↑B).det +
      ↑(↑B 1 0) *
        denom
          (toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A) *
            toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B))
          ↑z

Tactic:
have h0 := Matrix.two_mul_expl A.1 B.1
  simp only [Fin.isValue, coe_mul, h0.2.2.1, Int.cast_add, Int.cast_mul, ModularGroup.denom_apply,
    Matrix.det_fin_two B.1, Int.cast_sub, ← map_mul, h0.2.2.2]
  ring

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
modular_T_zpow_smul,

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

Goal state before:
pp: z : ℍ
⊢ logDeriv (η ∘ fun x ↦ -1 / x) ↑z = (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹

Tactic:
simp only [neg_div, one_div, inv_neg]

Goal state after:
z : ℍ
⊢ logDeriv (η ∘ fun x ↦ -x⁻¹) ↑z = (↑z ^ 2)⁻¹ * logDeriv η (-(↑z)⁻¹)
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ Δ z ≠ 0

Tactic:
simpa [discriminant] using eta_ne_zero z.2

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‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖cexp (2 * ↑π * I * z / ↑p)‖ ^ n ≤ ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
hr : ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ < 1
⊢ ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * ‖cexp (2 * ↑π * I * ↑n * z / ↑p)‖ ≤
    ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n

Tactic:
gcongr

Goal state after:
case hbc
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, ℂ) := ⋯
r : ℝ := ⋯
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖cexp (2 * ↑π * I * z / ↑p)‖ ^ n ≤ ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
hr : ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ < 1
⊢ ‖cexp (2 * ↑π * I * ↑n * z / ↑p)‖ ≤ ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
⊢ g • ρ = ρ ↔ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}

Tactic:
by
  constructor
  · intro hg
    have neS : g ≠ S ∧ g ≠ -S := by
      have : S • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow]
      grind [SL_neg_smul]
    have neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹ := by
      have : T • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]
        norm_num
      have : T⁻¹ • ρ ≠ ρ := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
      grind [SL_neg_smul]
    have neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T) := by
      have : (T * S * T) • ρ ≠ ρ := by
        simp only [mul_smul, modular_T_smul, modular_S_smul,
          ne_eq, UpperHalfPlane.ext_iff, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow, normSq]
      grind [SL_neg_smul]
    have := cases_of_mem_fd_smul_mem_fd ρ_mem_fd (hg ▸ ρ_mem_fd)
    norm_num [UpperHalfPlane.ext_iff, Complex.ext_iff, norm_ρ, ρ, neS, neT, neTST] at this
    grind
  · suffices (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ by simp +contextual [-sl_moeb, or_imp, this]
    rw [mul_smul T⁻¹, inv_smul_eq_iff, ← eq_inv_smul_iff (g := S), S_inv, SL_neg_smul,
      mul_smul, eq_comm, and_self, modular_T_smul, modular_S_smul, UpperHalfPlane.ext_iff]
    norm_num [ρ, Complex.ext_iff, normSq, ← pow_two, div_pow]

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

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))

Tactic:
gcongr

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ ↑((σ (k - 1)) n) * ‖cexp (2 * ↑π * I * ↑z)‖ ^ n ≤ ↑n ^ k * ‖cexp (2 * ↑π * I * ↑z)‖ ^ n

Tactic:
gcongr

Goal state after:
case hbc
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ ↑((σ (k - 1)) n) ≤ ↑n ^ k
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))

Tactic:
gcongr

Goal state after:
case hd
y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 0 < 1 - rexp (-(π * 1))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

pp: case inr
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

Tactic:
· exact ⟨1, (one_smul SL(2, ℤ) τ).symm ▸ h, by
      simp only [map_one, denom_one, norm_one, le_refl]⟩

Goal state after:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).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
⊢ ModularForm.norm ℋ f = 0 ↔ ⇑f = 0

Tactic:
refine ⟨fun hn ↦ ?_, fun hf ↦ ?_⟩

Goal state after:
case refine_1
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hn : ModularForm.norm ℋ f = 0
⊢ ⇑f = 0

case refine_2
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ⇑f = 0
⊢ ModularForm.norm ℋ f = 0
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), {g | g ∈ H ∧ (g • t • K ∩ L).Nonempty}.Finite
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G)) S
hT : (Subtype.val '' S).Finite
⊢ {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
have hS' {g : Γ} (hg : g ∈ G) : ∃ t ∈ Subtype.val '' S, g * t⁻¹ ∈ H := by
    obtain ⟨p, hp⟩ := (hS.existsUnique ⟨g, hg⟩).exists
    aesop

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), {g | g ∈ H ∧ (g • t • K ∩ L).Nonempty}.Finite
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G)) S
hT : (Subtype.val '' S).Finite
hS' : ∀ {g : Γ}, g ∈ G → ∃ t ∈ Subtype.val '' S, g * t⁻¹ ∈ H
⊢ {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
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 ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
set U : Set (Π i, R i) := Sᶜ.pi K

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
⊢ v.intValuation d < 1

Tactic:
have := intValuation_le_one v n

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : v.intValuation n ≤ 1
⊢ v.intValuation d < 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: k : ℤ
hk : Odd k
⊢ 8 ∣ k ^ 2 - 1

Tactic:
rcases hk with ⟨m, rfl⟩

Goal state after:
m : ℤ
⊢ 8 ∣ (2 * m + 1) ^ 2 - 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: k : ℕ
hk : Odd k
⊢ 8 ∣ k ^ 2 - 1

Tactic:
rcases hk with ⟨m, rfl⟩

Goal state after:
m : ℕ
⊢ 8 ∣ (2 * m + 1) ^ 2 - 1
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 * 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))⁻¹)

Tactic:
Real.log_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) + Real.log ((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))⁻¹)

case hx
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₀ }
⊢ (normAtPlace ↑w) x ≠ 0

case hy
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₀ }
⊢ (normAtPlace ↑w) y ≠ 0
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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
h₂ : DiscreteTopology ↥(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))))
⊢ IsMaxRank u ↔ (Subgroup.closure (Set.range u)).FiniteIndex

Tactic:
rw [finiteIndex_iff_sup_torsion_finiteIndex, finiteIndex_iff, h₁, finiteQuotient_iff,
    unitLattice_rank, ← Set.finrank, IsMaxRank, linearIndependent_iff_card_eq_finrank_span,
    Real.finrank_eq_int_finrank_of_discrete h₂, Set.finrank, Set.finrank, ← finrank_map_subtype_eq,
    map_span, ← Set.range_comp', eq_comm]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
h₂ : DiscreteTopology ↥(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))))
⊢ finrank ℤ ↥(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i)))) = Fintype.card (Fin (rank K)) ↔
    finrank ℤ
        ↥(span ℤ
            (Set.range fun x ↦
              (unitLattice K).subtype ((⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u) x))) =
      rank K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet (fundamentalCone K)

Tactic:
refine MeasurableSet.diff ?_ ?_

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet
    (logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet {x | mixedEmbedding.norm x = 0}
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 ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
simpa [norm_eq_of_normAtPlace_eq hy] using hx.2

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
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
hx : x ∈ integerSet K
⊢ ζ • x ∈ integerSet K

Tactic:
obtain ⟨a, ⟨_, rfl⟩, rfl⟩ := (mem_integerSet.mp hx).2

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
a : 𝓞 K
hx : (mixedEmbedding K) ↑a ∈ integerSet K
⊢ ζ • (mixedEmbedding K) ↑a ∈ integerSet K
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✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : (complexConj K) ↑x = ↑x
⊢ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K))

Tactic:
RingOfIntegers.complexConj_eq_self_iff

Goal state after:
case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x
⊢ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K))
Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

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
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ ↑((algebraMap K (WithAbs ↑w)) x) =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) (WithAbs.toAbs (↑v) x)) }.toCompletion

Tactic:
simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply]

Goal state after:
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
this✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
this : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivComplexOfIsComplex hv)
        ((ringEquivComplexOfIsComplex (LiesOver.isComplex_of_isComplex_under _ hv)).trans
          (starRingAut (R := ℂ))) (by ext; simp [← conjugate_coe_eq]),
        Module.finrank_self]

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 * ∑ w', ↑w'.mult) * (↑(finrank ℚ K))⁻¹ = 0 x✝

Tactic:
← Nat.cast_sum,

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

Tactic:
← Nat.cast_sum,

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 : ↑(∑ x, x.mult) = 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:
← Nat.cast_sum,

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 =
    |↑(∑ 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|
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 ⋯
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
rw [← powerBasis_dim hPirr.ne_zero, ← pB.finrank, ← orderOf_frobeniusAlgEquivOfAlgebraic]

Goal state after:
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 ⋯
⊢ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = orderOf (unitOfCoprime (p ^ f) ⋯)