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

Goal state before:
pp: 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) in s,
      ENNReal.ofReal
          (Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
            regulator K) *
        f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      ∫⁻ (x : realSpace K) in s,
        ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
          f (↑expMapBasis x)

Tactic:
← lintegral_const_mul _ (by fun_prop)

Goal state after:
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) in s,
      ENNReal.ofReal
          (Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
            regulator K) *
        f (↑expMapBasis x) =
    ∫⁻ (a : realSpace K) in s,
      2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        (ENNReal.ofReal (Real.exp (a w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ a w) ↑i))⁻¹ *
          f (↑expMapBasis a))
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:
rw [mem_span_singleton]

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
h : 2 < p
⊢ ¬hζ.toInteger - 1 ∣ 2
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 ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ P = span {hζ✝.toInteger - 1}

Tactic:
exact eq_span_zeta_sub_one_of_liesOver p 0 K hζ P

Goal state after:
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
⊢ Submodule.IsPrincipal q'

Tactic:
have : p.IsMaximal := (hqp.under A).isMaximal (q.under_ne_bot A hq)

Goal state after:
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
⊢ Submodule.IsPrincipal q'
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 : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
I : ↥(Ideal (𝓞 K))⁰
⊢ ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C ↔ C = ClassGroup.mk0 I ∧ ↑(absNorm ↑J) * ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J)

Tactic:
mul_comm s,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
I : ↥(Ideal (𝓞 K))⁰
⊢ ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C ↔ C = ClassGroup.mk0 I ∧ ↑(absNorm ↑J) * ↑(absNorm ↑I) ≤ ↑(absNorm ↑J) * s
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 : Nat.card Gal(↥Fₘ/ℚ) * Nat.card Gal(↥Fₚ/ℚ) = Nat.card Gal(K/ℚ)
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1

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

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ₘ)) * Nat.card Gal(↥Fₚ/ℚ) =
    Nat.card Gal(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
hα0 : α ≠ 0
h_neg : ∀ (w : InfinitePlace K), w ↑α < 1
w₀ : InfinitePlace K := Classical.arbitrary (InfinitePlace K)
h_ge_one : 1 ≤ w₀ ↑α
⊢ False

Tactic:
exact (h_neg w₀).not_ge h_ge_one

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:

Tactic:
f n = f ((Nat.ofDigits m L : ℕ) : ℚ) := by rw [Nat.ofDigits_digits m n]
    _ = f L'.sum := by simp [L', Nat.ofDigits_eq_sum_mapIdx]
    _ ≤ (L'.map f).sum := listSum_le f L'
    _ ≤ (L.mapIdx fun i _ ↦ m * (f m) ^ i).sum := ?_

Goal state after:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
⊢ (List.map (⇑f) L').sum ≤ (List.mapIdx (fun i x ↦ ↑m * f ↑m ^ i) L).sum
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m✝ n✝ : ℕ
hm✝ : 1 < m✝
hn✝ : 1 < n✝
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
hfm : 1 < f ↑m
⊢ ↑m * ((f ↑m ^ (m.digits n).length - 1) / (f ↑m - 1)) = ↑m * ((f ↑m ^ (d + 1) - 1) / (f ↑m - 1))

Tactic:
← Nat.length_digits m n hm (ne_zero_of_lt hn)

Goal state after:
f : AbsoluteValue ℚ ℝ
m✝ n✝ : ℕ
hm✝ : 1 < m✝
hn✝ : 1 < n✝
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
hfm : 1 < f ↑m
⊢ ↑m * ((f ↑m ^ (m.digits n).length - 1) / (f ↑m - 1)) = ↑m * ((f ↑m ^ (m.digits n).length - 1) / (f ↑m - 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)
a b : ℤ_[p]
⊢ (mahlerSeries fun x ↦ r ^ x) (a + b) = (mahlerSeries fun x ↦ r ^ x) a * (mahlerSeries fun x ↦ r ^ x) b

Tactic:
by
    let F : C(ℤ_[p], R) := mahlerSeries (r ^ ·)
    change F (a + b) = F a * F b
    -- It is fiddly to show directly that `F (a + b) = F a * F b` for general `a, b`,
    -- so we prove it for `a, b ∈ ℕ` directly, and then deduce it for all `a, b` by continuity.
    have hF (n : ℕ) : F n = (r + 1) ^ n := by
      rw [mahlerSeries_apply_nat hr le_rfl, (Commute.one_right _).add_pow]
      refine Finset.sum_congr rfl fun i hi ↦ ?_
      rw [one_pow, mul_one, nsmul_eq_mul, Nat.cast_comm]
    refine congr_fun ((denseRange_natCast.prodMap denseRange_natCast).equalizer
      ((map_continuous F).comp continuous_add)
      (continuous_mul.comp (map_continuous <| F.prodMap F)) (funext fun ⟨m, n⟩ ↦ ?_)) (a, b)
    simp [← Nat.cast_add, hF, ContinuousMap.prodMap_apply, pow_add]

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

Goal state before:
pp: case hp
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsClosed {a | ‖withValUniformEquiv a‖ ≤ 1 ↔ Valued.v a ≤ 1}

Tactic:
rw [Set.ext fun _ ↦ Iff.comm]

Goal state after:
case hp
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsClosed {x | Valued.v x ≤ 1 ↔ ‖withValUniformEquiv x‖ ≤ 1}
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
E : Type u_4
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
inst✝¹ : Module R E
inst✝ : ContinuousSMul R E
⊢ ∀ (m₁ m₂ : AbstractMeasure Y R R) (n : C(X × Y, R)),
    (↑(m₁ + m₂)).comp n.curry = (↑m₁).comp n.curry + (↑m₂).comp n.curry

pp: X : Type u_1
Y : Type u_2
R : Type u_3
E : Type u_4
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
inst✝¹ : Module R E
inst✝ : ContinuousSMul R E
⊢ ∀ (c : R) (m : AbstractMeasure Y R R) (n : C(X × Y, R)), (↑(c • m)).comp n.curry = c • (↑m).comp n.curry

pp: X : Type u_1
Y : Type u_2
R : Type u_3
E : Type u_4
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
inst✝¹ : Module R E
inst✝ : ContinuousSMul R E
⊢ ∀ (m : AbstractMeasure Y R R) (n₁ n₂ : C(X × Y, R)),
    (↑m).comp (n₁ + n₂).curry = (↑m).comp n₁.curry + (↑m).comp n₂.curry

pp: X : Type u_1
Y : Type u_2
R : Type u_3
E : Type u_4
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
inst✝¹ : Module R E
inst✝ : ContinuousSMul R E
⊢ ∀ (c : R) (m : AbstractMeasure Y R R) (n : C(X × Y, R)), (↑m).comp (c • n).curry = c • (↑m).comp n.curry

Tactic:
finally
    all_goals intros; ext; simp

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : (a.x + b * a.y) * (a.x - b * a.y) = 1
⊢ False

Tactic:
Int.mul_eq_one_iff_eq_one_or_neg_one

Goal state after:
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x + b * a.y = 1 ∧ a.x - b * a.y = 1 ∨ a.x + b * a.y = -1 ∧ a.x - b * a.y = -1
⊢ False
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤

Tactic:
let M : Submodule R S := Submodule.span R b

Goal state after:
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case h
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
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
⊢ ∃ n, a = a₁ ^ n

Tactic:
| h x ih =>

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j + ↑1 - 1 < ↑m * s ∧ ↑m * s ≤ ↑j + ↑1
⊢ False

Tactic:
Int.cast_one,

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

Goal state before:
pp: case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ ↑⌈(↑j + 1) / r⌉ - ↑1 < ↑j / r ∧ (↑j + 1) / r ≤ ↑⌈(↑j + 1) / r⌉ - ↑1 + 1

Tactic:
Int.cast_one,

Goal state after:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ ↑⌈(↑j + 1) / r⌉ - 1 < ↑j / r ∧ (↑j + 1) / r ≤ ↑⌈(↑j + 1) / r⌉ - 1 + 1
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ ↑j ≤ (↑⌈(↑j + 1) / r⌉ - ↑1) * r ∧ (↑⌈(↑j + 1) / r⌉ - ↑1) * r < ↑j + 1

Tactic:
Int.cast_one,

Goal state after:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r ∧ (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j + 1
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ↑⌊↑k * r⌋ + ↑1 - 1 < ↑k * r ∧ ↑k * r ≤ ↑⌊↑k * r⌋ + ↑1

Tactic:
Int.cast_one,

Goal state after:
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ↑⌊↑k * r⌋ + 1 - 1 < ↑k * r ∧ ↑k * r ≤ ↑⌊↑k * r⌋ + 1
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ ∃ x, (valuation K⟮X⟯ p) x ≤ 1 ∧ 1 < (inftyValuation K) x ∨ 1 < (valuation K⟮X⟯ p) x ∧ (inftyValuation K) x ≤ 1

Tactic:
refine ⟨X, .inl ⟨p.valuation_le_one _, ?_⟩⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ 1 < (inftyValuation K) X
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
l : ℕ
hl : Squarefree l
hnu_nonzero : s.nu l ≠ 0
⊢ (selbergTerms l)⁻¹ =
    ∑ x ∈ l.divisorsAntidiagonal,
      match x with
      | (d, e) => ↑(μ d) * (s.nu e)⁻¹

Tactic:
simp only [selbergTerms_apply, mul_inv, inv_inv,
    Finset.prod_inv_distrib, s.nu_mult.prodPrimeFactors_one_sub_of_squarefree _ hl, mul_sum]
  rw [← Nat.sum_divisorsAntidiagonal fun i _ : ℕ ↦ (s.nu l)⁻¹ * (↑(μ i) * s.nu i)]
  congr! 1 with ⟨d, e⟩ hd
  obtain ⟨rfl, -⟩ : d * e = l ∧ _ := by simpa using hd
  obtain ⟨hde, -⟩ : d.Coprime e ∧ _ := by simpa only [squarefree_mul_iff] using hl
  obtain ⟨hd0, he0⟩ : ¬s.nu d = 0 ∧ ¬s.nu e = 0 := by simp_all [s.nu_mult.map_mul_of_coprime hde]
  simp [field, s.nu_mult.map_mul_of_coprime hde, mul_assoc]

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

Goal state before:
pp: case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)

Tactic:
have mem_span_b : ((Submodule.mkQ (map (algebraMap R S) p)) x : S ⧸ map (algebraMap R S) p) ∈
          Submodule.span (R ⧸ p) (Set.range b) := b.mem_span _

Goal state after:
case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b : (Submodule.mkQ (map f p)) x ∈ Submodule.span (R ⧸ p) (Set.range ⇑b)
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ IsSquare (-1)

Tactic:
refine ⟨u * y, ?_⟩

Goal state after:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑u * ↑y * (↑u * ↑y)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p))‖ ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Tactic:
mul_comm s,

Goal state after:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖cexp s * ((∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)) * s)‖ ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case e'_4.e'_6
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ 1 = MeasureTheory.volume.real (Set.Ioc 0 1)

Tactic:
Real.volume_real_Ioc_of_le zero_le_one,

Goal state after:
case e'_4.e'_6
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ 1 = 1 - 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
⊢ ∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)

Tactic:
have me0 : 0 < max (1 / ε) M := lt_max_iff.mpr (Or.inl (one_div_pos.mpr e0))

Goal state after:
Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
⊢ ∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) ↥⊥ = 0

Tactic:
exact rank_bot (R ⧸ p) (S ⧸ P ^ e)

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ (↑p_k * ↑m ^ (k + 1)! + ↑(m ^ k !) * 1) / (↑(m ^ k !) * ↑m ^ (k + 1)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) / ↑(m ^ (k + 1)!)

pp: case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

pp: case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0

Tactic:
div_eq_div_iff,

Goal state after:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ (↑p_k * ↑m ^ (k + 1)! + ↑(m ^ k !) * 1) * ↑(m ^ (k + 1)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case calc_2
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
⊢ map f p ≠ ⊥

Tactic:
rwa [Ne, Ideal.map_eq_bot_iff_le_ker, (RingHom.injective_iff_ker_eq_bot _).mp <|
      algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ ↑b ≤ ↑b ^ (2 + 1 / ↑n.succ)

Tactic:
calc
      (b : ℝ) = (b : ℝ) ^ (1 : ℝ) := (rpow_one _).symm
      _ ≤ (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) :=
        rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n.succ)
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ 2 ≤ 2 + 1 / ↑(n + 1)
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case inl
h : ↑(0 - 1)! = -1
h1 : 0 ≠ 1
⊢ Prime 0

Tactic:
norm_num at h

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
hp : 1 < p
⊢ Irrational x

Tactic:
rintro ⟨r, rfl⟩
  rcases eq_or_ne r 0 with (rfl | h0)
  · refine h.ne_cast_int hp 0 ?_; rw [Rat.cast_zero, Int.cast_zero]
  · refine (h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_
    rw [Rat.cast_inv, mul_inv_cancel₀]
    exacts [Int.cast_one.symm, Rat.cast_ne_zero.mpr h0]

Goal state after: