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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
⊢ (algebraMap F K).comp (CMExtension.equivMaximalRealSubfield F K).symm.toRingHom =
    (RingEquiv.refl K).toRingHom.comp (algebraMap (↥(maximalRealSubfield K)) K)

Tactic:
ext

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x✝ : ↥(maximalRealSubfield K)
⊢ ((algebraMap F K).comp (CMExtension.equivMaximalRealSubfield F K).symm.toRingHom) x✝ =
    ((RingEquiv.refl K).toRingHom.comp (algebraMap (↥(maximalRealSubfield K)) K)) x✝
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
⊢ φ.comp (algebraMap ℚ K) = ψ.comp (algebraMap ℚ K)

Tactic:
ext

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
x✝ : ℚ
⊢ (φ.comp (algebraMap ℚ K)) x✝ = (ψ.comp (algebraMap ℚ K)) x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
← Real.exp_add,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) =
    Real.exp (x w₀ + 0) • fun w ↦
      ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i
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 θ
h : span {↑p} ≠ ⊥
⊢ (span {↑p}).primesOver (𝓞 K) = {J | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))}

Tactic:
ext

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
h : span {↑p} ≠ ⊥
x✝ : Ideal (𝓞 K)
⊢ x✝ ∈ (span {↑p}).primesOver (𝓞 K) ↔ x✝ ∈ {J | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))}
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ basisOfIsMaxRank ⋯ = Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ : Fin (rank K)
x✝ : { w // w ≠ w₀ }
⊢ (basisOfIsMaxRank ⋯) i✝ x✝ = (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) i✝ x✝
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
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
⊢ (algebraMap (ZMod p) ((ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})).comp
      (Int.quotientSpanNatEquivZMod p).toRingHom =
    (RingEquiv.toRingHom ?m.136).comp (algebraMap (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}))

Tactic:
ext

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
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
x✝ : ℤ
⊢ (((algebraMap (ZMod p) ((ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})).comp
            (Int.quotientSpanNatEquivZMod p).toRingHom).comp
        (Ideal.Quotient.mk (span {↑p})))
      x✝ =
    (((RingEquiv.toRingHom ?m.136).comp (algebraMap (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}))).comp
        (Ideal.Quotient.mk (span {↑p})))
      x✝
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx✝ : x ∈ torsion K
hx : x ∈ rootsOfUnity (torsionOrder K) (𝓞 K)
y : (𝓞 K)ˣ
hy✝ : y ∈ torsion K
hy : y ∈ rootsOfUnity (torsionOrder K) (𝓞 K)
h : I.torsionMapQuot ⟨x, hx✝⟩ = I.torsionMapQuot ⟨y, hy✝⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
exact rootsOfUnityMapQuot_injective (torsionOrder K) hI₁ hI₂ h

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
⊢ Function.Injective ⇑I.torsionMapQuot

Tactic:
intro ⟨x, hx⟩ ⟨y, hy⟩ h
  rw [← rootsOfUnity_eq_torsion] at hx hy
  rw [Subtype.mk_eq_mk, ← Subtype.mk_eq_mk (h := hx) (h' := hy)]
  exact rootsOfUnityMapQuot_injective (torsionOrder K) hI₁ hI₂ h

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

Goal state before:
pp: case pos
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : p = 2
⊢ Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p

Tactic:
cases k with
    | zero =>
      rw [h, zero_add, pow_one] at hK hζ
      rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
    | succ n =>
      rw [h, add_assoc, one_add_one_eq_two] at hK hζ
      rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]

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
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ (algebraMap F K) ζ ^ (↑((galEquivZMod m F) (σ.restrictNormal F))).val = (algebraMap F K) ((σ.restrictNormal F) ζ)

pp: case hx
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ (algebraMap F K) ζ ^ n = 1

Tactic:
galEquivZMod_apply_of_pow_eq m _ _ hζ.pow_eq_one,

Goal state after:
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ (algebraMap F K) ζ ^ (↑((galEquivZMod m F) (σ.restrictNormal F))).val =
    (algebraMap F K) (zeta m ℚ F ^ (↑((galEquivZMod m F) (σ.restrictNormal F))).val)

case hx
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ (algebraMap F K) ζ ^ n = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)

Tactic:
have h := isPrime_span_zeta_sub_one p k hζ
  have hp0 : 𝒑 ≠ ⊥ := by simpa using hp.out.ne_zero
  rw [← Nat.totient_prime_pow_succ hp.out, ← finrank _ K,
    IsDedekindDomain.ramificationIdx_eq_multiplicity 𝒑, map_eq_span_zeta_sub_one_pow p k hζ,
    multiplicity_pow_self (span_zeta_sub_one_ne_bot p k hζ) (isUnit_iff.not.mpr h.ne_top)]
  exact map_ne_bot_of_ne_bot hp0

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ (fun x ↦
      x ∈
        ⇑(↑(toMixed K)).toEquiv ''
          ({x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∩
            ⇑↑↑(toMixed K) ⁻¹' ↑(idealLattice K ((FractionalIdeal.mk0 K) J)))) =
    fun x ↦ x ∈ idealSet K J ∧ mixedEmbedding.norm x ≤ s

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ x✝ ∈
      ⇑(↑(toMixed K)).toEquiv ''
        ({x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∩
          ⇑↑↑(toMixed K) ⁻¹' ↑(idealLattice K ((FractionalIdeal.mk0 K) J))) ↔
    x✝ ∈ idealSet K J ∧ mixedEmbedding.norm x✝ ≤ s
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ∃ y ∈ ↑↑↑J, (mixedEmbedding K) y = ↑↑(toMixed K) x) ∧
        (↑(toMixed K)).toEquiv x = x✝) ↔
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ∃ y ∈ ↑↑↑J, (mixedEmbedding K) y = ↑↑(toMixed K) x) ∧
        (↑(toMixed K)).toEquiv x = x✝) →
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s

case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s →
    ∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ∃ y ∈ ↑↑↑J, (mixedEmbedding K) y = ↑↑(toMixed K) x) ∧
        (↑(toMixed K)).toEquiv x = x✝
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ∃ y ∈ ↑↑↑J, (mixedEmbedding K) y = ↑↑(toMixed K) x) ∧
        (↑(toMixed K)).toEquiv x = x✝) →
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s

Tactic:
rintro ⟨_, ⟨⟨hx₁, hx₂⟩, _, ⟨x, hx₃, rfl⟩, h⟩, rfl⟩
    exact ⟨⟨hx₁, x, hx₃, h⟩, hx₂⟩

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

Goal state before:
pp: 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}
⊢ {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K

Tactic:
ext

Goal state after:
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}
x✝ : mixedSpace K
⊢ x✝ ∈ {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} ↔ x✝ ∈ normLeOne K
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑n * max 1 ‖A‖ * ↑B + 1) ^ m ≤ (↑n * max 1 ‖A‖) ^ m * (↑B + 1) ^ m

Tactic:
rw [← mul_pow, mul_add, mul_one]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑n * max 1 ‖A‖ * ↑B + 1) ^ m ≤ (↑n * max 1 ‖A‖ * ↑B + ↑n * max 1 ‖A‖) ^ m
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
⊢ Summable f ↔ (CauchySeq fun s ↦ ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
⊢ Summable f → (CauchySeq fun s ↦ ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

case mpr
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
⊢ (CauchySeq fun s ↦ ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl → Summable f
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
constructor

Goal state after:
case mpr.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f)

case mpr.right
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ -↑⌊(↑n * max 1 ‖A‖) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ ≤ x i - y i ∧
    x i - y i ≤ ↑⌊(↑n * max 1 ‖A‖) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
constructor

Goal state after:
case left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ -↑⌊(↑n * max 1 ‖A‖) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ ≤ x i - y i

case right
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ x i - y i ≤ ↑⌊(↑n * max 1 ‖A‖) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊
Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
⊢ IsUltrametricDist C(X, Y)

Tactic:
constructor

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
⊢ ∀ (x y z : C(X, Y)), dist x z ≤ max (dist x y) (dist y z)
Module: Mathlib.Topology.Algebra.Monoid.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝⁴ : TopologicalSpace A
inst✝³ : AddMonoidWithOne A
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
hdr : DenseRange Nat.cast
κ₁ κ₂ : AddChar A M
hκ₁ : Continuous ⇑κ₁
hκ₂ : Continuous ⇑κ₂
h : κ₁ 1 = κ₂ 1
n : ℕ
⊢ (⇑κ₁ ∘ Nat.cast) n = (⇑κ₂ ∘ Nat.cast) n

Tactic:
simp only [Function.comp_apply, ← nsmul_one, h, AddChar.map_nsmul_eq_pow]

Goal state after:
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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
⊢ 0 < p ∧ 0 < h ∨ p < 0 ∧ h < 0

Tactic:
constructor

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := ⋯
hphqh : p * h < q * h
⊢ 0 < p ∧ 0 < h
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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
⊢ Fintype.card α * Fintype.card (K →+* ℂ) = p * h

Tactic:
cardα,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
⊢ p * Fintype.card (K →+* ℂ) = p * h
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Valued.v ((algebraMap ℚ_[p] (PadicAlgCl p)) ↑p) = 1 / ↑p

Tactic:
ext

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(Valued.v ((algebraMap ℚ_[p] (PadicAlgCl p)) ↑p)) = ↑(1 / ↑p)
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ ‖↑x‖₊ = ‖x‖₊

Tactic:
ext

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ ↑‖↑x‖₊ = ↑‖x‖₊
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ‖↑((algebraMap ℚ_[p] (PadicAlgCl p)) x)‖₊ = ‖x‖₊

Tactic:
ext

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ↑‖↑((algebraMap ℚ_[p] (PadicAlgCl p)) x)‖₊ = ↑‖x‖₊
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 : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖↑((-1) ^ (n - i) * ↑(n.choose i))‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖ ≤
    ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖

Tactic:
by norm_cast

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
⊢ (∀ (i : ℕ),
      ∃ j,
        ∀ (x y : WithVal (Rat.padicValuation p)),
          Valued.v.restrict (y - x) < ↑j →
            ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ i)⁻¹) ∧
    ∀ (j : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ),
      ∃ i,
        ∀ (x y : WithVal (Rat.padicValuation p)),
          ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ i)⁻¹ → Valued.v.restrict (y - x) < ↑j

Tactic:
constructor

Goal state after:
case left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
⊢ ∀ (i : ℕ),
    ∃ j,
      ∀ (x y : WithVal (Rat.padicValuation p)),
        Valued.v.restrict (y - x) < ↑j → ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ i)⁻¹

case right
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
⊢ ∀ (j : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ),
    ∃ i,
      ∀ (x y : WithVal (Rat.padicValuation p)),
        ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ i)⁻¹ → Valued.v.restrict (y - x) < ↑j
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)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
t : ℕ
ht : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
m : ℕ
hm : s * p ^ t ≤ m
⊢ ‖Δ_[1]^[m] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
simpa only [Nat.sub_add_cancel hm] using fwdDiff_iter_le_of_forall_le ht (m - s * p ^ t)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ mahlerTerm 1 n = mahler n

Tactic:
ext

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a✝ : ℤ_[p]
⊢ (mahlerTerm 1 n) a✝ = (mahler n) a✝
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
R✝ : Type u_3
V : Type u_4
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : TotallyDisconnectedSpace X✝
inst✝¹¹ : T2Space X✝
inst✝¹⁰ : CompactSpace X✝
inst✝⁹ : TopologicalSpace Y✝
inst✝⁸ : CompactSpace Y✝
inst✝⁷ : AddCommGroup V
inst✝⁶ : UniformSpace V
inst✝⁵ : IsUniformAddGroup V
S : Set (V × V)
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
f f' : C(X, R)
g : C(Y, R)
⊢ (f + f').comp fst * g.comp snd = f.comp fst * g.comp snd + f'.comp fst * g.comp snd

Tactic:
ext

Goal state after:
X✝ : Type u_1
Y✝ : Type u_2
R✝ : Type u_3
V : Type u_4
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : TotallyDisconnectedSpace X✝
inst✝¹¹ : T2Space X✝
inst✝¹⁰ : CompactSpace X✝
inst✝⁹ : TopologicalSpace Y✝
inst✝⁸ : CompactSpace Y✝
inst✝⁷ : AddCommGroup V
inst✝⁶ : UniformSpace V
inst✝⁵ : IsUniformAddGroup V
S : Set (V × V)
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
f f' : C(X, R)
g : C(Y, R)
a✝ : X × Y
⊢ ((f + f').comp fst * g.comp snd) a✝ = (f.comp fst * g.comp snd + f'.comp fst * g.comp snd) a✝