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

Goal state before:
pp: n : ℕ+
k l : ℕ
h : (k, l) ∈ (↑n).divisorsAntidiagonal
⊢ (fun x ↦ ⟨⟨↑x.1 * ↑x.2, ⋯⟩, ⟨(↑x.1, ↑x.2), ⋯⟩⟩) ((fun x ↦ divisorsAntidiagonalFactors x.fst x.snd) ⟨n, ⟨(k, l), h⟩⟩) =
    ⟨n, ⟨(k, l), h⟩⟩

Tactic:
Nat.mem_divisorsAntidiagonal

Goal state after:
n : ℕ+
k l : ℕ
h✝ : (k, l) ∈ (↑n).divisorsAntidiagonal
h : (k, l).1 * (k, l).2 = ↑n ∧ ↑n ≠ 0
⊢ (fun x ↦ ⟨⟨↑x.1 * ↑x.2, ⋯⟩, ⟨(↑x.1, ↑x.2), ⋯⟩⟩)
      ((fun x ↦ divisorsAntidiagonalFactors x.fst x.snd) ⟨n, ⟨(k, l), h✝⟩⟩) =
    ⟨n, ⟨(k, l), h✝⟩⟩
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: s : Set (Finset ℤ)
⊢ (∃ a, ∀ (b : ℕ), a ≤ b → Icc (-↑b) ↑b ∈ s) ↔ ∃ a, ∀ (b : ℕ), a ≤ b → Ioo (-↑b) ↑b ∈ s

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩ <;>
  [convert! ha (b - 1) (by grind) using 1; convert! ha (b + 1) (by grind) using 1]

Goal state after:
s : Set (Finset ℤ)
x✝ : ∃ a, ∀ (b : ℕ), a ≤ b → Icc (-↑b) ↑b ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Icc (-↑b) ↑b ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ Ioo (-↑b) ↑b = Icc (-↑(b - 1)) ↑(b - 1)

s : Set (Finset ℤ)
x✝ : ∃ a, ∀ (b : ℕ), a ≤ b → Ioo (-↑b) ↑b ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Ioo (-↑b) ↑b ∈ s
b : ℕ
hb : a - 1 ≤ b
⊢ Icc (-↑b) ↑b = Ioo (-↑(b + 1)) ↑(b + 1)
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: case h
K : Set ℂ
⊢ K ⊆ Metric.ball 0 1 →
    IsCompact K → HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
hK

Goal state after:
case h
K : Set ℂ
hK : 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.Modular

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

Tactic:
rcases this with h | h

Goal state after:
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
h : ↑g 0 0 = 0
⊢ T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T

case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
h : ↑g 0 0 = 1
⊢ T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 • ρ
this✝ : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
this : ↑g 0 0 = 0 ∨ ↑g 0 0 = -1
⊢ T ^ ↑g 0 0 * S * T⁻¹ = S * T⁻¹ ∨ T ^ ↑g 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

Tactic:
rcases this with h | h

Goal state after:
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
h : ↑g 0 0 = 0
⊢ T ^ ↑g 0 0 * S * T⁻¹ = S * T⁻¹ ∨ T ^ ↑g 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
h : ↑g 0 0 = -1
⊢ T ^ ↑g 0 0 * S * T⁻¹ = S * T⁻¹ ∨ T ^ ↑g 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹
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 ℂ
⊢ K ⊆ ℍₒ →
    IsCompact K →
      ∃ u,
        Summable u ∧
          ∀ (n : ℕ), ∀ k_1 ∈ K, ‖(f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) k_1‖ ≤ u n

Tactic:
hK

Goal state after:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
⊢ IsCompact K →
    ∃ u,
      Summable u ∧
        ∀ (n : ℕ), ∀ k_1 ∈ K, ‖(f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) k_1‖ ≤ u n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
m : ℤ
⊢ Summable fun b ↦ 1 / (↑m * ↑z + ↑b) - 1 / (↑m * ↑z + ↑b + 1)

Tactic:
by
  have := summable_linear_right_add_one_mul_linear_right z m m
  rw [← Finset.summable_compl_iff (s := {0, -1})] at *
  apply this.congr (fun b ↦ ?_)
  simpa [add_assoc, mul_comm] using
    (one_div_linear_sub_one_div_linear_eq z b (b + 1) m (by grind)).symm

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

Goal state before:
pp: τ : ℂ
⊢ ∀ (b : ℤ), cexp (↑π * I * ↑b ^ 2 * τ) = jacobiTheta₂_term b 0 τ

Tactic:
simp [jacobiTheta₂_term]

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

Goal state before:
pp: z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hc_eq : c = 1728
⊢ 1728 * discriminant z = E₄ z ^ 3 - E₆ z ^ 2

Tactic:
rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
hGH : H ≤ G
K L : Set α
⊢ IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
hK

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
hGH : H ≤ G
K L : Set α
hK : IsCompact K
⊢ IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
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 α
⊢ IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
hK

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
⊢ IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ∃ c, ⇑f = Function.const ℍ c

Tactic:
let : ModularFormClass (ModularForm 𝒮ℒ (0 * Nat.card (𝒮ℒ ⧸ 𝒢.subgroupOf 𝒮ℒ))) 𝒮ℒ 0 := by
    rw [zero_mul]; infer_instance

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this : ModularFormClass
  (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range
    (0 *
      ↑(Nat.card
          (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))))
  (Matrix.SpecialLinearGroup.mapGL ℝ).range 0 :=
  Eq.mpr
    (id
      (congrArg
        (fun _a ↦
          ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range _a)
            (Matrix.SpecialLinearGroup.mapGL ℝ).range 0)
        (zero_mul
          ↑(Nat.card
              (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range)))))
    inferInstance
⊢ ∃ c, ⇑f = Function.const ℍ c
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case refine_2
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : CuspFormClass F Γ k
hk : 0 < k
hs : ↑k / 2 + 1 < s.re
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ (↑k / 2)

Tactic:
simpa using CuspFormClass.qExpansion_isBigO f

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hp
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 + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ Prime 2

Tactic:
exact Int.prime_two

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : realMixedSpace K
w : { w // w.IsComplex }
⊢ ((homeoRealMixedSpacePolarSpace K) x).1 ↑w = (x.2 w).1

Tactic:
by
  simp_rw [homeoRealMixedSpacePolarSpace_apply, dif_neg (not_isReal_iff_isComplex.mpr w.prop)]

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
⊢ logMap (ζ • x) = logMap x

Tactic:
ext
  simp_rw [logMap_apply, unitSMul_smul, map_mul, norm_eq_norm, Units.norm, Rat.cast_one, one_mul,
    normAtPlace_apply, (mem_torsion K).mp hζ, one_mul]

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : K
⊢ x ∈ K⁺ ↔ x ∈ ⊥

Tactic:
IntermediateField.mem_bot

Goal state after:
case e'_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : K
⊢ x ∈ K⁺ ↔ x ∈ Set.range ⇑(algebraMap (↥K⁺) 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
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
by
  have h₁ := indexRealUnits_mul_eq K
  obtain h₂ | h₂ := (Nat.dvd_prime Nat.prime_two).mp <| index_unitsMulComplexConjInv_range_dvd K
  · exact Or.inr <| by rwa [h₂, mul_one] at h₁
  · exact Or.inl <| by rwa [h₂, Nat.mul_eq_right two_ne_zero] at 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 : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ y, (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap ∘ ⇑(↑↑↑J).subtype) y = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x

Tactic:
coe_subtype,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ y, (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap ∘ Subtype.val) y = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
Finsupp.coe_smul,

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

Goal state before:
pp: n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
this : (∑ i ∈ range n, ζ ^ i) * (ζ - 1) = 0
⊢ ∑ i ∈ range n, ζ ^ i = 0

Tactic:
exact (mul_eq_zero.1 this).resolve_right fun h ↦ hζ1 (sub_eq_zero.1 h)

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
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
⊢ σ (zeta n ℚ K) ^ a = (zeta n ℚ K ^ (↑(↑(IsPrimitiveRoot.autToPow ℚ ⋯) σ)).val) ^ a

Tactic:
MonoidHom.toOneHom_coe,

Goal state after:
n : ℕ
inst✝² : NeZero n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
⊢ σ (zeta n ℚ K) ^ a = (zeta n ℚ K ^ (↑((IsPrimitiveRoot.autToPow ℚ ⋯) σ)).val) ^ a
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
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
⊢ (galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)

Tactic:
obtain ⟨i, hi⟩ := FiniteField.exists_forall_apply_eq_pow (ℤ ⧸ span {(p : ℤ)}) p (𝓞 K ⧸ P) τ

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ∀ (x : 𝓞 K ⧸ P), τ x = x ^ Nat.card (ℤ ⧸ span {↑p}) ^ i
⊢ (galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: case refine_2
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn✝ : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ orderOf (ZMod.unitOfCoprime p hn✝) ≤ Nat.card ↑↑(Subgroup.map (↑(galEquivZMod n K)) (stabilizer Gal(K/ℚ) P))

Tactic:
Subgroup.coe_map

Goal state after:
case refine_2
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn✝ : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ orderOf (ZMod.unitOfCoprime p hn✝) ≤ Nat.card ↑(⇑↑(galEquivZMod n K) '' ↑(stabilizer Gal(K/ℚ) P))
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ (∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n) ↔ f.IsEquiv g

Tactic:
rw [isEquiv_iff_exists_rpow_eq]
  refine ⟨fun ⟨c, hc, h⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, h⟩ ↦ ⟨c, hc, (congrFun h ·)⟩⟩
  ext1 x
  rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬real.IsEquiv (padic p)

Tactic:
rw [isEquiv_iff_exists_rpow_eq]
  rintro ⟨c, hc₀, hc⟩
  apply_fun (· 2) at hc
  simp only [real_eq_abs, abs_ofNat, cast_ofNat] at hc
  exact ((padic_le_one p 2).trans_lt <| one_lt_rpow one_lt_two hc₀).ne' hc

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ‖(algebraMap ℚ_[p] (PadicAlgCl p)) ↑p‖ = ↑(1 / ↑p)

Tactic:
norm_extends,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ‖↑p‖ = ↑(1 / ↑p)
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
j : ℕ
x✝ : j ∈ range (p ^ t - 1)
⊢ ‖Δ_[1]^[n + (j + 1) + k * p ^ t] (⇑f) 0‖₊ ≤ ‖f‖₊ / ↑p ^ k

Tactic:
exact_mod_cast IH (n + (j + 1)) (by lia)

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x✝ : HeightOneSpectrum.adicCompletion ℚ v
⊢ x✝ ∈ HeightOneSpectrum.adicCompletionIntegers ℚ v ↔
    (HeightOneSpectrum.adicCompletion.equiv ℚ v) x✝ ∈ Valued.v.valuationSubring

Tactic:
rw [HeightOneSpectrum.mem_adicCompletionIntegers]; rfl

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x✝ : HeightOneSpectrum.adicCompletion ℚ v
⊢ x✝ ∈ HeightOneSpectrum.adicCompletionIntegers ℚ v ↔
    (HeightOneSpectrum.adicCompletion.uniformEquiv ℚ v) x✝ ∈ Valued.v.valuationSubring

Tactic:
rw [HeightOneSpectrum.mem_adicCompletionIntegers]; rfl

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 0 < a.x ^ 2 - 1

Tactic:
sub_pos

Goal state after:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 1 < a.x ^ 2
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
⊢ p • ⊤ = Submodule.map M.mkQ (p • ⊤)

Tactic:
by
        rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : K
⊢ (valuation K v) x ^ v.asIdeal.ramificationIdx' w.asIdeal = (valuation L w) ((algebraMap K L) x)

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := A) x

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x y : A
hy : y ∈ nonZeroDivisors A
⊢ (valuation K v) ((algebraMap A K) x / (algebraMap A K) y) ^ v.asIdeal.ramificationIdx' w.asIdeal =
    (valuation L w) ((algebraMap K L) ((algebraMap A K) x / (algebraMap A K) y))
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖

Tactic:
rw [newton_seq_dist_to_a (k + 1) (succ_pos _)]

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ <
    ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ a * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2

Tactic:
rw [ha, hb]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ (x ^ 2 + y ^ 2) * (u ^ 2 + v ^ 2) = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (-1, -1)

Tactic:
rw [hx, hy]

Goal state after:
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (x * x, y * y)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ p * q % 4 ≠ 3

Tactic:
show 3 = 3 % 4 by simp,

Goal state after:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3 % 4
hq : q % 4 ≠ 3 % 4
⊢ p * q % 4 ≠ 3 % 4