mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (1 / (2 * ↑π) ^ (-s) / Gamma s * ↑(h Γ) ^ (-s))

Tactic:
one_div,

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 s * ↑(h Γ) ^ (-s))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: case refine_2
ι : 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
U : Set ((i : ι) → R i) := Sᶜ.pi K
U_nhds : U ∈ 𝓝 ⇑x
QU : DFunLike.coe ⁻¹' U ⊆ DFunLike.coe ⁻¹' Q
⊢ DFunLike.coe ⁻¹' U ∈ 𝓝 x

Tactic:
· simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (s ⊔ torsion K) * (s ⊔ torsion K).index ≠ 0

Tactic:
refine Nat.mul_ne_zero ?_ (Subgroup.finiteIndex_iff.mp h)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (s ⊔ torsion K) ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

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

Tactic:
Subtype.forall,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ (∀ (a : InfinitePlace K) (b : a.IsComplex), (x✝.1 a, x✝.2 ⟨a, b⟩) ∈ Complex.polarCoord.target) ↔
    (∀ (i : InfinitePlace K), i.IsComplex → x✝.1 i ∈ Set.Ioi 0) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex), x✝.2 ⟨a, b⟩ ∈ Set.Ioo (-π) π
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
w : InfinitePlace K
x : K
⊢ w ((complexConj K) x) = w x

Tactic:
← norm_embedding_eq,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
⊢ ‖w.embedding ((complexConj K) x)‖ = w x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ ↑a ≠ 0

Tactic:
by_contra!

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
this : ↑a = 0
⊢ False
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 : ℝ
x✝² x✝¹ : ↥(torsion K)
x✝ : ↑(integerSet K)
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
Subtype.mk_eq_mk

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
x✝² x✝¹ : ↥(torsion K)
x✝ : ↑(integerSet K)
⊢ ↑((x✝² * x✝¹) • 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
x✝ y✝ : (𝓞 K)ˣ
⊢ ⟨x✝ * y✝ * ((unitsComplexConj K) (x✝ * y✝))⁻¹, ⋯⟩ =
    ⟨x✝ * ((unitsComplexConj K) x✝)⁻¹ * (y✝ * ((unitsComplexConj K) y✝)⁻¹), ⋯⟩

Tactic:
Subtype.mk_eq_mk

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ y✝ : (𝓞 K)ˣ
⊢ x✝ * y✝ * ((unitsComplexConj K) (x✝ * y✝))⁻¹ = x✝ * ((unitsComplexConj K) x✝)⁻¹ * (y✝ * ((unitsComplexConj K) y✝)⁻¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑(((((integerSetEquiv K).subtypeEquiv ⋯).trans
                  { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, (↑x).2), invFun := fun x ↦ ⟨(↑x.1, x.2), ⋯⟩, left_inv := ⋯,
                    right_inv := ⋯ }).trans
              {
                toFun := fun ab ↦
                  ((Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n) ab.1, ab.2),
                invFun := fun ab ↦
                  ((Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n).symm ab.1,
                    ab.2),
                left_inv := ⋯, right_inv := ⋯ })
            a).1 =
    Ideal.span {↑(preimageOfMemIntegerSet ↑a)}

Tactic:
Equiv.trans_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑({
              toFun := fun ab ↦
                ((Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n) ab.1, ab.2),
              invFun := fun ab ↦
                ((Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n).symm ab.1,
                  ab.2),
              left_inv := ⋯, right_inv := ⋯ }
            ({ toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, (↑x).2), invFun := fun x ↦ ⟨(↑x.1, x.2), ⋯⟩, left_inv := ⋯,
                right_inv := ⋯ }
              (((integerSetEquiv K).subtypeEquiv ⋯) a))).1 =
    Ideal.span {↑(preimageOfMemIntegerSet ↑a)}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMap (x w₀ • (completeBasis K) w₀ + ∑ i, x ↑i • (completeBasis K) ↑i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
expMap_add,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMap (x w₀ • (completeBasis K) w₀) * ↑expMap (∑ i, x ↑i • (completeBasis K) ↑i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i
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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ Irreducible P

Tactic:
classical
  have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
  obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
  refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)
  rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]
  exact dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ

Goal state after:
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) = 1 - 1
⊢ ∑ i ∈ range n, ζ ^ i = 0

Tactic:
sub_self

Goal state after:
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
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
h✝ : ¬w = w₀
⊢ IsCompact (Set.Icc 0 1)

Tactic:
exact isCompact_Icc

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

Goal state before:
pp: case calc_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖↑((Algebra.norm ℚ) α)‖ = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) α)‖

Tactic:
Real.norm_eq_abs,

Goal state after:
case calc_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ |↑((Algebra.norm ℚ) α)| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) α)‖
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : v ∈ T
⊢ A *ᵥ v ∈ S

Tactic:
rw [mem_Icc] at hv ⊢
  have mulVec_def : A.mulVec v =
      fun i ↦ Finset.sum univ fun j : β ↦ A i j * v j := rfl
  rw [mulVec_def]
  refine ⟨fun i ↦ ?_, fun i ↦ ?_⟩
  all_goals
    simp only [mul_neg]
    gcongr ∑ _ : β, ?_ with j _ -- Get rid of sums
    rw [← mul_comm (v j)] -- Move A i j to the right of the products
    -- We have to distinguish cases: we have now 4 goals
    rcases le_total 0 (A i j) with hsign | hsign
  · rw [negPart_eq_zero.2 hsign]
    exact mul_nonneg (hv.1 j) hsign
  · rw [negPart_eq_neg.2 hsign]
    simp only [mul_neg, neg_neg]
    exact mul_le_mul_of_nonpos_right (hv.2 j) hsign
  · rw [posPart_eq_self.2 hsign]
    gcongr
    apply hv.2
  · rw [posPart_eq_zero.2 hsign]
    exact mul_nonpos_of_nonneg_of_nonpos (hv.1 j) hsign

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

Goal state before:
pp: case convert_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ MeasurableSet {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ 1}

pp: case convert_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ MeasureTheory.volume
      (frontier {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ 1}) =
    0

Tactic:
· exact (toMixed K).continuous.measurable (measurableSet_normLeOne K)

Goal state after:
case convert_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ MeasureTheory.volume
      (frontier {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ 1}) =
    0
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ ↑n ^ t ≤ ↑n ^ s

Tactic:
← hfn

Goal state after:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ f ↑n ≤ ↑n ^ s
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)
a b : ℤ_[p]
⊢ (mahlerSeries fun x ↦ r ^ x) (a + b) = (mahlerSeries fun x ↦ r ^ x) a * (mahlerSeries fun x ↦ r ^ x) b

Tactic:
let F : C(ℤ_[p], R) := mahlerSeries (r ^ ·)
    change F (a + b) = F a * F b
    -- It is fiddly to show directly that `F (a + b) = F a * F b` for general `a, b`,
    -- so we prove it for `a, b ∈ ℕ` directly, and then deduce it for all `a, b` by continuity.
    have hF (n : ℕ) : F n = (r + 1) ^ n := by
      rw [mahlerSeries_apply_nat hr le_rfl, (Commute.one_right _).add_pow]
      refine Finset.sum_congr rfl fun i hi ↦ ?_
      rw [one_pow, mul_one, nsmul_eq_mul, Nat.cast_comm]
    refine congr_fun ((denseRange_natCast.prodMap denseRange_natCast).equalizer
      ((map_continuous F).comp continuous_add)
      (continuous_mul.comp (map_continuous <| F.prodMap F)) (funext fun ⟨m, n⟩ ↦ ?_)) (a, b)
    simp [← Nat.cast_add, hF, ContinuousMap.prodMap_apply, pow_add]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case pos
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

pp: case neg
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
· exact .inr <| equiv_padic_of_bounded hf_nontriv bdd

Goal state after:
case neg
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ = ↑(1 / ↑p)

Tactic:
one_div,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ = ↑(↑p)⁻¹
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Valued.v ↑p = 1 / ↑p

Tactic:
by
  rw [← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]), ← coe_eq, valuation_extends,
    PadicAlgCl.valuation_p]

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
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 ∈ range (p ^ t - 1)
⊢ 0 ≤ ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊

Tactic:
by simp only [zero_le]

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: k : ℕ
hk0 : k ≠ 0
n p : ℕ
hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
⊢ ∃ b, n ≤ b ∧ Prime b ∧ b ≡ 1 [MOD k]

Tactic:
exact ⟨p, ⟨hp.2.1.le, hp.1, hp.2.2⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : d = 0 ∨ a.y ^ 2 = 0
⊢ a = 1

Tactic:
or_iff_right h₀,

Goal state after:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : a.y ^ 2 = 0
⊢ a = 1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Tactic:
obtain ⟨q₁, h₁ : q₁.num ^ 2 - d * (q₁.den : ℤ) ^ 2 = m,
      q₂, h₂ : q₂.num ^ 2 - d * (q₂.den : ℤ) ^ 2 = m, hne, hqf⟩ :=
    hm.exists_ne_map_eq_of_mapsTo (mapsTo_univ f _) finite_univ

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
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
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤

Tactic:
obtain ⟨n, a, ha⟩ := @Module.Finite.exists_fin R (S ⧸ M) _ _ _ _

Goal state after:
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) = ⊤
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
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) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), a'' i ∈ p
hx : (a''.sum fun i c ↦ c • a i) = x
⊢ ∑ i, (fun i ↦ a'' i) i • a i = x

Tactic:
rw [← hx, Finsupp.sum_fintype]

Goal state after:
case h
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) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), a'' i ∈ p
hx : (a''.sum fun i c ↦ c • a i) = x
⊢ ∀ (i : Fin n), 0 • a i = 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : (a ^ m).y < (a ^ n).y
⊢ m < n

Tactic:
contrapose! H

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : n ≤ m
⊢ (a ^ n).y ≤ (a ^ m).y
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²¹ : Field K
inst✝²⁰ : Field L
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.LiesOver p
inst✝¹⁴ : FiniteDimensional K L
inst✝¹³ : MulSemiringAction Gal(L/K) B
inst✝¹² : IsGaloisGroup Gal(L/K) A B
inst✝¹¹ : IsDedekindDomain A
inst✝¹⁰ : IsDedekindDomain B
inst✝⁹ : Module.Finite A B
inst✝⁸ : Module.IsTorsionFree A B
inst✝⁷ : Ring.HasFiniteQuotients A
inst✝⁶ : P.IsMaximal
D : Type u_5
inst✝⁵ : Field D
inst✝⁴ : Algebra D L
inst✝³ : IsDecompositionField K L P D
inst✝² : IsGalois K L
inst✝¹ : Algebra K D
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
⊢ Module.finrank K D = (p.primesOver B).ncard

Tactic:
by
  have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
  have : FiniteDimensional D L := FiniteDimensional.right K D L
  refine mul_left_injective₀ (b := Module.finrank D L) Module.finrank_pos.ne' ?_
  dsimp only
  rw [Module.finrank_mul_finrank, rank_left A K L P D hp,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn p B Gal(L/K),
    IsGaloisGroup.card_eq_finrank Gal(L/K) K L]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case h.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 < a.y
⊢ ∃ n, a = a₁ ^ n

Tactic:
have hx₁ : 1 < a.x := by nlinarith [a.prop, h.d_pos]
    have hxx₁ := h.mul_inv_x_pos hx₁ hy
    have hxx₂ := h.mul_inv_x_lt_x hx₁ hy
    have hyy := h.mul_inv_y_nonneg hx₁ hy
    lift (a * a₁⁻¹).x to ℕ using hxx₁.le with x' hx'
    obtain ⟨n, hn⟩ := ih x' (mod_cast hxx₂.trans_eq hax'.symm) hyy hx' hxx₁
    exact ⟨n + 1, by rw [pow_succ', ← hn, mul_comm a, ← mul_assoc, mul_inv_cancel, one_mul]⟩

Goal state after:
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
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ‖(Polynomial.aeval z) F‖ ^ 2 / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 ≤
    (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) ^ 2 /
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

Tactic:
gcongr
      exact hz.2

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr.inr.inr
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⁻¹
⊢ ∃ n, -b⁻¹ = a₁ ^ n ∨ -b⁻¹ = -a₁ ^ n

Tactic:
exact ⟨-n, Or.inr (by simp [hn])⟩

Goal state after: