mathlib-initiative/mathlib-tactics huggingface dataset:
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))) ≤
    AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)))

Tactic:
← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).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)))
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₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap (mixedSpaceOfRealSpace (Real.exp (x w₀) • ↑expMapBasis fun i ↦ if i = w₀ then 0 else x i))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
map_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap (Real.exp (x w₀) • mixedSpaceOfRealSpace (↑expMapBasis fun i ↦ if i = w₀ then 0 else x i))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
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,
          (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
            (x ↑x_1 • fun i ↦ (completeBasis K) ↑x_1 ↑i))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
map_smul,

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

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
P : (ZMod p)[X]
hpn : ¬p ∣ n
hP : P ∣ cyclotomic n (ZMod p)
hPdeg : P.natDegree = orderOf (unitOfCoprime p ⋯)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ 1) ⋯)

Tactic:
by simpa

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
⊢ Associated (ζ - 1) (σ ζ - 1)

Tactic:
← hζ.autToPow_spec R σ

Goal state after:
A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
⊢ Associated (ζ - 1) (ζ ^ (↑((autToPow R hζ) σ)).val - 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this✝ : Measurable ↑expMapBasis
x : realSpace K
this : 0 ≤ (∏ w, ↑expMapBasis x ↑w)⁻¹
⊢ ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * ENNReal.ofReal (∏ w, ↑expMapBasis x ↑w)⁻¹ *
            ENNReal.ofReal 2⁻¹ ^ nrComplexPlaces K *
          ENNReal.ofReal ↑(finrank ℚ K) *
        ENNReal.ofReal (regulator K) *
      f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      (ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
        f (↑expMapBasis x))

Tactic:
ofReal_inv_of_pos (Finset.prod_pos
    fun _ _ ↦ expMapBasis_pos _ _),

Goal state after:
case e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this✝ : Measurable ↑expMapBasis
x : realSpace K
this : 0 ≤ (∏ w, ↑expMapBasis x ↑w)⁻¹
⊢ ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (ENNReal.ofReal (∏ i, ↑expMapBasis x ↑i))⁻¹ *
            ENNReal.ofReal 2⁻¹ ^ nrComplexPlaces K *
          ENNReal.ofReal ↑(finrank ℚ K) *
        ENNReal.ofReal (regulator K) *
      f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      (ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
        f (↑expMapBasis x))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsCompact (compactSet K)

Tactic:
refine isCompact_Icc.smul_set <| (isCompact_univ_pi fun w ↦ ?_).image_of_continuousOn
    (continuous_expMapBasis K).continuousOn
  split_ifs
  · exact isCompact_singleton
  · exact isCompact_Icc

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

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this : IsAbelianGalois ℚ K
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
have : NeZero m := ⟨fun h ↦ by simp [h] at hm⟩

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝ : IsAbelianGalois ℚ K
this : NeZero m
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)
Module: Mathlib.RingTheory.Unramified.Dedekind

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Module.Finite A B
inst✝² : IsDedekindDomain A
inst✝¹ : IsDomain B
inst✝ : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this✝¹ : p.IsMaximal
this✝ : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing (B ⧸ Ideal.map (algebraMap A B) p)
⊢ q' = Ideal.map (algebraMap B (Localization.AtPrime q)) (Ideal.map (algebraMap A B) p)

Tactic:
rw [← (Algebra.FormallyUnramified.isRadical_map_isMaximal A B p).radical,
      IsLocalization.map_radical q.primeCompl,
      IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes (Localization.AtPrime q) q,
      Localization.AtPrime.map_eq_maximalIdeal]

Goal state after:
case hIq
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Module.Finite A B
inst✝² : IsDedekindDomain A
inst✝¹ : IsDomain B
inst✝ : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this✝¹ : p.IsMaximal
this✝ : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing (B ⧸ Ideal.map (algebraMap A B) p)
⊢ q ∈ (Ideal.map (algebraMap A B) p).minimalPrimes
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main :
  (𝒑.primesOver (𝓞 ↥Fₘ)).ncard * (𝒑.ramificationIdxIn (𝓞 ↥Fₘ) * 𝒑.inertiaDegIn (𝓞 ↥Fₘ)) *
      ((𝒑.primesOver (𝓞 ↥Fₚ)).ncard * (𝒑.ramificationIdxIn (𝓞 ↥Fₚ) * 𝒑.inertiaDegIn (𝓞 ↥Fₚ))) =
    Nat.card Gal(K/ℚ)
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1

Tactic:
← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 𝒑 (𝓞 K) Gal(K/ℚ),

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main :
  (𝒑.primesOver (𝓞 ↥Fₘ)).ncard * (𝒑.ramificationIdxIn (𝓞 ↥Fₘ) * 𝒑.inertiaDegIn (𝓞 ↥Fₘ)) *
      ((𝒑.primesOver (𝓞 ↥Fₚ)).ncard * (𝒑.ramificationIdxIn (𝓞 ↥Fₚ) * 𝒑.inertiaDegIn (𝓞 ↥Fₚ))) =
    (𝒑.primesOver (𝓞 K)).ncard * (𝒑.ramificationIdxIn (𝓞 K) * 𝒑.inertiaDegIn (𝓞 K))
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1
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:
set σ' := σ.toRatAlgHom

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖(Algebra.norm ℚ) α‖ ≤ ‖σ α‖ * house α ^ (finrank ℚ K - 1)
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤ c K * house ((algebraMap (𝓞 K) K) α)

Tactic:
let σ := canonicalEmbedding K
  calc
    _ ≤ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      rw [← inverse_basisMatrix_mulVec_eq_repr]
      exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le
    _ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      gcongr
      exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹
    _ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖
        * house (algebraMap (𝓞 K) K α) := by
      gcongr with j
      exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j
    _ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := by
      simp [Embeddings.card, mul_assoc]

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

Goal state before:
pp: case convert_1
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
x✝² : euclidean.mixedSpace K
x✝¹ : ℝ
x✝ : x✝² ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K
h : 0 < x✝¹
⊢ (toMixed K) (x✝¹ • x✝²) ∈ fundamentalCone K

Tactic:
map_smul,

Goal state after:
case convert_1
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
x✝² : euclidean.mixedSpace K
x✝¹ : ℝ
x✝ : x✝² ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K
h : 0 < x✝¹
⊢ x✝¹ • (toMixed K) x✝² ∈ fundamentalCone K
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case convert_2
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
x✝¹ : euclidean.mixedSpace K
x✝ : ℝ
h : 0 ≤ x✝
⊢ mixedEmbedding.norm ((toMixed K) (x✝ • x✝¹)) =
    x✝ ^ Module.finrank ℝ (euclidean.mixedSpace K) * mixedEmbedding.norm ((toMixed K) x✝¹)

Tactic:
map_smul,

Goal state after:
case convert_2
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
x✝¹ : euclidean.mixedSpace K
x✝ : ℝ
h : 0 ≤ x✝
⊢ mixedEmbedding.norm (x✝ • (toMixed K) x✝¹) =
    x✝ ^ Module.finrank ℝ (euclidean.mixedSpace K) * mixedEmbedding.norm ((toMixed K) x✝¹)
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * max 1 ‖A‖ * ↑B = ∑ x, max 1 ‖A‖ * ↑B
j : β
a✝ : j ∈ univ
⊢ |↑(A i j)| ≤ max 1 ‖A‖

Tactic:
exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
r : X → ι
hr : ∀ (a : X), a ∈ U (r a)
V : X → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ ↑(U (r x))
t : Finset X
ht : univ ⊆ ⋃ i ∈ t, V i
x : X
hx : x ∈ univ
m : X
hm : m ∈ t
hm' : x ∈ V m
⊢ x ∈ ↑((fun j ↦ { carrier := V ↑(t.equivFin.symm j), isClopen' := ⋯ }) (t.equivFin ⟨m, hm⟩))

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
j : Fin n
hj : x ∈ ↑(W j)
this : W j ≠ ⊥
⊢ x ∈ ↑((fun k ↦ W ↑(t.equivFin.symm k)) (t.equivFin ⟨j, ⋯⟩))

Tactic:
by simpa

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
x y z : ℤ_[p]
hz : (Polynomial.aeval x) F - (Polynomial.aeval y) F = z * (x - y)
⊢ ‖(Polynomial.aeval x) F - (Polynomial.aeval y) F‖ ≤ ‖x - y‖

Tactic:
calc
    ‖F.aeval x - F.aeval y‖ = ‖z‖ * ‖x - y‖ := by simp [hz]
    _ ≤ 1 * ‖x - y‖ := by gcongr; apply PadicInt.norm_le_one
    _ = ‖x - y‖ := by simp

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]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : (Polynomial.aeval a) (Polynomial.derivative F) + q * h = 0
this : (Polynomial.aeval a) (Polynomial.derivative F) = -q * h
⊢ 1 * ‖h‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
by simpa

Goal state after:
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
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this : p.IsMaximal
⊢ Module.finrank D E = p.inertiaDegIn B

Tactic:
have := Module.finrank_mul_finrank K D E

Goal state after:
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
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : Module.finrank K D * Module.finrank D E = Module.finrank K E
⊢ Module.finrank D E = p.inertiaDegIn B
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case h.inl.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
hax : 0 < ↑x
hay : 0 ≤ (-1).y
hax' : ↑x = (-1).x
hy : 0 = (-1).y
⊢ -1 = a₁ ^ 0

Tactic:
· simp at hax'

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

Goal state before:
pp: A : Type u_1
B : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : Module.IsTorsionFree A B
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : x ≠ 0
⊢ (algebraMap A B) x ≠ 0

Tactic:
by simpa

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j ≤ ↑k * r ∧ ↑k * r < ↑j + 1
m : ℤ
h₂ : beattySeq' s m = j
⊢ False

Tactic:
← div_le_iff₀ hrs.pos,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k * r < ↑j + 1
m : ℤ
h₂ : beattySeq' s m = j
⊢ False
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

Tactic:
by_cases h₁ : j ∈ {beattySeq r k | k}

Goal state after:
case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∈ {x | ∃ k, beattySeq r k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

Tactic:
by_cases h₁ : j ∈ {beattySeq r k | k} <;> by_cases h₂ : j ∈ {beattySeq' s k | k}

Goal state after:
case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∈ {x | ∃ k, beattySeq r k = x}
h₂ : j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∈ {x | ∃ k, beattySeq r k = x}
h₂ : j ∉ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
h₂ : j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
h₂ : j ∉ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
⊢ selbergTerms d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

Tactic:
by
  unfold selbergTerms
  by_cases h : d = 0
  · simp [h]
  rw [ArithmeticFunction.pmul_apply, ArithmeticFunction.prodPrimeFactors_apply h]

Goal state after: