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)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝¹ i] (A i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
set S := {i | IsCompact (A i) ∧ x i ∈ A i}
    have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr (hAcompact.and x.2)
    have hSx : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi.2
    have hSA : ∀ i ∈ S, IsCompact (A i) := fun i hi ↦ hi.1
    have := weaklyLocallyCompactSpace_of_principal hS hSA
    rcases exists_inclusion_eq_of_eventually R A hS hSx with ⟨x', hxx'⟩
    rw [← hxx', nhds_eq_map_inclusion hAopen]
    rcases exists_compact_mem_nhds x' with ⟨K, K_compact, hK⟩
    exact ⟨inclusion R A hS '' K, K_compact.image (continuous_inclusion hS), image_mem_map hK⟩

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst✝¹ : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst✝¹ i] (A' i)
X : Type u_4
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst✝] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
hU : cofinite ≤ 𝓟 (S ∩ T)
⊢ Continuous[instTopologicalSpaceProd, inst✝] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))

Tactic:
have hSU : 𝓟 U ≤ 𝓟 S := principal_mono.mpr inter_subset_left

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst✝¹ : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst✝¹ i] (A' i)
X : Type u_4
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst✝] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
hU : cofinite ≤ 𝓟 (S ∩ T)
hSU : 𝓟 U ≤ 𝓟 S
⊢ Continuous[instTopologicalSpaceProd, inst✝] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
⊢ s.FiniteIndex ↔ (s ⊔ torsion K).FiniteIndex

Tactic:
refine ⟨fun h ↦ Subgroup.finiteIndex_of_le le_sup_left, fun h ↦ ?_⟩
  rw [Subgroup.finiteIndex_iff, ← Subgroup.relIndex_mul_index (le_sup_left : s ≤ s ⊔ torsion K)]
  refine Nat.mul_ne_zero ?_ (Subgroup.finiteIndex_iff.mp h)
  rw [Subgroup.relIndex_sup_left]
  exact Subgroup.FiniteIndex.index_ne_zero

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
⊢ IsDiscrete ↑(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))))

Tactic:
refine (inferInstance : DiscreteTopology (unitLattice K)).isDiscrete.mono ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
⊢ ↑(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i)))) ⊆ ↑(unitLattice K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
⊢ x ∈ normAtComplexPlaces '' A →
    x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0

Tactic:
rintro ⟨a, ha, rfl⟩
    refine ⟨?_, by simpa using h a⟩
    rw [Set.mem_preimage, ← hA, Set.mem_preimage, normAtComplexPlaces_mixedSpaceOfRealSpace (h a)]
    exact Set.mem_image_of_mem _ ha

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✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
v : (𝓞 ↥K⁺)ˣ
hv : (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
⊢ (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u

Tactic:
hv

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
v : (𝓞 ↥K⁺)ˣ
hv : (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
⊢ (algebraMap (𝓞 K) K) ↑u = (algebraMap (𝓞 K) K) ↑u
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ x ∈ normAtAllPlaces '' normLeOne K →
    x ∈
      ⇑mixedSpaceOfRealSpace ⁻¹'
              logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∩
            {x | ∀ (w : InfinitePlace K), 0 ≤ x w} ∩
          {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0} ∩
        {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}

Tactic:
rintro ⟨y, ⟨⟨h₁, h₂⟩, h₃⟩, rfl⟩

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈
    ⇑mixedSpaceOfRealSpace ⁻¹'
            logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∩
          {x | ∀ (w : InfinitePlace K), 0 ≤ x w} ∩
        {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0} ∩
      {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
⊢ False

Tactic:
have h' : E ⊔ (maximalRealSubfield K) = ⊤ := by
    let L : IntermediateField E K := (E ⊔ (maximalRealSubfield K)).toIntermediateField
      (fun x ↦ (le_sup_left (a := E)) x.prop)
    have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K
      (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_
    · simpa [L] using congr_arg IntermediateField.toSubfield this
    · contrapose h
      rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h
      rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot]
      aesop

Goal state after:
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ↑expMap ((completeBasis K) w₀) = fun x ↦ Real.exp 1

Tactic:
ext
  simp_rw [expMap_apply, completeBasis_apply_of_eq, inv_mul_cancel₀ mult_coe_ne_zero]

Goal state after:
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]
    rw [if_neg i.prop]

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₀ }
| 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
⊢ |LinearMap.det ↑(fderiv_expMap ((completeBasis K).equivFun.symm x) ∘SL ↑(completeBasis K).equivFunL.symm)| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
toLinearMap_comp,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |LinearMap.det (↑(fderiv_expMap ((completeBasis K).equivFun.symm x)) ∘ₗ ↑↑(completeBasis K).equivFunL.symm)| =
    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
x : realSpace K
⊢ |LinearMap.det
          (LinearMap.pi fun i ↦
            ↑(smulRight 1 (deriv_expMap_single i ((completeBasis K).equivFun.symm x i)) ∘SL proj i)) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
toLinearMap_comp,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |LinearMap.det
          (LinearMap.pi fun i ↦
            ↑(smulRight 1 (deriv_expMap_single i ((completeBasis K).equivFun.symm x i))) ∘ₗ ↑(proj i)) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K
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))
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ P = span {hζ.toInteger - 1}

Tactic:
by
  have : P ∈ primesOver 𝒑 (𝓞 K) := ⟨hP₁, hP₂⟩
  have : span {hζ.toInteger - 1} ∈ primesOver 𝒑 (𝓞 K) :=
    ⟨isPrime_span_zeta_sub_one p k hζ, liesOver_span_zeta_sub_one p k hζ⟩
  have := ncard_primesOver_of_prime_pow p k K
  aesop

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
⊢ 𝒑.inertiaDegIn (𝓞 K) = 1

Tactic:
by
  rw [← pow_one p] at hK
  exact inertiaDegIn_eq_of_prime_pow p 0 K

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

Goal state before:
pp: case convert_4
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
⊢ MeasureTheory.volume (⇑(toMixed K) ⁻¹' frontier {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1}) = 0

Tactic:
(volumePreserving_toMixed K).measure_preimage
      measurableSet_frontier.nullMeasurableSet,

Goal state after:
case convert_4
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
⊢ MeasureTheory.volume (frontier {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1}) = 0
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‖) ^ m * (↑B + 1) ^ m = ((↑n * max 1 ‖A‖) ^ e) ^ (↑n - ↑m) * (↑B + 1) ^ m

Tactic:
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')

Goal state after:
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
⊢ 1 * f ↑p ^ k + 1 * f ↑m ^ k < 1

Tactic:
have hm₀ : 0 < f m := f.pos <| Nat.cast_ne_zero.mpr fun H ↦ hpm <| H ▸ dvd_zero p
    linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]

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
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
⊢ Fintype.card (α × (K →+* ℂ)) < Fintype.card (β × (K →+* ℂ))

Tactic:
by rwa [hfinp, hfinq]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
⊢ (a ^ n).y.sign = n.sign

Tactic:
by
  rcases n with ((_ | n) | n)
  · rfl
  · rw [Int.ofNat_eq_natCast, zpow_natCast]
    exact Int.sign_eq_one_of_pos (y_pow_succ_pos hax hay n)
  · rw [zpow_negSucc]
    exact Int.sign_eq_neg_one_of_neg (neg_neg_of_pos (y_pow_succ_pos hax hay n))

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x y : A
hy : y ∈ nonZeroDivisors A
⊢ (valuation K v) ((algebraMap A K) x / (algebraMap A K) y) ^ v.asIdeal.ramificationIdx' w.asIdeal =
    (valuation L w) ((algebraMap K L) ((algebraMap A K) x / (algebraMap A K) y))

Tactic:
simp [valuation_of_algebraMap, div_pow, ← IsScalarTower.algebraMap_apply A K L,
    IsScalarTower.algebraMap_apply A B L, intValuation_liesOver v w]

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hπᵥ : ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne = a * b
hb : ¬IsUnit b
⊢ 1 ≤ v ↑a

Tactic:
set πᵥ := degree_lt_wf.min _ hne

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
⊢ 1 ≤ v ↑a
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₂ : beattySeq' s m = j
⊢ False

Tactic:
beattySeq',

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

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
⊢ Irreducible (⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne)

Tactic:
set πᵥ := degree_lt_wf.min _ hne

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
⊢ Irreducible πᵥ
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j < ↑⌊(↑j + 1) / r⌋ * r
⊢ beattySeq' r ⌊(↑j + 1) / r⌋ = j

Tactic:
beattySeq',

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

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

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

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

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

Tactic:
· exact (Set.not_disjoint_iff.2 ⟨j, h₁, h₂⟩ (Beatty.no_collision hrs)).elim

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

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

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

Goal state before:
pp: case a.inr
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ 0 < beattySeq' s k

Tactic:
beattySeq',

Goal state after:
case a.inr
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ 0 < ⌈↑k * s⌉ - 1
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq' s✝ k = x}
k : ℤ
hj : 0 < beattySeq' s✝ k
hk : beattySeq' s✝ k = j
⊢ k > 0

Tactic:
beattySeq',

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq' s✝ k = x}
k : ℤ
hj : 0 < ⌈↑k * s✝⌉ - 1
hk : beattySeq' s✝ k = j
⊢ k > 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
l : ℕ
hl : l ∣ s.prodPrimes
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : Nat.Prime p
hp_dvd : p ∣ s.prodPrimes
⊢ 0 < 1 - s.nu p

Tactic:
linarith only [s.nu_lt_one_of_prime p hp_prime hp_dvd]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹ =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

Tactic:
have hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes :=
      (Nat.gcd_dvd_left d1 d2).trans (dvd_of_mem_divisors hd1)

Goal state after:
case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹ =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case a
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ (-(x • s)).re ≤ ‖s‖

Tactic:
simp only [Set.mem_Ioc] at hx
    apply (re_le_norm _).trans
    rw [norm_neg, norm_smul, Real.norm_of_nonneg hx.1.le]
    exact mul_le_of_le_one_left (norm_nonneg _) hx.2

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

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
rw [lt_div_iff₀' (pow_pos b0 _), pow_add, mul_assoc] at a1

Goal state after:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 1 / A ≤ ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
lift b to ℕ using zero_le_one.trans b1.le
    specialize h a b.pred
    rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ←
      div_le_iff₀ hA] at h
    exact Int.ofNat_lt.mp b1

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ↑b ≠ 0

Tactic:
intro h; apply hb.1; apply_fun val at h
      simpa only [val_cast_of_lt hb.right, val_zero] using h

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ b ∈ Ico 1 (p - 1).succ, ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b

Tactic:
intro b hb
    rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, Nat.add_one_sub_one, pos_iff_ne_zero] at hb
    refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩
    · intro h; apply hb.1; apply_fun val at h
      simpa only [val_cast_of_lt hb.right, val_zero] using h
    · simp only [val_cast_of_lt hb.right, Units.val_mk0]

Goal state after: