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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) = normAtComplexPlaces (mixedSpaceOfRealSpace x.1)

Tactic:
ext w

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
w : InfinitePlace K
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) w = normAtComplexPlaces (mixedSpaceOfRealSpace x.1) w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a : ↑(integerSet K)
⊢ ¬↑a = 0

Tactic:
ne_zero_of_mem_integerSet,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a : ↑(integerSet K)
⊢ ¬False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ ⟦preimageOfMemIntegerSet a⟧ = ⟦preimageOfMemIntegerSet b⟧ ↔ ∃ ζ, ζ • a = b

Tactic:
Associates.quotient_mk_eq_mk,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ Associates.mk (preimageOfMemIntegerSet a) = Associates.mk (preimageOfMemIntegerSet b) ↔ ∃ ζ, ζ • a = b
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
ζ : ↥(torsion K)
⊢ ↑((unitsMulComplexConjInv K) ↑ζ) = ↑(ζ ^ 2)

Tactic:
by simp [unitsMulComplexConjInv_apply, unitsComplexConj_torsion, pow_two]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² : ℝ
x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ (x✝² • x✝¹) ↑x✝ - (↑(↑x✝).mult * ∑ w', (x✝² • x✝¹) w') * (↑(finrank ℚ K))⁻¹ =
    ((RingHom.id ℝ) x✝² • fun w ↦ x✝¹ ↑w - (↑(↑w).mult * ∑ w', x✝¹ w') * (↑(finrank ℚ K))⁻¹) x✝

Tactic:
simp [← mul_sum]; ring

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
⊢ realSpaceToLogSpace (↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x))) = logMap ((mixedEmbedding K) x)

Tactic:
ext w

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace (↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x))) w = logMap ((mixedEmbedding K) x) w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) ↑w -
      (↑(↑w).mult * ∑ w', ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) w') * (↑(finrank ℚ K))⁻¹ =
    logMap ((mixedEmbedding K) x) w

Tactic:
sum_expMap_symm_apply hx,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) ↑w -
      ↑(↑w).mult * Real.log ↑|(Algebra.norm ℚ) x| * (↑(finrank ℚ K))⁻¹ =
    logMap ((mixedEmbedding K) x) w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))) ∈ expMap.target

Tactic:
by simp [expMap_target, pos_at_place]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝² : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this✝¹ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this✝ : IsTotallyComplex K
this : IsAbelianGalois ℚ K
⊢ IsCMField K

Tactic:
exact IsCMField.of_isAbelianGalois K

Goal state after:
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
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
← 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
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card =
    (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) / orderOf (unitOfCoprime (p ^ f) ⋯)
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
n : ℕ
ζ : K
hn : 2 ≤ n
hζ : IsPrimitiveRoot ζ n
h : hζ.toInteger - 1 ∈ I
h₁ : (absNorm I).Coprime n
p : ℕ
hp : Nat.Prime p
h₂ : p ∣ absNorm I
this : Fact (Nat.Prime p)
⊢ False

Tactic:
refine hp.not_dvd_one <| h₁ ▸ Nat.dvd_gcd h₂ ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI : absNorm I ≠ 1
n : ℕ
ζ : K
hn : 2 ≤ n
hζ : IsPrimitiveRoot ζ n
h : hζ.toInteger - 1 ∈ I
h₁ : (absNorm I).Coprime n
p : ℕ
hp : Nat.Prime p
h₂ : p ∣ absNorm I
this : Fact (Nat.Prime p)
⊢ p ∣ n
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
⊢ x ∈ normAtAllPlaces '' normLeOne K ↔ x ∈ ↑expMapBasis '' paramSet K

Tactic:
rw [← expMapBasis.right_inv (Set.mem_univ_pi.mpr hx), (injective_expMapBasis K).mem_set_image]
    simp only [normAtAllPlaces_normLeOne, Set.mem_inter_iff, Set.mem_ofPred_eq, expMapBasis_nonneg,
      Set.mem_preimage, logMap_expMapBasis, implies_true, and_true, norm_expMapBasis,
      pow_le_one_iff_of_nonneg (Real.exp_nonneg _) Module.finrank_pos.ne', Real.exp_le_one_iff,
      ne_eq, pow_eq_zero_iff', Real.exp_ne_zero, false_and, not_false_eq_true, Set.mem_univ_pi]
    refine ⟨fun ⟨h₁, h₂⟩ w ↦ ?_, fun h ↦ ⟨fun w hw ↦ by simpa [hw] using h w, by simpa using h w₀⟩⟩
    · split_ifs with hw
      · exact hw ▸ h₂
      · exact h₁ w hw

Goal state after:
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
x : 𝓞 K
hx : ¬hζ.toInteger - 1 ∣ x
⊢ gcd (span {hζ.toInteger - 1}) (span {x}) = 1

Tactic:
(prime_span_singleton_iff.mpr
    hζ.zeta_sub_one_prime').irreducible.gcd_eq_one_iff,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
x : 𝓞 K
hx : ¬hζ.toInteger - 1 ∣ x
⊢ ¬span {hζ.toInteger - 1} ∣ span {x}
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

Tactic:
rcases le_total 0 (A i j) with hsign | hsign

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
rcases le_total 0 (A i j) with hsign | hsign

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺

case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
hs : 0 ≤ s
this : Fintype { I // ↑(absNorm ↑I) ≤ s }
e : (C : ClassGroup (𝓞 K)) → { x // ClassGroup.mk0 ↑x = C } ≃ { x // ↑(absNorm ↑x) ≤ s ∧ ClassGroup.mk0 x = C } :=
  fun C ↦ Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ ↑(absNorm ↑I) ≤ s) fun I ↦ ClassGroup.mk0 I = C
⊢ ∑ x, ↑{x_1 | ClassGroup.mk0 ↑x_1 = x}.card / s = ↑(Fintype.card { I // ↑(absNorm ↑I) ≤ s }) / s

Tactic:
Fintype.card,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
hs : 0 ≤ s
this : Fintype { I // ↑(absNorm ↑I) ≤ s }
e : (C : ClassGroup (𝓞 K)) → { x // ClassGroup.mk0 ↑x = C } ≃ { x // ↑(absNorm ↑x) ≤ s ∧ ClassGroup.mk0 x = C } :=
  fun C ↦ Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ ↑(absNorm ↑I) ≤ s) fun I ↦ ClassGroup.mk0 I = C
⊢ ∑ x, ↑{x_1 | ClassGroup.mk0 ↑x_1 = x}.card / s = ↑Finset.univ.card / s
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
⊢ ∏ x, (∑ x_1, ↑B * ↑(A x x_1)⁺ - ∑ x_1, ↑B * -↑(A x x_1)⁻ + 1) < (↑B + 1) ^ n

Tactic:
calc
  ∏ x : α, (∑ x_1 : β, ↑B * ↑(A x x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A x x_1)⁻ + 1)
    ≤ ∏ x : α, (n * max 1 ‖A‖ * B + 1) := by
      refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)
      · have h := N_le_P_add_one A i
        rify at h
        linarith only [h]
      · simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]
        have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
          simp
          ring
        simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]
        gcongr with j _
        rw [posPart_add_negPart (A i j), Int.cast_abs]
        exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)
  _ = (n * max 1 ‖A‖ * B + 1) ^ m := by simp
  _ ≤ (n * max 1 ‖A‖) ^ m * (B + 1) ^ m := by
        rw [← mul_pow, mul_add, mul_one]
        gcongr
        have H : 1 ≤ (n : ℝ) := mod_cast (hm.trans hn)
        exact one_le_mul_of_one_le_of_one_le H <| le_max_left ..
  _ = ((n * max 1 ‖A‖) ^ (m / ((n : ℝ) - m))) ^ ((n : ℝ) - m) * (B + 1) ^ m := by
        congr 1
        rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (le_trans zero_le_one (le_max_left ..))),
          ← Real.rpow_natCast, div_mul_cancel₀]
        exact sub_ne_zero_of_ne (mod_cast hn.ne')
  _ < (B + 1) ^ ((n : ℝ) - m) * (B + 1) ^ m := by
        gcongr
        · exact sub_pos.mpr (mod_cast hn)
        · exact Nat.lt_floor_add_one ((n * max 1 ‖A‖) ^ e)
  _ = (B + 1) ^ n := by
        rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: case h
α : 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
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
⊢ Disjoint t (Set.Finite.toFinset ⋯) → ∏ b ∈ t, f b ∈ U

Tactic:
ht

Goal state after:
case h
α : 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
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∏ b ∈ t, f b ∈ U
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
⊢ f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹

Tactic:
calc
    f n = (f ↑(n ^ k)) ^ (k : ℝ)⁻¹ := by
      rw [Nat.cast_pow, map_pow, ← rpow_natCast, rpow_rpow_inv (by positivity) (by positivity)]
    _ ≤ (n₀ * (logb n₀ ↑(n ^ k) + 1)) ^ (k : ℝ)⁻¹ := by
      gcongr
      exact h_ineq1 <| one_le_pow₀ (one_le_iff_ne_zero.mpr h₀)
    _ = (n₀ * (k * logb n₀ n + 1)) ^ (k : ℝ)⁻¹ := by
      rw [Nat.cast_pow, logb_pow]
    _ ≤ (n₀ * (k * logb n₀ n + k)) ^ (k : ℝ)⁻¹ := by
      gcongr
      exact one_le_cast.mpr hk
    _ = (n₀ * (logb n₀ n + 1)) ^ (k : ℝ)⁻¹ * k ^ (k : ℝ)⁻¹ := by
      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: case inr
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
⊢ f ↑n ≤ 1

Tactic:
have h_ineq2 (k : ℕ) (hk : 0 < k) :
      f n ≤ (n₀ * (logb n₀ n + 1)) ^ (k : ℝ)⁻¹ * k ^ (k : ℝ)⁻¹ := by
    have : 0 ≤ logb n₀ n := logb_nonneg (mod_cast hn₀) (mod_cast one_le_iff_ne_zero.mpr h₀)
    calc
    f n = (f ↑(n ^ k)) ^ (k : ℝ)⁻¹ := by
      rw [Nat.cast_pow, map_pow, ← rpow_natCast, rpow_rpow_inv (by positivity) (by positivity)]
    _ ≤ (n₀ * (logb n₀ ↑(n ^ k) + 1)) ^ (k : ℝ)⁻¹ := by
      gcongr
      exact h_ineq1 <| one_le_pow₀ (one_le_iff_ne_zero.mpr h₀)
    _ = (n₀ * (k * logb n₀ n + 1)) ^ (k : ℝ)⁻¹ := by
      rw [Nat.cast_pow, logb_pow]
    _ ≤ (n₀ * (k * logb n₀ n + k)) ^ (k : ℝ)⁻¹ := by
      gcongr
      exact one_le_cast.mpr hk
    _ = (n₀ * (logb n₀ n + 1)) ^ (k : ℝ)⁻¹ * k ^ (k : ℝ)⁻¹ := by
      rw [← mul_rpow (by positivity) (by positivity), mul_assoc, add_mul, one_mul,
        mul_comm _ (k : ℝ)]

Goal state after:
case inr
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)⁻¹
⊢ f ↑n ≤ 1
Module: Mathlib.NumberTheory.Padics.AddChar

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ ∑ i ∈ Finset.range 1, Nat.choose 0 i • r ^ i = 1

Tactic:
Finset.sum_range_one,

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ Nat.choose 0 0 • r ^ 0 = 1
Module: Mathlib.NumberTheory.Padics.AddChar

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ ∑ x ∈ Finset.range 1, Nat.choose 1 x • r ^ x + Nat.choose 1 1 • r ^ 1 = 1 + r

Tactic:
Finset.sum_range_one,

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ Nat.choose 1 0 • r ^ 0 + Nat.choose 1 1 • r ^ 1 = 1 + r
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i ∈ range (p ^ t - 1)
⊢ ‖↑((p ^ t).choose (i + 1)) • Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ ≤ (↑p)⁻¹ * ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊

Tactic:
refine (nnnorm_smul_le _ _).trans <| mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le])

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i ∈ range (p ^ t - 1)
⊢ ‖↑((p ^ t).choose (i + 1))‖₊ ≤ (↑p)⁻¹
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case succ
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
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ‖Δ_[1]^[n + (k + 1) * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ (k + 1)

Tactic:
rw [add_mul, one_mul, ← add_assoc]
    refine (bojanic_mahler_step2 hst (n + k * p ^ t)).trans (max_le ?_ ?_)
    · rw [← coe_nnnorm, ← NNReal.coe_natCast, ← NNReal.coe_pow, ← NNReal.coe_div, NNReal.coe_le_coe]
      refine Finset.sup_le fun j _ ↦ ?_
      rw [pow_succ, ← div_div, div_le_div_iff_of_pos_right (mod_cast hp.out.pos), add_right_comm]
      exact_mod_cast IH (n + (j + 1)) (by lia)
    · exact div_le_div_of_nonneg_left (norm_nonneg _)
        (mod_cast pow_pos hp.out.pos _) (mod_cast pow_le_pow_right₀ hp.out.one_le hk)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
⊢ Tendsto (fun x ↦ Δ_[1]^[x] (⇑f) 0) atTop (𝓝 0)

Tactic:
refine NormedAddGroup.tendsto_nhds_zero.mpr (fun ε hε ↦ ?_)
  have : Tendsto (fun s ↦ ‖f‖ / p ^ s) _ _ := tendsto_const_nhds.div_atTop
    (tendsto_pow_atTop_atTop_of_one_lt (mod_cast hp.out.one_lt))
  obtain ⟨s, hs⟩ := (this.eventually_lt_const hε).exists
  refine .mp ?_ (.of_forall fun x hx ↦ lt_of_le_of_lt hx hs)
  -- use uniform continuity to find `t`
  obtain ⟨t, ht⟩ : ∃ t : ℕ, ∀ x y, ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s := by
    rcases eq_or_ne f 0 with rfl | hf
    · -- silly case : f = 0
      simp
    have : 0 < ‖f‖ / p ^ s := div_pos (norm_pos_iff.mpr hf) (mod_cast pow_pos hp.out.pos _)
    obtain ⟨δ, hδpos, hδf⟩ := f.uniform_continuity _ this
    obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos
    exact ⟨t, fun x y hxy ↦  by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le⟩
  filter_upwards [eventually_ge_atTop (s * p ^ t)] with m hm
  simpa only [Nat.sub_add_cancel hm] using fwdDiff_iter_le_of_forall_le ht (m - s * p ^ t)

Goal state after:
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)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
⊢ ∃ n g h, ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x • (h i) y) ∈ S

Tactic:
have hS' : {(f, g) | ∀ y, (f y, g y) ∈ S} ∈ 𝓤 C(Y, V) :=
    (mem_compactConvergence_entourage_iff _).mpr
      ⟨_, _, isCompact_univ, hS, by simp only [Set.mem_univ, true_implies, subset_refl]⟩
  obtain ⟨n, U, v, hv⟩ := exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal
    f.curry (nhdsSet_diagonal_le_uniformity hS')
  refine ⟨n, fun i ↦ ⟨_, (U i).isClopen.continuous_indicator <| continuous_const (y := 1)⟩,
    v, fun x y ↦ ?_⟩
  convert! hv x y using 2
  simp only [sum_apply]
  congr 1 with i
  by_cases hi : x ∈ U i <;> simp [hi]

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inl
n : ℕ
hk0 : 1 ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]

Tactic:
rcases exists_infinite_primes (n + 1) with ⟨p, hnp, hp⟩

Goal state after:
case inl
n : ℕ
hk0 : 1 ≠ 0
p : ℕ
hnp : n + 1 ≤ p
hp : Prime p
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
Module: Mathlib.NumberTheory.Pell

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

Tactic:
exact mod_cast mt sub_eq_zero.mp (mt Rat.eq_iff_mul_eq_mul.mpr hne)

Goal state after: