mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
⊢ ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 S_1), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun a ↦ a⁻¹) ∘ inclusion R (fun i ↦ ↑(B i)) hS)

Tactic:
intro T

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T✝ : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
T : Set ι
⊢ ∀ (hS : 𝓕 ≤ 𝓟 T),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 T), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun a ↦ a⁻¹) ∘ inclusion R (fun i ↦ ↑(B i)) hS)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
⊢ ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 S_1), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun x ↦ g • x) ∘ inclusion R (fun i ↦ ↑(B i)) hS)

Tactic:
intro T

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T✝ : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
T : Set ι
⊢ ∀ (hS : 𝓕 ≤ 𝓟 T),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 T), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun x ↦ g • x) ∘ inclusion R (fun i ↦ ↑(B i)) hS)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫⁻ (x : mixedSpace K), f x

Tactic:
by
  rw [← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).lintegral_comp_emb
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding, ← lintegral_comp_polarCoordReal_symm,
    polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq, Function.comp_def]

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

Goal state before:
pp: case hy
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) y ≠ 0

Tactic:
· exact mixedEmbedding.norm_ne_zero_iff.mp hy w

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
rw [Set.mem_ofPred_eq, mixedEmbedding.norm_smul, mul_eq_zero, not_or]
    exact ⟨pow_ne_zero _ (abs_ne_zero.mpr hc), hx.2⟩

Goal state after:
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)
⊢ ¬(algebraMap (𝓞 K) K) ⋯.choose = (algebraMap (𝓞 K) K) 0

Tactic:
← (mixedEmbedding_injective K).eq_iff,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a : ↑(integerSet K)
⊢ ¬(mixedEmbedding K) ((algebraMap (𝓞 K) K) ⋯.choose) = (mixedEmbedding K) ((algebraMap (𝓞 K) K) 0)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
hx : (mixedEmbedding K) ↑x ∈ integerSet K
⊢ ↑↑(preimageOfMemIntegerSet ⟨(mixedEmbedding K) ↑x, hx⟩) = ↑x

Tactic:
← (mixedEmbedding_injective K).eq_iff,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
hx : (mixedEmbedding K) ↑x ∈ integerSet K
⊢ (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet ⟨(mixedEmbedding K) ↑x, hx⟩) = (mixedEmbedding K) ↑x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ ↑↑(preimageOfMemIntegerSet ⟨u • (mixedEmbedding K) ↑↑x, hu⟩ * ↑(unitsNonZeroDivisorsEquiv.symm u⁻¹)) = ↑↑x

Tactic:
← (mixedEmbedding_injective K).eq_iff,

Goal state after:
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ (mixedEmbedding K)
      ↑↑(preimageOfMemIntegerSet ⟨u • (mixedEmbedding K) ↑↑x, hu⟩ * ↑(unitsNonZeroDivisorsEquiv.symm u⁻¹)) =
    (mixedEmbedding K) ↑↑x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

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

Tactic:
← (mixedEmbedding_injective K).eq_iff,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ (∃ u, (mixedEmbedding K) ↑↑(↑u * preimageOfMemIntegerSet a) = (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet b)) ↔
    ∃ ζ, ↑(ζ • a) = ↑b
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w // w.IsReal }
⊢ 0 < x.1 w

Tactic:
have := funext_iff.mp ha₂ w

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w // w.IsReal }
this : normAtComplexPlaces a ↑w = normAtComplexPlaces x ↑w
⊢ 0 < x.1 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
u : (↥(𝓞 K)⁰)ˣ
h : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
⊢ unitsNonZeroDivisorsEquiv u ∈ torsion K

Tactic:
exact (unit_smul_mem_iff_mem_torsion a.prop.1 _).mp (by simpa [h] using b.prop.1)

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
have h₁ := indexRealUnits_mul_eq K
  obtain h₂ | h₂ := (Nat.dvd_prime Nat.prime_two).mp <| index_unitsMulComplexConjInv_range_dvd K
  · exact Or.inr <| by rwa [h₂, mul_one] at h₁
  · exact Or.inl <| by rwa [h₂, Nat.mul_eq_right two_ne_zero] at h₁

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedEmbedding.norm (mixedSpaceOfRealSpace (normAtAllPlaces x)) = mixedEmbedding.norm x

Tactic:
mixedEmbedding.norm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ∏ w, (normAtPlace w) (mixedSpaceOfRealSpace (normAtAllPlaces x)) ^ w.mult = ∏ w, (normAtPlace w) x ^ w.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x x✝ : realSpace K
h : x✝ ∈ Set.range fun w ↦ completeFamily K ↑w
⊢ ∑ w, x✝ w = 0

Tactic:
obtain ⟨w, rfl⟩ := h

Goal state after:
case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : { w // w ≠ w₀ }
⊢ ∑ w_1, (fun w ↦ completeFamily K ↑w) w w_1 = 0
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 fun w ↦
        (∑ i, (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i) ↑w)
      (equivFinRank.symm ⟨w, hw⟩) ∈
    Set.Ico 0 1

Tactic:
enter [2, 1, 2, w, 2, i]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w✝ : InfinitePlace K
hw : w✝ ≠ w₀
w i : { i // i ≠ w₀ }
| (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |∏ x_1, deriv_expMap_single x_1 ((completeBasis K).equivFun.symm x x_1)| * (↑(finrank ℚ K) * regulator K) =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
prod_deriv_expMap_single

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |Real.exp (x w₀) ^ finrank ℚ K * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K| *
      (↑(finrank ℚ K) * regulator K) =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (paramSet K) =ᵐ[volume] interior (paramSet K)

Tactic:
by
  rw [closure_paramSet, interior_paramSet, volume_pi]
  refine Measure.ae_eq_set_pi fun w _ ↦ ?_
  split_ifs
  · exact Iio_ae_eq_Iic.symm
  · exact Ioo_ae_eq_Icc.symm

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 ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
n : ℤ
⊢ hζ✝.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n

Tactic:
exact zeta_sub_one_dvd_intCast_iff p 0 hζ

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

Goal state before:
pp: case h_fin
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (normLeOne K) < ∞

Tactic:
volume_normLeOne

Goal state after:
case h_fin
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) < ∞
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝⁴ : IsDomain 𝒪
this✝³ : IsDedekindDomain 𝒪
this✝² : IsFractionRing 𝒪 K
this✝¹ : Module.Finite ℤ 𝒪
this✝ : CharZero 𝒪
this : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
⊢ ∃ p, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
have := IsGaloisGroup.of_isFractionRing Gal(K/ℚ) ℤ 𝒪 ℚ K

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝⁵ : IsDomain 𝒪
this✝⁴ : IsDedekindDomain 𝒪
this✝³ : IsFractionRing 𝒪 K
this✝² : Module.Finite ℤ 𝒪
this✝¹ : CharZero 𝒪
this✝ : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this : IsGaloisGroup Gal(K/ℚ) ℤ 𝒪
⊢ ∃ p, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_3
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
s : ℝ
⊢ ↑(Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }) / s =
    ((fun x ↦ ↑(Nat.card { a // mixedEmbedding.norm ↑a ≤ x }) / x * (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)) ∘ fun x ↦
        x * ↑(absNorm ↑J))
      s

Tactic:
← card_isPrincipal_dvd_norm_le,

Goal state after:
case e'_3
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
s : ℝ
⊢ ↑(Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }) / s =
    ((fun x ↦
          ↑(Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ x } * torsionOrder K) / x *
            (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)) ∘
        fun x ↦ x * ↑(absNorm ↑J))
      s
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < ↑(⌈logb M (1 / 2)⌉₊ + 1)

Tactic:
push_cast

Goal state after:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < ↑⌈logb M (1 / 2)⌉₊ + 1
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f 1 = f (↑a * ↑p ^ k + ↑b * ↑m ^ k)

Tactic:
by rw_mod_cast [bezout]; norm_cast

Goal state after:
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]
        gcongr
        have H : 1 ≤ (n : ℝ) := mod_cast (hm.trans hn)
        exact one_le_mul_of_one_le_of_one_le H <| le_max_left ..

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

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

Tactic:
by
      rw [Nat.cast_pow, logb_pow]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
by_cases bdd : ∀ n : ℕ, f n ≤ 1

Goal state after:
case pos
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

case neg
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real ∨ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p
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
a : E
n : ℕ
x : ℤ_[p]
⊢ (mahlerTerm a n) x = (mahler n) x • a

Tactic:
simp only [mahlerTerm, ContinuousMap.smul_apply', ContinuousMap.const_apply]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ih : 0 < (a ^ n.succ).y
⊢ 0 < (a ^ (n + 1).succ).y

Tactic:
rw [pow_succ']

Goal state after:
case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ih : 0 < (a ^ n.succ).y
⊢ 0 < (a * a ^ (n + 1)).y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ ↑|d * ↑q.den ^ 2 - q.num ^ 2| / |↑q.den ^ 2| < ↑M / |↑q.den ^ 2|

Tactic:
push_cast

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |↑d * ↑q.den ^ 2 - ↑q.num ^ 2| / |↑q.den ^ 2| < ↑M / |↑q.den ^ 2|
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: 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
⊢ m ≠ 0

Tactic:
rintro rfl

Goal state after:
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
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}.Infinite
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: 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
hm₀ : m ≠ 0
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
⊢ ↑(q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)) = 0

Tactic:
push_cast

Goal state after:
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
hm₀ : m ≠ 0
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
⊢ ↑q₁.num * ↑q₂.num - ↑d * (↑q₁.den * ↑q₂.den) = 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: 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
hm₀ : m ≠ 0
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)
⊢ ↑(q₂.num * ↑q₁.den) = ↑(q₁.num * ↑q₂.den)

Tactic:
push_cast

Goal state after:
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
hm₀ : m ≠ 0
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)
⊢ ↑q₂.num * ↑q₁.den = ↑q₁.num * ↑q₂.den
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)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
⊢ x ∈ p • ⊤

Tactic:
smul_top_eq

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
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
⊢ x ∈ ⊤
Module: Mathlib.NumberTheory.Pell

Goal state before:

Tactic:
a.y ^ 2 = 1 * a.y ^ 2 := (one_mul _).symm
    _ ≤ d * a.y ^ 2 := (mul_le_mul_iff_left₀ <| sq_pos_of_pos hay).mpr h.d_pos
    _ < d * a.y ^ 2 + 1 := lt_add_one _
    _ = (1 + d * a.y ^ 2) * 1 := by rw [add_comm, mul_one]
    _ ≤ (1 + d * a.y ^ 2) * a₁.y ^ 2 :=
      (mul_le_mul_iff_right₀ (by have := h.d_pos; positivity)).mpr (sq_pos_of_pos h.2.1)

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]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ≤
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
by
      gcongr
      apply newton_seq_norm_le

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ ¬∃ j k m, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1 ∧ ↑m ≤ ↑j / s ∧ (↑j + 1) / s < ↑m + 1

Tactic:
intro ⟨j, k, m, h₁₁, h₁₂, h₂₁, h₂₂⟩

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