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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ((c • 1) • ⇑f) ∣[k] γ = (c • 1) • ⇑f

Tactic:
← smul_one_smul ℂ,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (((c • 1) • 1) • ⇑f) ∣[k] γ = ((c • 1) • 1) • ⇑f
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
refine ⟨max D E, fun τ hτ ↦ ?_⟩

Goal state after:
E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
⊢ ‖f τ‖ ≤ max D E * τ.im ^ t
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: case refine_3.inl
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
hq : 0 ∈ Metric.ball 0 1
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖UpperHalfPlane.cuspFunction 1 (⇑f) 0‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖

pp: case refine_3.inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖

Tactic:
· refine ⟨0, by simpa only [norm_zero] using exp_nonneg _, le_rfl⟩

Goal state after:
case refine_3.inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case ha
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ 0 ≤ F

Tactic:
rw [← div_le_iff₀ (by positivity)] at hF𝒟

Goal state after:
case ha
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ / (g • τ).im ^ t ≤ F
hg : g • τ ∈ 𝒟
⊢ 0 ≤ F
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:
rw [hgz]
    simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
zpow_neg_one,

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun c ↦ ‖↑↑c ^ (k + 1) * r ^ ↑c‖

Tactic:
apply (summable_norm_pow_mul_geometric_of_norm_lt_one (k + 1) hr).subtype

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

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

Tactic:
rw [norm_pow, mul_comm, Nat.div_mul_cancel (dvd_of_mem_divisors hi)]

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

Goal state before:
pp: case h
⊢ HasProdLocallyUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) (Metric.ball 0 1)

Tactic:
apply hasProdLocallyUniformlyOn_of_forall_compact Metric.isOpen_ball

Goal state after:
case h
⊢ ∀ K ⊆ Metric.ball 0 1,
    IsCompact K → HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: case refine_2
z : ℂ
hz : z ∈ ℍₒ
⊢ Summable fun x ↦ ‖-eta_q x z‖

Tactic:
simpa [eta_q, ← summable_norm_iff] using! summable_eta_q ⟨z, hz⟩

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

Goal state before:
pp: case pos
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : n = -1
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
simp [hb, hn, δ_eq_two]
        ring

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 = -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)
⊢ normSq ↑z = 1 ∧ z.re = 1 / 2

Tactic:
have : 1 ≤ normSq z := hz.1

Goal state after:
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)
this : 1 ≤ normSq ↑z
⊢ normSq ↑z = 1 ∧ z.re = 1 / 2
Module: Mathlib.NumberTheory.ModularForms.Discriminant

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

Tactic:
logDeriv_comp,

Goal state after:
z : ℍ
⊢ logDeriv η (-(↑z)⁻¹) * deriv (fun x ↦ -x⁻¹) ↑z = (↑z ^ 2)⁻¹ * logDeriv η (-(↑z)⁻¹)

case hf
z : ℍ
⊢ DifferentiableAt ℂ η (-(↑z)⁻¹)

case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Set.EqOn (logDeriv (η ∘ fun z ↦ -1 / z)) (logDeriv (sqrt * η)) upperHalfPlaneSet

Tactic:
exact fun z hz ↦ logDeriv_eta_comp_eq_logDeriv_csqrt_eta ⟨z, hz⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
suffices (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ by simp +contextual [-sl_moeb, or_imp, this]

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case inr
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
hb : b ≠ 0
⊢ ∑' (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

Tactic:
have : NeZero b := ⟨hb⟩
    simpa [eisSummand_of_gammaSet_eq_divIntMap k z, tsum_mul_left, hb]
      using (gammaSetDivGcdEquiv b).tsum_eq (eisSummand k · z)

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

Goal state before:
pp: ⊢ E₄CubeSubE₆SqForm.IsCuspForm

Tactic:
by
  simp [isCuspForm_iff_coeffZero_eq_zero, E₄CubeSubE₆SqForm_qExpansion_eq,
    PowerSeries.coeff_mul, -PowerSeries.coeff_zero_eq_constantCoeff,
    E_qExpansion_coeff_zero _ ⟨2, rfl⟩, E_qExpansion_coeff_zero _ ⟨3, rfl⟩]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: τ : ℍ
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im

Tactic:
obtain ⟨γ, hγ⟩ := exists_smul_mem_fd τ

Goal state after:
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: ⊢ (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (modularForm CuspForm.discriminant) =
    (1 / 1728) •
      ((DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (E₄.pow 3) -
        (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (E₆.pow 2))

Tactic:
← map_sub (DirectSum.of (ModularForm 𝒮ℒ) 12),

Goal state after:
⊢ (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (modularForm CuspForm.discriminant) =
    (1 / 1728) • (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (E₄.pow 3 - E₆.pow 2)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: case h
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
r : ↥ℋ
⊢ quotientFunc f ⟦r⟧ ∣[k] h = quotientFunc f (⟨h, hh⟩⁻¹ • ⟦r⟧)

Tactic:
simp [SlashAction.slash_mul]

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
⊢ (Ideal.Quotient.mk (span {s})) (∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) =
    ∑ i ∈ range p, (Ideal.Quotient.mk (span {s})) ((a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) * a ^ (p - 1 - i))

Tactic:
s,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {↑p ^ 2})) (∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) =
    ∑ x ∈ range p, (Ideal.Quotient.mk (span {↑p ^ 2})) ((a ^ (x - 1) * (↑p * b) * ↑x + a ^ x) * a ^ (p - 1 - x))
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
r : ℝ
hr : Complex.ofRealHom r = v.embedding x
⊢ (star v.embedding) x = v.embedding x

Tactic:
simp [ComplexEmbedding.conjugate_coe_eq, ← hr, Complex.conj_ofReal]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p * ↑p ∣ ↑p * y ^ (p - 1)

Tactic:
mul_dvd_mul_iff_left hp.ne_zero

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ∣ y ^ (p - 1)
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 : cofinite ≤ 𝓟 S
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
le_principal_iff,

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 ∈ cofinite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A✝ : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i : ι
x : G i
⊢ ∀ a ∈ {i}ᶜ, Pi.mulSingle i x a ∈ ↑(A a)

Tactic:
simp_all

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2.succ
x✝ y : ℤ
hx✝ : ¬2 ∣ x✝
hxy : 4 ∣ x✝ - y
hx_odd : Odd x✝
hxy_even : Even (x✝ - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
⊢ x ^ 2 ^ (i + 1) % 4 = 1

Tactic:
rw [pow_succ', mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 ↑(n + 1)

Tactic:
have h : FiniteMultiplicity 2 n.succ := Nat.finiteMultiplicity_iff.mpr ⟨by simp, n.succ_pos⟩

Goal state after:
case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 n.succ
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 ↑(n + 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ (∀ (a : InfinitePlace K) (b : a.IsComplex), (x✝.1 a, x✝.2 ⟨a, b⟩) ∈ Complex.polarCoord.target) ↔
    (∀ (i : InfinitePlace K), i.IsComplex → x✝.1 i ∈ Set.Ioi 0) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex), x✝.2 ⟨a, b⟩ ∈ Set.Ioo (-π) π

Tactic:
Complex.polarCoord_target,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ (∀ (a : InfinitePlace K) (b : a.IsComplex), (x✝.1 a, x✝.2 ⟨a, b⟩) ∈ Set.Ioi 0 ×ˢ Set.Ioo (-π) π) ↔
    (∀ (i : InfinitePlace K), i.IsComplex → x✝.1 i ∈ Set.Ioi 0) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex), x✝.2 ⟨a, b⟩ ∈ Set.Ioo (-π) π
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ 0 = 0 x✝

Tactic:
Pi.zero_apply

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ 0 = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
⊢ u • x ∈ fundamentalCone K ↔ u ∈ torsion K

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
⊢ u ∈ torsion K
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
h₁ : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h₂ : (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2

Tactic:
h₂,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h₁ : indexRealUnits K * 1 = 2
h₂ : (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2
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
h₁ : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h₂ : (unitsMulComplexConjInv K).range.index = 2
⊢ indexRealUnits K = 1

Tactic:
h₂,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h₁ : indexRealUnits K * 2 = 2
h₂ : (unitsMulComplexConjInv K).range.index = 2
⊢ indexRealUnits K = 1
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case refine_1
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|
⊢ ∀ (i : Fin (rank K)), ∑ j, of (fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))) i j = 0

Tactic:
· intro _
    simp_rw [of_apply, ← Real.log_pow]
    rw [← Real.log_prod, Equiv.prod_comp f (fun w ↦ (w (u _) ^ (mult w))), prod_eq_abs_norm,
      Units.norm, Rat.cast_one, Real.log_one]
    exact fun _ _ ↦ pow_ne_zero _ <| (map_ne_zero _).mpr (coe_ne_zero _)

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' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ regOfFamily u = |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e i))))).det|

Tactic:
by
  simp [regOfFamily_eq_det', abs_det_eq_abs_det u e (equivFinRank K).symm, logEmbedding]

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₀ }
⊢ 0 = 0 x✝

Tactic:
Pi.zero_apply

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ 0 = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
⊢ (completeBasis K) w i =
    if h : w = w₀ then ↑i.mult
    else ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, h⟩))))

Tactic:
split_ifs with hw

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

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ (completeBasis K) w i = ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩))))
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ 0
hj : j.Coprime 0
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ 1
hj : j.Coprime 1
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hj_Unit : IsUnit ↑j
hζ : IsPrimitiveRoot ζ 0
hj : j.Coprime 0
⊢ IsUnit (∑ i ∈ range j, ζ ^ i)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hj_Unit : IsUnit ↑j
hζ : IsPrimitiveRoot ζ 1
hj : j.Coprime 1
⊢ IsUnit (∑ i ∈ range j, ζ ^ i)

Tactic:
simp_all

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : (absNorm P).Coprime (torsionOrder K)
this : P.IsMaximal
x✝ : Field (𝓞 K ⧸ P) := Quotient.field P
hP₃ : absNorm P ≠ 1
h : Nat.card ↥(torsion K) ∣ Nat.card (𝓞 K ⧸ P)ˣ
⊢ torsionOrder K ∣ absNorm P - 1

Tactic:
Nat.card_units

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : (absNorm P).Coprime (torsionOrder K)
this : P.IsMaximal
x✝ : Field (𝓞 K ⧸ P) := Quotient.field P
hP₃ : absNorm P ≠ 1
h : Nat.card ↥(torsion K) ∣ Nat.card (𝓞 K ⧸ P) - 1
⊢ torsionOrder K ∣ absNorm P - 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
x✝ : (∀ (w : InfinitePlace K), ¬w = w₀ → ↑expMapBasis.symm x w ∈ Set.Ico 0 1) ∧ ↑expMapBasis.symm x w₀ ≤ 0
w : InfinitePlace K
h₁ : ∀ (w : InfinitePlace K), ¬w = w₀ → ↑expMapBasis.symm x w ∈ Set.Ico 0 1
h₂ : ↑expMapBasis.symm x w₀ ≤ 0
⊢ ↑expMapBasis.symm x w ∈ if w = w₀ then Set.Iic 0 else Set.Ico 0 1

Tactic:
split_ifs with hw

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
x✝ : (∀ (w : InfinitePlace K), ¬w = w₀ → ↑expMapBasis.symm x w ∈ Set.Ico 0 1) ∧ ↑expMapBasis.symm x w₀ ≤ 0
w : InfinitePlace K
h₁ : ∀ (w : InfinitePlace K), ¬w = w₀ → ↑expMapBasis.symm x w ∈ Set.Ico 0 1
h₂ : ↑expMapBasis.symm x w₀ ≤ 0
hw : w = w₀
⊢ ↑expMapBasis.symm x w ∈ Set.Iic 0

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
x✝ : (∀ (w : InfinitePlace K), ¬w = w₀ → ↑expMapBasis.symm x w ∈ Set.Ico 0 1) ∧ ↑expMapBasis.symm x w₀ ≤ 0
w : InfinitePlace K
h₁ : ∀ (w : InfinitePlace K), ¬w = w₀ → ↑expMapBasis.symm x w ∈ Set.Ico 0 1
h₂ : ↑expMapBasis.symm x w₀ ≤ 0
hw : ¬w = w₀
⊢ ↑expMapBasis.symm x w ∈ Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case neg
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : ¬p = 2
⊢ Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p

Tactic:
hζ.norm_toInteger_sub_one_of_prime_ne_two h

Goal state after:
case neg
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : ¬p = 2
⊢ Associated ↑p ↑p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)

Tactic:
have h := isPrime_span_zeta_sub_one p k hζ

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : (span {hζ.toInteger - 1}).IsPrime
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)