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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) = 1

Tactic:
← Nat.cast_one

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)) = 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ^ (1 + 1) ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)

Tactic:
rw [one_add_one_eq_two, eq_add_of_sub_eq' hk]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ^ 2 ∣ ∑ i ∈ range p, (y + ↑p * k) ^ i * y ^ (p - ↑1 - i)
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst✝⁵ : (i : ι₁) → SetLike (S₁ i) (R₁ i)
inst✝⁴ : (j : ι₂) → SetLike (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
inst✝³ : (i : ι₁) → Monoid (R₁ i)
inst✝² : (i : ι₂) → Monoid (R₂ i)
inst✝¹ : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)
inst✝ : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)
φ : (j : ι₂) → R₁ (f j) →* R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)
⊢ mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ 1 = 1

Tactic:
ext i

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst✝⁵ : (i : ι₁) → SetLike (S₁ i) (R₁ i)
inst✝⁴ : (j : ι₂) → SetLike (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
inst✝³ : (i : ι₁) → Monoid (R₁ i)
inst✝² : (i : ι₂) → Monoid (R₂ i)
inst✝¹ : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)
inst✝ : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)
φ : (j : ι₂) → R₁ (f j) →* R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)
i : ι₂
⊢ (mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ 1) i = 1 i
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst✝⁵ : (i : ι₁) → SetLike (S₁ i) (R₁ i)
inst✝⁴ : (j : ι₂) → SetLike (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
inst✝³ : (i : ι₁) → Monoid (R₁ i)
inst✝² : (i : ι₂) → Monoid (R₂ i)
inst✝¹ : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)
inst✝ : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)
φ : (j : ι₂) → R₁ (f j) →* R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)
x y : Πʳ (i : ι₁), [R₁ i, ↑(B₁ i)]_[𝓕₁]
⊢ mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ (x * y) =
    mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ x * mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ y

Tactic:
ext i

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst✝⁵ : (i : ι₁) → SetLike (S₁ i) (R₁ i)
inst✝⁴ : (j : ι₂) → SetLike (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
inst✝³ : (i : ι₁) → Monoid (R₁ i)
inst✝² : (i : ι₂) → Monoid (R₂ i)
inst✝¹ : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)
inst✝ : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)
φ : (j : ι₂) → R₁ (f j) →* R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)
x y : Πʳ (i : ι₁), [R₁ i, ↑(B₁ i)]_[𝓕₁]
i : ι₂
⊢ (mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ (x * y)) i =
    (mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ x * mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ y) i
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ n ≠ 0

pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x + (y + 1) ≠ 0

pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x ^ n + (y + 1) ^ n ≠ 0

Tactic:
· exact (Odd.pos hn).ne'

Goal state after:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x + (y + 1) ≠ 0

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x ^ n + (y + 1) ^ n ≠ 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 : realMixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target, (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) =
    ∫ (x : realMixedSpace K) in Set.univ, f x

Tactic:
← setIntegral_congr_set (polarCoordReal_symm_target_ae_eq_univ K),

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : realMixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target, (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) =
    ∫ (x : realMixedSpace K) in ↑(polarCoordReal K).symm '' (polarCoordReal K).target, f x
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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
h₂ : DiscreteTopology ↥(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))))
⊢ IsMaxRank u ↔
    finrank ℤ ↥(span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))) =
      finrank ℤ ↥(unitLattice K)

Tactic:
unitLattice_rank,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
h₂ : DiscreteTopology ↥(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))))
⊢ IsMaxRank u ↔
    finrank ℤ ↥(span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))) = rank K
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 ⇑(homeoRealMixedSpacePolarSpace K) ⁻¹' (polarSpaceCoord K).target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) a)) ∂volume =
    ∫⁻ (x : mixedSpace K), f x

Tactic:
← mixedEmbedding.lintegral_comp_polarCoord_symm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in ⇑(homeoRealMixedSpacePolarSpace K) ⁻¹' (polarSpaceCoord K).target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) a)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x)
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)ˣ
hu : IsMaxRank u
⊢ regOfFamily u = ZLattice.covolume (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))) volume

Tactic:
by
  rw [regOfFamily, dif_pos hu]

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✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
⊢ (complexConj K) ↑x = ↑x ↔ ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x

Tactic:
by
  rw [complexConj_eq_self_iff]
  refine ⟨fun h ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
  · have : IsIntegral ℤ (⟨x, h⟩ : K⁺) :=
      (isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective K⁺ K)).mp x.isIntegral_coe
    refine ⟨⟨⟨x, h⟩, this⟩, ?_⟩
    rw [IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺, RingOfIntegers.map_mk]
    rfl
  · rw [← hy, IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺]
    exact SetLike.coe_mem _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ |(↑(completeBasis K).equivFunL.symm).det| = ↑(finrank ℚ K) * regulator K

Tactic:
rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
    regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ |((LinearMap.toMatrix (completeBasis K) (completeBasis K)) ↑↑(completeBasis K).equivFunL.symm).transpose.det| =
    |(Matrix.of fun i w ↦
          if h : i = w₀ then ↑w.mult
          else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨i, h⟩))))).det|
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ emultiplicity (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩))
      (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p})) =
    emultiplicity ((mapEquiv (Int.quotientSpanNatEquivZMod p).symm) (Polynomial.map (Int.castRingHom (ZMod p)) Q))
      ((mapEquiv (Int.quotientSpanNatEquivZMod p).symm) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))

Tactic:
emultiplicity_factors_map_eq_emultiplicity inferInstance (by simp [NeZero.ne p])
      (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ emultiplicity
      (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk ⋯ ⋯ ⋯ ⋯)
          ⟨↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩), ?m.141⟩))
      (Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ)) =
    emultiplicity ((mapEquiv (Int.quotientSpanNatEquivZMod p).symm) (Polynomial.map (Int.castRingHom (ZMod p)) Q))
      ((mapEquiv (Int.quotientSpanNatEquivZMod p).symm) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))

K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) ∈
    normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
h : 2 < p
⊢ 2 ∉ span {hζ.toInteger - 1}

Tactic:
by
  rw [mem_span_singleton]
  rw [← pow_one p] at hK hζ
  exact hζ.toInteger_sub_one_not_dvd_two h.ne'

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
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:
apply SetLike.ext'

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
this : IsGalois ℚ K
⊢ ↑((galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P)) = ↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn))
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
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥((OrderIso.dualDual (Subgroup (DirichletCharacter R n))).symm
          ((subgroupGalEquivSubgroupChar n K R).dual (IsGalois.intermediateFieldEquivSubgroup F))) =
    Module.finrank ℚ ↥F

Tactic:
OrderIso.dualDual_symm_apply,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥(OrderDual.ofDual
          (OrderDual.ofDual ((subgroupGalEquivSubgroupChar n K R).dual (IsGalois.intermediateFieldEquivSubgroup F)))) =
    Module.finrank ℚ ↥F
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
i : ℕ
⊢ house (α ^ i) ≤ house α ^ i

Tactic:
simpa only [house, map_pow] using norm_pow_le ((canonicalEmbedding K) α) i

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ (fun i ↦ ↑(#(Icc (∑ j, ↑B * -(A i j)⁻) (∑ j, ↑B * (A i j)⁺)))) = fun i ↦ P i - N i + 1

Tactic:
ext i

Goal state after:
case e_f
α : 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)⁺))) = P i - N i + 1
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]
  congr
  ext i
  rw [Int.card_Icc_of_le (N i) (P i) (N_le_P_add_one A i)]
  exact add_sub_right_comm (P i) 1 (N i)

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

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

Tactic:
suffices LocallyCompactSpace ℚ_[p] from .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace _

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ LocallyCompactSpace ℚ_[p]
Module: Mathlib.NumberTheory.Padics.ProperSpace

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

Tactic:
suffices LocallyCompactSpace ℚ_[p] from .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace _
  have : closedBall 0 1 ∈ 𝓝 (0 : ℚ_[p]) := closedBall_mem_nhds _ zero_lt_one
  simp only [closedBall, dist_eq_norm_sub, sub_zero] at this
  refine IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup ?_ this
  simpa only [isCompact_iff_compactSpace] using! PadicInt.compactSpace p

Goal state after:
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 ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Tactic:
intro U

Goal state after:
G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
⊢ U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
⊢ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
intro U

Goal state after:
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
⊢ U ∈ 𝓝 1 → ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ ∀ (i : α × (K →+* ℂ)) (j : β × (K →+* ℂ)), ‖asiegel K a i j‖ ≤ c₂ K * A

pp: case hr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ 0 ≤ c₂ K * A

Tactic:
· intro kr lu
    calc
      ‖asiegel K a kr lu‖ = |asiegel K a kr lu| := ?_
      _ ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * ((newBasis K) lu.2))) := ?_
      _ ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) *
        house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) := ?_
      _ ≤ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) := ?_
      _ ≤ c K * A * supOfBasis K := ?_
      _ ≤ c₂ K * A := ?_
    · simp only [Int.cast_abs, ← Real.norm_eq_abs (asiegel K a kr lu)]; rfl
    · have remark := basis_repr_norm_le_const_mul_house K
      simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
        integralBasis_repr_apply, eq_intCast, Rat.cast_intCast,
          Complex.norm_intCast] at remark
      exact mod_cast remark ((a kr.1 lu.1 * ((newBasis K) lu.2))) kr.2
    · simp only [house, map_mul, mul_assoc]
      gcongr
      apply norm_mul_le
    · rw [mul_assoc, mul_assoc]
      gcongr _ * (?_ * _)
      · apply house_nonneg
      · exact habs kr.1 lu.1
    · gcongr
      simp only [supOfBasis, le_sup'_iff, mem_univ]; use lu.2
    · rw [mul_right_comm, c₂]
      gcongr
      exacts [supOfBasis_nonneg _, le_max_right ..]

Goal state after:
case hr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ 0 ≤ c₂ K * A
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ (↑n₀ * (↑k * logb ↑n₀ ↑n + ↑k)) ^ (↑k)⁻¹ = (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹

Tactic:
rw [← mul_rpow (by positivity) (by positivity), mul_assoc, add_mul, one_mul,
        mul_comm _ (k : ℝ)]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ 1 < ↑n

Tactic:
by norm_cast; lia

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
n : ℕ
h : 1 < n
⊢ f ↑m = ↑m ^ s

Tactic:
rw [rpow_logb (by positivity) (by norm_cast; omega) (zero_lt_one.trans hfm1)]

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

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

Tactic:
NNReal.coe_inv,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ = (↑↑p)⁻¹
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
⊢ ∀ (o : Set C(X × Y, R)), IsOpen o → f ∈ o → ∃ x, x ∈ o ∩ Set.range ⇑tensorHom

Tactic:
intro U

Goal state after:
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
⊢ IsOpen U → f ∈ U → ∃ x, x ∈ U ∩ Set.range ⇑tensorHom
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inr.refine_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
⊢ p ≡ 1 [MOD k]

Tactic:
· have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=
      ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)
    have : NeZero (k : ZMod p) :=
      NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)
    have : k = orderOf (b : ZMod p) := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf
    rw [← this] at hdiv
    exact ((modEq_iff_dvd' hprime.1.pos).2 hdiv).symm

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : ℤ√d
⊢ a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d)

Tactic:
rw [← norm_eq_one_iff_mem_unitary, norm_def, sq, sq, ← mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
⊢ (a * b).x = a.x * b.x + d * (a.y * b.y)

Tactic:
rw [← mul_assoc]

Goal state after:
d : ℤ
a b : Solution₁ d
⊢ (a * b).x = a.x * b.x + d * a.y * b.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
x y : ℤ_[p]
⊢ ‖(Polynomial.aeval x) F - (Polynomial.aeval y) F‖ ≤ ‖x - y‖

Tactic:
let ⟨z, hz⟩ := (F.map (algebraMap R ℤ_[p])).evalSubFactor x y

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
x y z : ℤ_[p]
hz :
  Polynomial.eval x (Polynomial.map (algebraMap R ℤ_[p]) F) -
      Polynomial.eval y (Polynomial.map (algebraMap R ℤ_[p]) F) =
    z * (x - y)
⊢ ‖(Polynomial.aeval x) F - (Polynomial.aeval y) F‖ ≤ ‖x - y‖