mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case coe
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • ↑c = ↑c
⊢ 0 ≤ (↑g).discr

Tactic:
have : g.val.discr = (2 * g 1 0 * c + (g 1 1 + -g 0 0)) ^ 2 := by
      replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h
      simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]
      grind

Goal state after:
case coe
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • ↑c = ↑c
this : (↑g).discr = (2 * ↑g 1 0 * c + (↑g 1 1 + -↑g 0 0)) ^ 2
⊢ 0 ≤ (↑g).discr
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: c : OnePoint ℝ
⊢ IsCusp c (mapGL ℝ).range ↔ c ∈ Set.range (OnePoint.map Rat.cast)

Tactic:
constructor
  · rintro ⟨-, ⟨g, rfl⟩, hgp, hgc⟩
    simpa only [hgp.smul_eq_self_iff.mp hgc] using ⟨(mapGL ℚ g).parabolicFixedPoint,
      by simp [GeneralLinearGroup.parabolicFixedPoint, apply_ite]⟩
  · rintro ⟨c, rfl⟩
    obtain ⟨a, rfl⟩ := c.exists_mem_SL2 ℤ
    refine ⟨_, ⟨a * ModularGroup.T * a⁻¹, rfl⟩, ?_, ?_⟩
    · suffices (mapGL ℝ ModularGroup.T).IsParabolic by simpa
      refine ⟨fun ⟨a, ha⟩ ↦ zero_ne_one' ℝ (by simpa [ModularGroup.T] using congr_fun₂ ha 0 1), ?_⟩
      simp [discr_fin_two, trace_fin_two, det_fin_two, ModularGroup.T]
      norm_num
    · rw [← Rat.coe_castHom, ← (Rat.castHom ℝ).algebraMap_toAlgebra]
      simp [OnePoint.map_smul, mul_smul, smul_infty_eq_self_iff, ModularGroup.T]

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

Goal state before:
pp: case left
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods ≠ 0

pp: case right
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.periods.relIndex 𝒢.strictPeriods ≠ 0

Tactic:
· rcases 𝒢.relIndex_strictPeriods with h | h <;> simp [h]

Goal state after:
case right
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.periods.relIndex 𝒢.strictPeriods ≠ 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0

Tactic:
apply inv_ne_zero

Goal state after:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
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:
obtain ⟨ξ, hξ, hξ₂⟩ := exists_one_half_le_im_and_norm_le hk f
        ⟨_, im_invQParam_pos_of_norm_lt_one Real.zero_lt_one (mem_ball_zero_iff.mp hq) hq'⟩
      exact ⟨_, norm_qParam_le_of_one_half_le_im hξ,
        by simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL
            one_ne_zero, qParam_right_inv one_ne_zero hq'] using hξ₂⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
this : |↑n| < 1
⊢ n = 0

Tactic:
rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c' ^ 2 ≤ 1 ^ 2
⊢ |↑g 1 0| ≤ 1

Tactic:
sq_le_sq,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : |c'| ≤ |1|
⊢ |↑g 1 0| ≤ 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 ≤ 1
⊢ c ^ 4 * z.im ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 * 16 ≤ 16

Tactic:
rw [← mul_pow]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 ≤ 1
⊢ (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 * 16 ≤ 16
Module: Mathlib.NumberTheory.Modular

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

Tactic:
rw [hgz, zpow_one, eq_self_iff_true, true_or, true_and]

Goal state after:
case inr.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 ^ 1
hre : (g • z).re = ↑b + z.re
hb : b = 1
⊢ z.re = -1 / 2
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 : ∑' (b : ℕ+) (c : ℕ+), ↑↑b ^ k * r ^ (↑c * ↑b) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e
⊢ ∑' (n : ℕ+) (n_1 : ℕ+), ↑↑n ^ k * (r ^ ↑n) ^ ↑n_1 = ∑' (b : ℕ+) (c : ℕ+), ↑↑b ^ k * r ^ (↑c * ↑b)

Tactic:
exact tsum_congr₂ <| fun b c ↦ by simp [mul_comm c.val b.val, pow_mul]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty ⇑f) 0
hper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑Γ.strictWidthInfty
⊢ Tendsto (⇑f) atImInfty (𝓝 (valueAtInfty ⇑f))

Tactic:
← cuspFunction_apply_zero hh hanal hper

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : DiscreteTopology ↥Γ
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : Fact (IsCusp ∞ Γ)
inst✝ : ModularFormClass F Γ k
f : F
h : valueAtInfty ⇑f = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty ⇑f) 0
hper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑Γ.strictWidthInfty
⊢ Tendsto (⇑f) atImInfty (𝓝 (cuspFunction Γ.strictWidthInfty (⇑f) 0))
Module: Mathlib.NumberTheory.Modular

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

Tactic:
have := hg.2

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this : |(T ^ ↑g 0 0 • S • z).re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
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:
by
  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.ModularForms.DedekindEta

Goal state before:
pp: q : ℂ
hq : ‖q‖ < 1
⊢ Summable fun i ↦ ‖-q ^ (i + 1)‖

Tactic:
simpa using (summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one (norm_nonneg _) hq)

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

Goal state before:
pp: z : ℍ
a b : ℤ
this : Summable fun x ↦ (↑b - ↑a) * ((↑↑x * ↑z + ↑a) * (↑↑x * ↑z + ↑b))⁻¹
⊢ Summable fun x ↦ 1 / (↑↑x * ↑z + ↑a) - 1 / (↑↑x * ↑z + ↑b)

Tactic:
apply this.congr (fun m ↦ ?_)

Goal state after:
z : ℍ
a b : ℤ
this : Summable fun x ↦ (↑b - ↑a) * ((↑↑x * ↑z + ↑a) * (↑↑x * ↑z + ↑b))⁻¹
m : { x // x ∉ {0} }
⊢ (↑b - ↑a) * ((↑↑m * ↑z + ↑a) * (↑↑m * ↑z + ↑b))⁻¹ = 1 / (↑↑m * ↑z + ↑a) - 1 / (↑↑m * ↑z + ↑b)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inl
k : ℤ
hk_neg : k < 0
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
levelOne_neg_weight_rank_zero hk_neg

Goal state after:
case inl
k : ℤ
hk_neg : k < 0
⊢ 0 < Cardinal.aleph0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ g ≠ S ∧ g ≠ -S

Tactic:
have : S • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow]

Goal state after:
g : SL(2, ℤ)
hg : g • ρ = ρ
this : S • ρ ≠ ρ
⊢ g ≠ S ∧ g ≠ -S
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ IsClosed {z | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
refine .inter ?_ (.inter ?_ ?_)

Goal state after:
case refine_1
⊢ IsClosed fun z ↦ Real.le✝ 0 z.im

case refine_2
⊢ IsClosed fun z ↦ Real.le✝ 1 ‖z‖

case refine_3
⊢ IsClosed fun z ↦ Real.le✝ |z.re| (1 / 2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.re ^ 2 ≤ (1 / 2) ^ 2

Tactic:
sq_le_sq,

Goal state after:
case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ |z.re| ≤ |1 / 2|
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
⊢ (Subtype.val '' S).Finite

Tactic:
have : Fintype (G ⧸ H.subgroupOf G) := Subgroup.fintypeQuotientOfFiniteIndex

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
this : Fintype (↥G ⧸ H.subgroupOf G)
⊢ (Subtype.val '' S).Finite
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
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
x : ℕ
hx : x + 1 ∈ range p
⊢ a ^ (x + 1 - 1 + (p - 1 - (x + 1))) * ↑p * b * ↑(x + 1) = ↑p * b * a ^ (p - 2) * ↑(x + 1)

Tactic:
have : x.succ - 1 + (p - 1 - x.succ) = p - 2 := by
          rw [← Nat.add_sub_assoc (Nat.le_sub_one_of_lt (Finset.mem_range.mp hx))]
          exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)

Goal state after:
case succ
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
x : ℕ
hx : x + 1 ∈ range p
this : x.succ - 1 + (p - 1 - x.succ) = p - 2
⊢ a ^ (x + 1 - 1 + (p - 1 - (x + 1))) * ↑p * b * ↑(x + 1) = ↑p * b * a ^ (p - 2) * ↑(x + 1)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
⊢ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑n ^ s =
    ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s *
      (2 / s.Gammaℂ * ↑(h Γ) ^ (-s))

Tactic:
generalize (PowerSeries.coeff n) (qExpansion (h Γ) f) = p

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (2 / s.Gammaℂ * ↑(h Γ) ^ (-s))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n

Tactic:
by
  simp only [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]
  iterate 4 rw [padicValNat_eq_emultiplicity]
  · exact Nat.two_pow_sub_pow hxy hx hneven
  · exact hn
  · exact Nat.sub_ne_zero_of_lt hyx
  · lia
  · simp [← Nat.pos_iff_ne_zero, tsub_pos_iff_lt, Nat.pow_lt_pow_left hyx hn]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ζ ∈ MulAction.stabilizer (↥(torsion K)) a
⊢ ζ = 1

Tactic:
rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integerSetTorsionSMul_smul_coe,
    unitSMul_smul, ← mixedEmbedding_preimageOfMemIntegerSet, ← map_mul,
    (mixedEmbedding_injective K).eq_iff, ← map_mul, ← RingOfIntegers.ext_iff, mul_eq_right₀,
    Units.val_eq_one, OneMemClass.coe_eq_one] at hζ

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ * ↑(preimageOfMemIntegerSet a) = ↑(preimageOfMemIntegerSet a)
⊢ ↑(preimageOfMemIntegerSet a) ≠ 0
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
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
obtain h₂ | h₂ := (Nat.dvd_prime Nat.prime_two).mp <| index_unitsMulComplexConjInv_range_dvd K

Goal state after:
case inl
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 = 1 ∨ indexRealUnits K = 2

case inr
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 ∨ 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
⊢ indexRealUnits K = 2 ↔ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤

Tactic:
suffices (∃ u : (𝓞 K)ˣ, Subgroup.zpowers (unitsMulComplexConjInv K u) = ⊤) ↔
      (unitsMulComplexConjInv K).range.index = 1 by
    rw [this]
    have h_eq := indexRealUnits_mul_eq K
    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · rwa [h, Nat.mul_eq_left two_ne_zero] at h_eq
    · rwa [h, mul_one] at h_eq
  refine ⟨fun ⟨u, hu⟩ ↦ Subgroup.index_eq_one.mpr (top_le_iff.mp ?_), fun h ↦ ?_⟩
  · refine le_of_eq_of_le ?_ ((Subgroup.zpowers u).map_le_range (unitsMulComplexConjInv K))
    rw [MonoidHom.map_zpowers, ← hu]
  · obtain ⟨ζ, hζ⟩ := exists_zpow_surjective (torsion K)
    rw [Subgroup.index_eq_one, MonoidHom.range_eq_top] at h
    obtain ⟨u, rfl⟩ := h ζ
    exact ⟨u, (Subgroup.eq_top_iff' _).mpr hζ⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : ↑x✝¹ = ↑x✝
⊢ x✝¹ = x✝

Tactic:
Subtype.ext_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : ↑x✝¹ = ↑x✝
⊢ ↑x✝¹ = ↑x✝
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₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ regOfFamily (realFundSystem K) = |∏ w, 2| * regOfFamily (fundSystem ↥K⁺)

Tactic:
regOfFamily_eq_det _ W₀ g.symm,

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 ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ |(Matrix.of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(realFundSystem K (g.symm i))))).det| =
    |∏ w, 2| * regOfFamily (fundSystem ↥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
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
i w : { w // w ≠ w₀ }
⊢ ↑((equivInfinitePlace K).symm ↑w).mult *
      Real.log (((equivInfinitePlace K).symm ↑w) ((algebraMap (𝓞 K) K) ↑(realFundSystem K (g.symm (f.symm i))))) =
    2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i w

Tactic:
show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl,

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 ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
i w : { w // w ≠ w₀ }
⊢ ↑((equivInfinitePlace K).symm ↑w).mult *
      Real.log
        (((equivInfinitePlace K).symm ↑w)
          ((algebraMap (↥K⁺) K) ↑↑(fundSystem (↥K⁺) ((finCongr ⋯) (g.symm (f.symm i)))))) =
    2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : x ∈ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
⊢ ∑ w, x w = 0

Tactic:
induction hx using Submodule.span_induction with
  | mem _ h =>
      obtain ⟨w, rfl⟩ := h
      simp_rw [completeFamily, dif_neg w.prop, sum_expMap_symm_apply (coe_ne_zero _),
        Units.norm, Rat.cast_one, Real.log_one]
  | zero => simp
  | add _ _ _ _ hx hy => simp [sum_add_distrib, hx, hy]
  | smul _ _ _ hx => simp [← mul_sum, hx]

Goal state after:
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 θ
⊢ span {↑p} ≠ ⊥

Tactic:
by simp [NeZero.ne p]

Goal state after:
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
⊢ span {↑p} ≠ ⊥

Tactic:
by simp [NeZero.ne p]

Goal state after:
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} ≠ ⊥

Tactic:
by simp [NeZero.ne p]

Goal state after:
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
⊢ (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩)).ramificationIdx ℤ =
    multiplicity Q (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
by
  obtain ⟨S, rfl⟩ := (map_surjective _ (ZMod.ringHom_surjective (Int.castRingHom (ZMod p)))) Q
  rw [ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply]

Goal state after:
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))
⊢ map (algebraMap ℤ (𝓞 K)) 𝒑 = span {hζ.toInteger - 1} ^ Module.finrank ℚ K

Tactic:
have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
  have : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K)) := by
    refine IsGalois.of_equiv_equiv (f := (FractionRing.algEquiv ℤ ℚ).toRingEquiv.symm)
      (g := (FractionRing.algEquiv (𝓞 K) K).toRingEquiv.symm) <|
        RingHom.ext fun x ↦ IsFractionRing.algEquiv_commutes (FractionRing.algEquiv ℤ ℚ).symm
          (FractionRing.algEquiv (𝓞 K) K).symm _
  rw [map_span, Set.image_singleton, span_singleton_eq_span_singleton.mpr
    ((associated_norm_zeta_sub_one p k hζ).symm.map (algebraMap ℤ (𝓞 K))),
    ← Algebra.intNorm_eq_norm, Algebra.algebraMap_intNorm_of_isGalois, ← prod_span_singleton]
  conv_lhs =>
    enter [2, σ]
    rw [span_singleton_eq_span_singleton.mpr
      (hζ.toInteger_isPrimitiveRoot.associated_sub_one_map_sub_one σ).symm]
  rw [Finset.prod_const, Finset.card_univ, ← Fintype.card_congr (galRestrict ℤ ℚ K (𝓞 K)).toEquiv,
    ← Nat.card_eq_fintype_card, IsGalois.card_aut_eq_finrank]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
⊢ (Real.exp (y w₀) • ↑expMapBasis fun i ↦ if i = w₀ then 0 else y i) = ↑expMapBasis y

Tactic:
rw [expMapBasis_apply'' y]

Goal state after: