mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem.inl
γ g : SL(2, ℤ)
h1 : g = S
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
ext z
        simp only [Pi.sub_apply, h1, D2_S z, SlashInvariantForm.slash_S_apply G2 2 z, mul_comm,
          G2_S_transform z, modular_S_smul]
        ring_nf
        aesop

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

Goal state before:
pp: case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this✝ :
  iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
h :
  -(2 * ↑π * I * (2 * ↑π * I) ^ k) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n =
    -(2 * ↑π * I) * ∑' (n : ℕ), (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
this : ∀ (x : ℂ), cexp (2 * ↑π * I * ↑n * x / 1) = cexp (2 * ↑π * I * x / 1) ^ n
⊢ iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z = (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
div_one

Goal state after:
case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this✝ :
  iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
h :
  -(2 * ↑π * I * (2 * ↑π * I) ^ k) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n =
    -(2 * ↑π * I) * ∑' (n : ℕ), (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
this : ∀ (x : ℂ), cexp (2 * ↑π * I * ↑n * x) = cexp (2 * ↑π * I * x) ^ n
⊢ iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z = (2 * ↑π * I * ↑n) ^ k * cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this : T • z ≠ z
⊢ T⁻¹ • z ≠ z

Tactic:
ne_eq,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this : T • z ≠ z
⊢ ¬T⁻¹ • z = z
Module: Mathlib.NumberTheory.Modular

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

Tactic:
ne_eq,

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

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

Tactic:
ne_eq,

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

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

Tactic:
ne_eq,

Goal state after:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
⊢ ¬T⁻¹ • ρ = ρ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ

Tactic:
suffices (ModularGroup.T ^ 2 • τ :) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add]
  have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := rfl
  simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd]
  norm_cast

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) * (1 / (-I * ↑τ) ^ (1 / 2)) * jacobiTheta₂ 0 (-1 / ↑τ)

Tactic:
mul_one_div,

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
i j : Fin 2
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S))) i j =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      i j

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
case «0».«0»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
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})) (∑ x ∈ range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, ↑p * b * a ^ (p - 2) * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))

Tactic:
rw [Finset.sum_congr rfl]

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
⊢ ∀ x ∈ range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x = ↑p * b * a ^ (p - 2) * ↑x
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
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i

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
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬p ∣ k

Tactic:
rintro ⟨c, rfl⟩

Goal state after:
case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
c : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * (p * c)
⊢ False
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

Tactic:
obtain hyx | hyx := le_total y x
  · iterate 2 rw [← Int.natCast_emultiplicity]
    rw [Int.ofNat_sub (Nat.pow_le_pow_left hyx n)]
    rw [← Int.natCast_dvd_natCast] at hxy hx
    rw [Int.natCast_sub hyx] at *
    push_cast at *
    exact Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n
  · simp only [Nat.sub_eq_zero_iff_le.mpr (Nat.pow_le_pow_left hyx n), emultiplicity_zero,
    Nat.sub_eq_zero_iff_le.mpr hyx, top_add]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ logMap (c • x) ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
logMap_real_smul hx.2 hc

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ logMap x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
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 : ℝ
a : ↑(integerSet K)
⊢ ⋯.choose ≠ 0

Tactic:
ne_eq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a : ↑(integerSet K)
⊢ ¬⋯.choose = 0
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
⊢ u ∈ realUnits K ↔ ∃ v, (algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v = ↑u

Tactic:
simp [realUnits, MonoidHom.mem_range, RingHom.toMonoidHom_eq_coe, Units.ext_iff]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
⊢ volume A =
    2 ^ nrRealPlaces K * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
have hA₁ (x : mixedSpace K) : x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A := by
    rw [← hA]
    simp_rw [Set.mem_preimage, Set.mem_image, normAtAllPlaces_norm_at_real_places]
  have hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A := by
    refine subset_antisymm (fun x ⟨a, ha₁, ha₂⟩ ↦ ⟨?_, fun w ↦ ?_⟩) (Set.subset_preimage_image _ _)
    · rw [← hA, Set.mem_preimage, ← normAtAllPlaces_eq_of_normAtComplexPlaces_eq ha₂]
      exact Set.mem_image_of_mem normAtAllPlaces (Set.inter_subset_left ha₁)
    · have := funext_iff.mp ha₂ w
      rw [normAtComplexPlaces_apply_isReal, normAtComplexPlaces_apply_isReal] at this
      rw [← this]
      exact ha₁.2 w
  rw [volume_eq_two_pow_mul_volume_plusPart hA₁ hm, volume_eq_two_pi_pow_mul_integral hA₃
    (measurableSet_plusPart hm), ← mul_assoc]
  refine congr_arg (_ * _ * ·) <| setLIntegral_congr ?_
  rw [← volume_eq_two_pow_mul_two_pi_pow_mul_integral_aux hA]
  refine inter_ae_eq_left_of_ae_eq_univ <| ae_eq_univ.mpr
    <| Set.compl_iInter _ ▸ measure_iUnion_null_iff.mpr fun w ↦ ?_
  rw [show {x : realSpace K | x w.1 ≠ 0}ᶜ = {x | x w.1 = 0} by ext; simp]
  exact realSpace.volume_eq_zero w.1

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

Goal state before:
pp: case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
x✝ : (𝓞 K)ˣ
⊢ x✝ ∈ Set.range (realFundSystem K) ↔ x✝ ∈ ⇑(Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) '' Set.range (fundSystem ↥K⁺)

Tactic:
simp [realFundSystem, Equiv.exists_congr_left (finCongr (units_rank_eq_units_rank K).symm)]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
hS : ∃ n ∈ S, 2 < n
inst✝ : IsCyclotomicExtension S ℚ K
⊢ IsCMField K

Tactic:
have : Algebra.IsIntegral ℚ K := integral S ℚ K

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
hS : ∃ n ∈ S, 2 < n
inst✝ : IsCyclotomicExtension S ℚ K
this : Algebra.IsIntegral ℚ K
⊢ IsCMField K
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
⊢ ∀ (b : InfinitePlace K),
    f.symm b ≠ f.symm w' →
      (if h : b = w' then ∑ x, ↑x.mult else ∑ x, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨b, ⋯⟩))))) = 0

Tactic:
ne_eq,

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
⊢ ∀ (b : InfinitePlace K),
    ¬f.symm b = f.symm w' →
      (if h : b = w' then ∑ x, ↑x.mult else ∑ x, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨b, ⋯⟩))))) = 0
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
      · exact hw ▸ h₂
      · exact h₁ w hw

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this : ζ ^ (↑((galEquivZMod m F) (σ.restrictNormal F))).val = ζ ^ (↑((galEquivZMod n K) σ)).val
⊢ (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)

Tactic:
by
    rw [(hζ.isOfFinOrder (NeZero.ne _)).pow_inj_mod, ← hζ.eq_orderOf,
      ← ZMod.natCast_eq_natCast_iff', ZMod.natCast_val, ZMod.natCast_val, ZMod.cast_id] at this
    rwa [Units.ext_iff]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) (eval 1 (cyclotomic p (𝓞 K)))

Tactic:
cyclotomic_eq_prod_X_sub_primitiveRoots hζ.toInteger_isPrimitiveRoot,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) (eval 1 (∏ μ ∈ primitiveRoots p (𝓞 K), (X - C μ)))
Module: Mathlib.RingTheory.Unramified.Dedekind

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Module.Finite A B
inst✝² : IsDedekindDomain A
inst✝¹ : IsDomain B
inst✝ : Algebra.FormallyUnramified A B
⊢ ∀ (P : Ideal B), P ≠ ⊥ → ∀ (x : P.IsPrime), IsDiscreteValuationRing (Localization.AtPrime P)

Tactic:
by
    intro q hq hqp
    let q' := IsLocalRing.maximalIdeal (Localization.AtPrime q)
    suffices q'.IsPrincipal from ((IsDiscreteValuationRing.TFAE (Localization.AtPrime q)
      (IsLocalization.AtPrime.not_isField B hq (Localization.AtPrime q))).out 4 0).mp this
    let p := q.under A
    let := Localization.AtPrime.algebraOfLiesOver p q
    have : p.IsMaximal := (hqp.under A).isMaximal (q.under_ne_bot A hq)
    let : Field (A ⧸ p) := Ideal.Quotient.field p
    have := IsArtinianRing.of_finite (A ⧸ p) (B ⧸ p.map (algebraMap A B))
    suffices q' = (p.map (algebraMap A B)).map (algebraMap B (Localization.AtPrime q)) by
      rw [this, Ideal.map_map, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq A (Localization.AtPrime p) (Localization.AtPrime q),
        ← Ideal.map_map]
      infer_instance
    rw [← (Algebra.FormallyUnramified.isRadical_map_isMaximal A B p).radical,
      IsLocalization.map_radical q.primeCompl,
      IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes (Localization.AtPrime q) q,
      Localization.AtPrime.map_eq_maximalIdeal]
    rw [Ideal.minimalPrimes_eq_comap]
    exact ⟨q.map (Ideal.Quotient.mk (p.map (algebraMap A B))),
      IsArtinianRing.mem_minimalPrimes bot_le, Ideal.comap_map_mk Ideal.map_comap_le⟩

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)

Tactic:
have hp : (1 : ℝ) < p :=
    mod_cast (is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin).one_lt

Goal state after:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp : 1 < ↑p
⊢ ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)
Module: Mathlib.NumberTheory.Padics.AddChar

Goal state before:
pp: p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : NormedRing R
inst✝² : Algebra ℤ_[p] R
inst✝¹ : IsBoundedSMul ℤ_[p] R
inst✝ : IsUltrametricDist R
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑κ
⊢ Tendsto (fun n ↦ (κ 1 - 1) ^ n) atTop (𝓝 0)

Tactic:
refine (PadicInt.fwdDiff_tendsto_zero ⟨κ, hκ⟩).congr fun n ↦ ?_
  simpa only [AddChar.map_zero_eq_one, mul_one] using! fwdDiff_addChar_eq κ 0 1 n

Goal state after:
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
⊢ HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) f

Tactic:
have : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] f 0) n)
      (mahlerSeries (Δ_[1]^[·] f 0) : C(ℤ_[p], E)) :=
    hasSum_mahlerSeries (fwdDiff_tendsto_zero f)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x ↦ Δ_[1]^[x] (⇑f) 0)
⊢ HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) f
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
g : X → Fin n
hg : ∀ (x : X), (fun i ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun i ↦ x ∈ E i) y → y = g x
i : Fin n
⊢ ∃ x, x ∈ E i

Tactic:
simpa [← SetLike.coe_set_eq, ← nonempty_iff_ne_empty] using! hEne i

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |d * ↑q.den ^ 2 - q.num ^ 2| < M

Tactic:
← @Int.cast_lt ℝ,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ ↑|d * ↑q.den ^ 2 - q.num ^ 2| < ↑M
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ v ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    v X ^ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).intDegree

Tactic:
intDegree_div (by grind only) (by grind only),

Goal state after:
case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ v ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    v X ^ (((algebraMap K[X] K⟮X⟯) p).intDegree - ((algebraMap K[X] K⟮X⟯) q).intDegree)
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j + 1 - 1 < ↑m * s ∧ ↑m * s ≤ ↑j + 1
⊢ False

Tactic:
add_sub_cancel_right,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j < ↑m * s ∧ ↑m * s ≤ ↑j + 1
⊢ False
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case refine_1
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : v ↑πᵥ < 1 ∧ πᵥ ≠ 0
⊢ ¬IsUnit πᵥ

Tactic:
simp only [Polynomial.isUnit_iff, isUnit_iff_ne_zero]
    intro ⟨a, ha0, ha⟩
    rw [← ha, coePolynomial, algebraMap_C, ← algebraMap_eq_C] at hπᵥ
    grind

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∈ {x | ∃ k, beattySeq r k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

Tactic:
by_cases h₂ : j ∈ {beattySeq' s k | k}

Goal state after:
case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∈ {x | ∃ k, beattySeq r k = x}
h₂ : j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∈ {x | ∃ k, beattySeq r k = x}
h₂ : j ∉ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}