mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
⊢ (Support R k).Finite

Tactic:
obtain ⟨⟨n, ⟨d, hd⟩⟩, hk⟩ := IsLocalization.surj (nonZeroDivisors R) k
  have hd' : d ≠ 0 := nonZeroDivisors.ne_zero hd
  suffices {v : HeightOneSpectrum R | v.valuation K (algebraMap R K d) < 1}.Finite by
    apply Set.Finite.subset this
    intro v hv
    apply_fun v.valuation K at hk
    simp only [Valuation.map_mul, valuation_of_algebraMap] at hk
    rw [Set.mem_ofPred_eq, valuation_of_algebraMap]
    have := intValuation_le_one v n
    contrapose! this
    rw [← hk, mul_comm]
    exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <|
      mul_le_mul_of_nonneg_right this (by simp)
  simp_rw [valuation_lt_one_iff_dvd]
  apply Ideal.finite_factors
  simpa only [Submodule.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot]

Goal state after:
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)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)

Tactic:
by
  refine ⟨fun H S hS ↦ H.comp ((continuous_inclusion hS).prodMap continuous_id),
    fun H ↦ ?_⟩
  simp_rw [continuous_iff_continuousAt, ContinuousAt]
  rintro ⟨x, y⟩
  set S : Set ι := {i | x i ∈ A i}
  have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr x.2
  have hxS : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi
  rcases exists_inclusion_eq_of_eventually R A hS hxS with ⟨x', hxx'⟩
  rw [← hxx', nhds_prod_eq, nhds_eq_map_inclusion hAopen hS x',
    ← Filter.map_id (f := 𝓝 y), prod_map_map_eq, ← nhds_prod_eq, tendsto_map'_iff]
  exact H S hS |>.tendsto ⟨x', y⟩

Goal state after:
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)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0

Tactic:
← this,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) x)) ∂volume =
    ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x)

Tactic:
polarSpaceCoord_symm_apply,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f
          (fun w ↦ ((homeoRealMixedSpacePolarSpace K) x).1 ↑w,
            Pi.map (fun i ↦ ↑Complex.polarCoord.symm) fun w ↦
              (((homeoRealMixedSpacePolarSpace K) x).1 ↑w, ((homeoRealMixedSpacePolarSpace K) x).2 w)) ∂volume =
    ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) a)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x)

Tactic:
polarSpaceCoord_symm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f
          (fun w ↦ ((homeoRealMixedSpacePolarSpace K) a).1 ↑w,
            Pi.map (fun i ↦ ↑Complex.polarCoord.symm) fun w ↦
              (((homeoRealMixedSpacePolarSpace K) a).1 ↑w, ((homeoRealMixedSpacePolarSpace K) a).2 w)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
⊢ logMap x = logMap y

Tactic:
by
  ext
  simp_rw [logMap_apply, h, norm_eq_of_normAtPlace_eq h]

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨(logEmbedding K) (Additive.ofMul u), ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
AddSubmonoid.mk_vadd,

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) +ᵥ logMap x ∈ ZSpan.fundamentalDomain B
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨0, ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
AddSubmonoid.mk_vadd,

Goal state after:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ 0 +ᵥ logMap x ∈ ZSpan.fundamentalDomain B
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨0, ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
    exact hx.1

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h : Function.Surjective ⇑(unitsMulComplexConjInv K)
u : (𝓞 K)ˣ
hζ : Function.Surjective fun x ↦ (unitsMulComplexConjInv K) u ^ x
⊢ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤

Tactic:
exact ⟨u, (Subgroup.eq_top_iff' _).mpr hζ⟩

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

Tactic:
rw [Matrix.submatrix_apply, Matrix.of_apply, Matrix.of_apply,
    show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,
    show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl, equivInfinitePlace_symm_apply]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
i w : { w // w ≠ w₀ }
⊢ ↑((equivInfinitePlace K).symm ↑w).mult * Real.log (↑w ↑↑(fundSystem (↥K⁺) ((finCongr ⋯) (g.symm (f.symm i))))) =
    2 * Matrix.of (fun i ↦ (logEmbedding ↥K⁺) (Additive.ofMul (fundSystem (↥K⁺) ((equivFinRank ↥K⁺).symm i)))) i w
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ ¬p ∣ absNorm (under ℤ (conductor ℤ θ))

pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsCoatom (span {↑p})

Tactic:
exponent

Goal state after:
K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ absNorm (under ℤ (conductor ℤ θ)) ↔ ¬p ∣ absNorm (under ℤ (conductor ℤ θ))

K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsCoatom (span {↑p})
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
smul_eq_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (fun i ↦
      Real.exp (x w₀) *
        (∏ x_1,
            normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_1)))) ^
              x ↑x_1)
          i) =
    fun i ↦ Real.exp (x w₀) * ∏ i_1, i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i_1))) ^ x ↑i_1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMapBasis x = Real.exp (x w₀) • ↑expMapBasis fun i ↦ if i = w₀ then 0 else x i

Tactic:
by
  rw [expMapBasis_apply', expMapBasis_apply', if_pos rfl, smul_smul, ← Real.exp_add, add_zero]
  conv_rhs =>
    enter [2, w, 2, i]
    rw [if_neg i.prop]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x_1, (Real.exp (x w₀) • ∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
smul_eq_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x_1, (Real.exp (x w₀) * ∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ AddSubgroup.map (logEmbedding K)
      (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)) ⊔ Subgroup.toAddSubgroup (torsion K)) ≤
    AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)))

Tactic:
← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ AddSubgroup.map (logEmbedding K)
      (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)) ⊔ Subgroup.toAddSubgroup (torsion K)) ≤
    AddSubgroup.map (logEmbedding K)
      (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)) ⊔ Subgroup.toAddSubgroup (torsion K))
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₀
⊢ (∑ x_1, if x_1 = ⟨w, hw⟩ then x ↑x_1 • 1 else x ↑x_1 • 0) ∈ Set.Ico 0 1 ↔ x w ∈ Set.Ico 0 1

Tactic:
smul_eq_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1, if x_1 = ⟨w, hw⟩ then x ↑x_1 * 1 else x ↑x_1 * 0) ∈ Set.Ico 0 1 ↔ x w ∈ Set.Ico 0 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
⊢ Multiset.count P (normalizedFactors (cyclotomic n K)) ≤ 1

Tactic:
by_contra! H

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
⊢ False
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:
IsPrimitiveRoot.autToPow_spec

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) ^ 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
this : IsGalois ℚ K
⊢ ↑((galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P)) = ↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn))

Tactic:
refine Set.eq_of_subset_of_card_le ?_ ?_

Goal state after:
case refine_1
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
⊢ ↑((galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P)) ⊆ ↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn))

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
⊢ Fintype.card ↑↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) ≤
    Fintype.card ↑↑((galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P))
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝⁷ : IsDomain 𝒪
this✝⁶ : IsDedekindDomain 𝒪
this✝⁵ : IsFractionRing 𝒪 K
this✝⁴ : Module.Finite ℤ 𝒪
this✝³ : CharZero 𝒪
this✝² : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this✝¹ : IsGaloisGroup Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w✝ : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Ideal.under ℤ P = Ideal.span {p}
hp0 : p ≠ 0
this✝ : Prime p
Q : Ideal 𝒪
x✝ : Q.IsPrime
hQ : ↑p ∈ Q
this : Ideal.span {p} = Ideal.under ℤ Q
⊢ ¬(Ideal.under ℤ Q).ramificationIdxIn 𝒪 = 1

Tactic:
← this,

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝⁷ : IsDomain 𝒪
this✝⁶ : IsDedekindDomain 𝒪
this✝⁵ : IsFractionRing 𝒪 K
this✝⁴ : Module.Finite ℤ 𝒪
this✝³ : CharZero 𝒪
this✝² : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this✝¹ : IsGaloisGroup Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w✝ : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Ideal.under ℤ P = Ideal.span {p}
hp0 : p ≠ 0
this✝ : Prime p
Q : Ideal 𝒪
x✝ : Q.IsPrime
hQ : ↑p ∈ Q
this : Ideal.span {p} = Ideal.under ℤ Q
⊢ ¬(Ideal.span {p}).ramificationIdxIn 𝒪 = 1
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 ℚ) α‖ = ‖∏ τ, τ α‖

pp: case calc_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖σ' α * ∏ τ ∈ univ.erase σ', τ α‖ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖

Tactic:
· rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]

Goal state after:
case calc_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖σ' α * ∏ τ ∈ univ.erase σ', τ α‖ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
⊢ ‖(Algebra.norm ℚ) α‖ ≤ ‖σ α‖ * house α ^ (finrank ℚ K - 1)

Tactic:
by
  classical
  set σ' := σ.toRatAlgHom
  calc _ = ‖∏ τ : K →ₐ[ℚ] ℂ, τ α‖ := ?_
       _ = ‖(σ' α) * ∏ τ ∈ univ.erase σ', τ α‖ := by rw [mul_prod_erase univ (· α) (mem_univ σ')]
       _ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖ := ?_
       _ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', house α := by gcongr; apply norm_embedding_le_house
       _ = ‖σ' α‖ * house α ^ (Module.finrank ℚ K - 1) := by simp
  · rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]
  · rw [Complex.norm_mul]
    gcongr
    exact norm_prod_le (univ.erase σ') (· α)

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ↑(#S) = ∏ i, (P i - N i + 1)

Tactic:
rw [Pi.card_Icc N P, Nat.cast_prod]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ∏ i, ↑(#(Icc (∑ j, ↑B * -(A i j)⁻) (∑ j, ↑B * (A i j)⁺))) = ∏ i, (P i - N i + 1)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion

Goal state before:
pp: G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
this : ⇑toCompl ⁻¹' C ∈ 𝓝 0
W : OpenAddSubgroup G
hCW : ↑W ⊆ ⇑toCompl ⁻¹' C
V : Set (Completion G) := ↑(map toCompl ↑W).topologicalClosure
⊢ ∃ V, ↑V ⊆ U

Tactic:
have : IsOpen V := by
      /- Since `V` is a subgroup of `Completion G`, it suffices to show that it is a neighborhood of
      `0` in `Completion G`. This follows from the fact that `toCompl : G → Completion G` is dense
      inducing and `W` is a neighborhood of `0` in `G`. -/
      apply isOpen_of_mem_nhds (g := 0)
      apply (isDenseInducing_toCompl _).closure_image_mem_nhds
      exact mem_nhds_zero W

Goal state after:
G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
this✝ : ⇑toCompl ⁻¹' C ∈ 𝓝 0
W : OpenAddSubgroup G
hCW : ↑W ⊆ ⇑toCompl ⁻¹' C
V : Set (Completion G) := ↑(map toCompl ↑W).topologicalClosure
this : IsOpen V
⊢ ∃ V, ↑V ⊆ U
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun i ↦ f i.1 * g i.2) (a * b)

Tactic:
← hasSum_iff_hasSum_compl

Goal state after:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum (⇑UniformSpace.Completion.toCompl ∘ f) ↑a
hg : HasSum (⇑UniformSpace.Completion.toCompl ∘ g) ↑b
⊢ HasSum (⇑UniformSpace.Completion.toCompl ∘ fun i ↦ f i.1 * g i.2) ↑(a * b)
Module: Mathlib.NumberTheory.Ostrowski

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

Tactic:
by
  obtain ⟨p, ⟨hp0, hp1⟩, hmin⟩ := exists_minimal_nat_zero_lt_and_lt_one hf_nontriv bdd
  have hp := is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin
  have : Fact p.Prime := ⟨hp⟩
  obtain ⟨t, ht, hpt⟩ := exists_pos_eq_pow_neg hp0 hp1 hmin
  simp_rw [← exists_nat_rpow_iff_isEquiv]
  refine ⟨p, ⟨inferInstance, t⁻¹, inv_pos.mpr ht, fun n ↦ ?_⟩, fun q ⟨hq, heq⟩ ↦ ?_⟩
  · rcases eq_or_ne n 0 with rfl | hn
    · simp [ht.ne']
    · rcases Nat.exists_eq_pow_mul_and_not_dvd hn p hp.ne_one with ⟨_, m, hpm, rfl⟩
      have := (padicNorm.nat_eq_one_iff m).mpr hpm
      simp_all [← rpow_natCast, ← rpow_mul, mul_comm t, mul_inv_cancel_right₀ ht.ne',
        eq_one_of_not_dvd bdd hp0 hp1 hmin hpm]
  · by_contra! hpq
    apply hq.elim.ne_one
    rw [ne_comm, ← Nat.coprime_primes hp hq.elim, hp.coprime_iff_not_dvd] at hpq
    rcases heq with ⟨_, _, heq⟩
    simpa [eq_one_of_not_dvd bdd hp0 hp1 hmin hpq] using heq q

Goal state after: