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

Goal state before:
pp: γ : SL(2, ℤ)
⊢ G2 ∣[2] γ = G2 - D2 γ

Tactic:
have : γ ∈ Subgroup.closure {S, T} := by simp [SpecialLinearGroup.SL2Z_generators]
  induction this using Subgroup.closure_induction with
  | one => simp only [SlashAction.slash_one, D2_one, sub_zero]
  | mem g hg =>
      simp only [mem_insert_iff, mem_singleton_iff] at hg
      rcases hg with (h1 | h2)
      · 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
      · simpa only [h2, D2_T, sub_zero] using G2_T_transform
  | mul g h _ _ ig ih =>
      rw [D2_mul, SlashAction.slash_mul, ig, sub_eq_add_neg, SlashAction.add_slash, ih]
      grind [SlashAction.neg_slash, SL_slash]
  | inv g _ ig =>
      have H1 : (G2 ∣[(2 : ℤ)] g) ∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g) ∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
      simp_rw [← SlashAction.slash_mul, sub_eq_add_neg, SlashAction.add_slash, mul_inv_cancel,
        SlashAction.slash_one, SL_slash, SlashAction.neg_slash] at H1
      nth_rw 2 [H1]
      have := D2_inv g
      simp only [SL_slash] at this
      rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
z : ℍ
hLHS :
  (serreDerivative (↑k) F ∣[k + 2] γ) z =
    (D F ∣[k + 2] γ) z - ↑k * 12⁻¹ * ((EisensteinSeries.E2 ∣[2] γ) z * (F ∣[k] γ) z)
⊢ (serreDerivative (↑k) F ∣[k + 2] γ) z = serreDerivative (↑k) (F ∣[k] γ) z

Tactic:
have hDz : (D (F ∣[k] γ)) z = (D F ∣[k + 2] γ) z -
      (k * (2 * π * I)⁻¹ * (γ 1 0 / denom γ z) * (F ∣[k] γ) z) := by
    simp [normalizedDerivOfComplex_SL_slash hF]

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
z : ℍ
hLHS :
  (serreDerivative (↑k) F ∣[k + 2] γ) z =
    (D F ∣[k + 2] γ) z - ↑k * 12⁻¹ * ((EisensteinSeries.E2 ∣[2] γ) z * (F ∣[k] γ) z)
hDz :
  D (F ∣[k] γ) z =
    (D F ∣[k + 2] γ) z -
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑γ 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] γ) z
⊢ (serreDerivative (↑k) F ∣[k + 2] γ) z = serreDerivative (↑k) (F ∣[k] γ) z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ HasSum (fun x ↦ e2Summand x z)
    (2 * riemannZeta 2 - 8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n) (symmetricIco ℤ)

Tactic:
apply (hasSum_e2Summand_symmetricIcc z).hasSum_symmetricIco_of_hasSum_symmetricIcc

Goal state after:
z : ℍ
⊢ Tendsto (fun N ↦ -e2Summand (↑N) z) atTop (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z

Tactic:
← gammaSetDivGcdSigmaEquiv.symm.tsum_eq,

Goal state after:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (c : (r : ℕ) × ↑(gammaSet 1 r 0)), eisSummand (↑k) (gammaSetDivGcdSigmaEquiv.symm c) z =
    riemannZeta ↑k * eisensteinSeries 0 (↑k) z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' Set.Ici 1

Tactic:
intro ξ

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
ξ : ℍ
⊢ ξ ∈ 𝒟 → ξ ∈ (fun τ ↦ ‖↑τ‖) ⁻¹' Set.Ici 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 𝒟 ⊆ UpperHalfPlane.re ⁻¹' Set.Icc (-(1 / 2)) (1 / 2)

Tactic:
intro ξ

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
ξ : ℍ
⊢ ξ ∈ 𝒟 → ξ ∈ UpperHalfPlane.re ⁻¹' Set.Icc (-(1 / 2)) (1 / 2)
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
i : ι
⊢ IsCompact (if i ∈ S then A i else K i)

Tactic:
by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
⊢ HasFDerivAt (↑(polarCoordReal K).symm) (FDerivPolarCoordRealSymm K x) x

Tactic:
classical
  exact (hasFDerivAt_id x.1).prodMap x (hasFDerivAt_pi_polarCoord_symm x.2)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ |(of (Subtype.val ∘ ⇑((Basis.restrictScalars ℤ (basisOfIsMaxRank hu)).reindex (equivFinRank K)))).det| =
    |(of fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))).det|

Tactic:
Basis.coe_reindex

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ |(of (Subtype.val ∘ ⇑(Basis.restrictScalars ℤ (basisOfIsMaxRank hu)) ∘ ⇑(equivFinRank K).symm)).det| =
    |(of fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))).det|
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
this : IsUnit y
⊢ (algebraMap (𝓞 ↥K⁺) K) ↑this.unit = (algebraMap (𝓞 K) K) ↑u

Tactic:
simp [hy]

Goal state after:
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
⊢ (unitsMulComplexConjInv K).ker = realUnits K

Tactic:
ext
  rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
⊢ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
have hζ' := isOfFinOrder_iff_pow_eq_one.mpr
      ⟨n, pos_of_ne_zero (fun h0 ↦ by simp [h0, hp.out.ne_one] at hn),
      hζ.pow_eq_one⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = orderOf (unitOfCoprime (p ^ f) ⋯)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
this : (φ ^ orderOf φ) (root P) = root P
⊢ ↑(unitOfCoprime (p ^ f) ⋯ ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P))) = ↑1

Tactic:
simp only [AlgEquiv.coe_pow, φ, coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, hK] at this

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
this : root P ^ (p ^ f) ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = root P
⊢ ↑(unitOfCoprime (p ^ f) ⋯ ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P))) = ↑1
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))
h : (span {hζ.toInteger - 1}).IsPrime
hp0 : 𝒑 ≠ ⊥
⊢ multiplicity (span {hζ.toInteger - 1}) (span {hζ.toInteger - 1} ^ Module.finrank ℚ K) = Module.finrank ℚ K

pp: case hp
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
hp0 : 𝒑 ≠ ⊥
⊢ map (algebraMap ℤ (𝓞 K)) 𝒑 ≠ ⊥

Tactic:
multiplicity_pow_self (span_zeta_sub_one_ne_bot p k hζ) (isUnit_iff.not.mpr h.ne_top)

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
hp0 : 𝒑 ≠ ⊥
⊢ Module.finrank ℚ K = Module.finrank ℚ K

case hp
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
hp0 : 𝒑 ≠ ⊥
⊢ map (algebraMap ℤ (𝓞 K)) 𝒑 ≠ ⊥
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ : ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∈ monicFactorsMod ζ p
h₃ : P.inertiaDeg ℤ = (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).natDegree
⊢ P.inertiaDeg ℤ = orderOf ↑p

Tactic:
Multiset.mem_toFinset,

Goal state after:
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : p.Coprime m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∈
    UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
h₃ : P.inertiaDeg ℤ = (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).natDegree
⊢ P.inertiaDeg ℤ = orderOf ↑p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ : ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∈ monicFactorsMod ζ p
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ P.ramificationIdx ℤ = 1

Tactic:
Multiset.mem_toFinset,

Goal state after:
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∈
    UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ P.ramificationIdx ℤ = 1
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Finset K
⊢ house (∏ x ∈ s, x) ≤ ∏ x ∈ s, house x

Tactic:
simpa [house, map_prod] using Finset.norm_prod_le _ _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ house (α + β) ≤ house α + house β

Tactic:
by
  simp only [house, map_add]; apply norm_add_le

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ 0 ≤ P i + 1

Tactic:
apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))
    intro j _
    positivity

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ CompactSpace ℤ_[p]

Tactic:
rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ TotallyBounded Set.univ ∧ IsComplete Set.univ
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hpq : q ≠ p
⊢ False

Tactic:
apply hq.elim.ne_one

Goal state after:
case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hpq : q ≠ p
⊢ q = 1
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case hbc
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := ⋯
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
r : K →+* ℂ
a✝ : r ∈ univ
⊢ house ((algebraMap (𝓞 K) K) ((newBasis K) r)) ≤ univ.sup' ⋯ fun r ↦ house ((algebraMap (𝓞 K) K) ((newBasis K) r))

Tactic:
simp only [le_sup'_iff, mem_univ, true_and]

Goal state after:
case hbc
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
r : K →+* ℂ
a✝ : r ∈ univ
⊢ ∃ b, house ((algebraMap (𝓞 K) K) ((newBasis K) r)) ≤ house ((algebraMap (𝓞 K) K) ((newBasis K) b))
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
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑κ
hκ' : κ 1 = 1 + r
⊢ κ 1 = (addChar_of_value_at_one r hr) 1

Tactic:
simp [hκ']

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (fun x ↦ ‖x‖) = Valued.v.norm

Tactic:
by
  apply UniformSpace.Completion.extension_unique (f := @norm (PadicAlgCl p) _) (g := Valued.v.norm)
  · exact uniformContinuous_norm
  · let S := (Valued.toNormedField ℂ_[p] NNReal).toNormedCommRing.toNormedRing.toSeminormedRing
    let := S.toNonUnitalSeminormedRing.toSeminormedAddCommGroup.toSeminormedAddGroup
    exact @uniformContinuous_norm ℂ_[p] this
  · intro x
    simp only [Valued.v.norm_def, RankOne.hom_eq_embedding]
    rw [embedding_restrict (PadicComplex.valued p).v x, valuation_extends,
      ← PadicAlgCl.valuation_coe]

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

Goal state before:
pp: case 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
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ 1 ≤ ↑(padicValNat p ((p ^ t).choose (i + 1)))

Tactic:
Nat.one_le_cast

Goal state after:
case 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
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ 1 ≤ padicValNat p ((p ^ t).choose (i + 1))
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
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
⊢ (mahlerSeries a) ↑m = ∑ i ∈ range (n + 1), m.choose i • a i

Tactic:
have h_van (i) : m.choose (i + (n + 1)) = 0 := Nat.choose_eq_zero_of_lt (by lia)
  have aux : Summable fun i ↦ m.choose (i + (n + 1)) • a (i + (n + 1)) := by
    simpa only [h_van, zero_smul] using summable_zero
  simp only [mahlerSeries_apply ha, mahler_natCast_eq, Nat.cast_smul_eq_nsmul, add_zero,
    ← aux.sum_add_tsum_nat_add' (f := fun i ↦ m.choose i • a i), h_van, zero_smul, tsum_zero]

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 - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 ≤ ↑q.den

Tactic:
Nat.one_le_cast

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

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ (a * a₁⁻¹).y

Tactic:
simpa only [y_inv, mul_neg, y_mul, le_neg_add_iff_add_le, add_zero] using!
    h.x_mul_y_le_y_mul_x hax hay

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ b⁻¹ = a₁ ^ (-↑n)

Tactic:
by simp [hn]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ -b = -a₁ ^ ↑n

Tactic:
by simp [hn]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ -b⁻¹ = -a₁ ^ (-↑n)

Tactic:
by simp [hn]

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
⊢ 1 ≤ v ↑a

Tactic:
have hda : a.degree < πᵥ.degree := by
    have hbpos := degree_pos_of_ne_zero_of_nonunit hab.2.2 hb
    simp_rw [hπᵥ, degree_mul, degree_eq_natDegree hab.2.1, degree_eq_natDegree hab.2.2] at hbpos ⊢
    norm_cast
    simpa using hbpos

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hda : a.degree < πᵥ.degree
⊢ 1 ≤ v ↑a
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ siftedSum ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d

Tactic:
rw [siftedSum_eq_sum_support_mul_ite]

Goal state after:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0) ≤
    ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
rcases hp.1.eq_two_or_odd' with (rfl | hodd)

Goal state after:
case inl
hp : Fact (Nat.Prime 2)
⊢ ∃ a b k, 0 < k ∧ k < 2 ∧ a ^ 2 + b ^ 2 + 1 = k * 2

case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
hy : y ≠ 0
⊢ (norm x).natAbs ≤ (norm x * norm y).natAbs

Tactic:
Int.natAbs_mul

Goal state after:
x y : ℤ[i]
hy : y ≠ 0
⊢ (norm x).natAbs ≤ (norm x).natAbs * (norm y).natAbs
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
⊢ (norm (↑p * x)).natAbs = { re := ↑k, im := -1 }.norm.natAbs

Tactic:
rw [hx]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
⊢ (norm (↑p * x)).natAbs = { re := ↑k, im := 1 }.norm.natAbs

Tactic:
rw [hx]

Goal state after: