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
f : realMixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| * f (↑(polarCoordReal K).symm x)

Tactic:
refine setLIntegral_congr_fun (polarCoordReal K).open_target.measurableSet (fun x hx ↦ ?_)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : realMixedSpace K → ℝ≥0∞
x : realMixedSpace K
hx : x ∈ (polarCoordReal K).target
⊢ (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| * f (↑(polarCoordReal K).symm x)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = ↑x
⊢ (algebraMap (𝓞 ↥K⁺) K) y ∈ K⁺

Tactic:
IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMap.target = Set.univ.pi fun x ↦ Set.Ioi 0

Tactic:
by
  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph,
    PartialEquiv.pi_target, expMap_single]

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
⊢ 0 < p - 1

Tactic:
grind [hp.out.one_lt]

Goal state after:
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 𝒑
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
let ζₚ := ζ ^ m

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
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
⊢ (galEquivZMod n K).mapSubgroup (stabilizer Gal(K/ℚ) P) = Subgroup.zpowers (ZMod.unitOfCoprime p hn)

Tactic:
by
  classical
  have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
  apply SetLike.ext'
  refine Set.eq_of_subset_of_card_le ?_ ?_
  · rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ
  · replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]
    change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)
    rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)}),
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime, inertiaDegIn_eq_of_not_dvd p K hn]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ 0 < ‖↑k.factorial‖

Tactic:
simpa using k.factorial_ne_zero

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : x' - y' = 0
⊢ 0 < embedding ↑γ

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : ¬x' - y' = 0
⊢ exp (-padicValRat p (x' - y')) < embedding ↑γ

Tactic:
· simp only [exp_neg]
        exact embedding_unit_pos _

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : ¬x' - y' = 0
⊢ exp (-padicValRat p (x' - y')) < embedding ↑γ
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
g : X → Fin n
hg : ∀ (x : X), (fun i ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun i ↦ x ∈ E i) y → y = g x
h_ex : ∀ (i : Fin n), ∃ x, x ∈ E i
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

Tactic:
choose r hr using h_ex

Goal state after:
X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
g : X → Fin n
hg : ∀ (x : X), (fun i ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun i ↦ x ∈ E i) y → y = g x
r : Fin n → X
hr : ∀ (i : Fin n), r i ∈ E i
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁸ : Field K
inst✝²⁷ : Field L
inst✝²⁶ : Algebra K L
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²² : P.LiesOver p
inst✝²¹ : FiniteDimensional K L
inst✝²⁰ : MulSemiringAction Gal(L/K) B
inst✝¹⁹ : IsGaloisGroup Gal(L/K) A B
inst✝¹⁸ : IsDedekindDomain A
inst✝¹⁷ : IsDedekindDomain B
inst✝¹⁶ : Module.Finite A B
inst✝¹⁵ : Module.IsTorsionFree A B
inst✝¹⁴ : Ring.HasFiniteQuotients A
inst✝¹³ : P.IsMaximal
D : Type u_5
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
⊢ Module.finrank D E = p.inertiaDegIn B

Tactic:
by
  have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
  have := Module.finrank_mul_finrank K D E
  rwa [IsInertiaField.rank_right A K L P E hp, IsDecompositionField.rank_right A K L P D hp,
    mul_right_inj'] at this
  exact IsDedekindDomain.primesOver_ncard_ne_zero p B

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

Goal state before:
pp: case inr
A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : Ideal.span {x} ≠ ⊥
⊢ ↑(v.asIdeal.ramificationIdx' w.asIdeal) * emultiplicity v.asIdeal (Ideal.span {x}) =
    ↑(v.asIdeal.ramificationIdx' w.asIdeal) * ↑(multiplicity v.asIdeal (Ideal.span {x}))

Tactic:
(FiniteMultiplicity.of_prime_left v.prime hx).emultiplicity_eq_multiplicity

Goal state after:
case inr
A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : Ideal.span {x} ≠ ⊥
⊢ ↑(v.asIdeal.ramificationIdx' w.asIdeal) * ↑(multiplicity v.asIdeal (Ideal.span {x})) =
    ↑(v.asIdeal.ramificationIdx' w.asIdeal) * ↑(multiplicity v.asIdeal (Ideal.span {x}))
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
ha : ¬(Polynomial.aeval a) F = 0
⊢ ∃ z,
    (Polynomial.aeval z) F = 0 ∧
      ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ∧
        ‖(Polynomial.aeval z) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ∧
          ∀ (z' : ℤ_[p]),
            (Polynomial.aeval z') F = 0 → ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ → z' = z

Tactic:
exact ⟨soln_gen hnorm, eval_soln hnorm,
      soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z => soln_unique hnorm ha z⟩

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

Goal state before:
pp: case inr
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
f : K⟮X⟯
hf : f ≠ 0
hlt' : 1 < (inftyValuation K) X
⊢ v f < 1 ↔ (inftyValuation K) f < 1

Tactic:
valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt hf,

Goal state after:
case inr
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
f : K⟮X⟯
hf : f ≠ 0
hlt' : 1 < (inftyValuation K) X
⊢ v X ^ f.intDegree < 1 ↔ (inftyValuation K) f < 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d =
    ∑ x ∈ s.prodPrimes.divisors, (s.totalMass * (muPlus x * s.nu x) + muPlus x * rem x)

Tactic:
congr with d

Goal state after:
case e_f
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
⊢ muPlus d * multSum d = s.totalMass * (muPlus d * s.nu d) + muPlus d * rem d
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d ∈ n.divisors, ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

Tactic:
congr! 1 with d hd

Goal state after:
case a
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∈ n.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d ∈ n.divisors, ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

Tactic:
by
  congr! 1 with d hd
  rw [mem_divisors] at hd
  suffices ∀ d1 d2, (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2) by
    simp_rw [← Nat.divisors_filter_dvd_of_dvd hd.2 hd.1, sum_filter, ite_sum_zero, ← ite_and, this]
  simp +contextual [← and_assoc, Nat.dvd_lcm_left, Nat.dvd_lcm_right]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg.a.a
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ weights d2 * weights d1 = ∑ x ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0

Tactic:
rw [sum_ite_eq_of_mem', mul_comm]

Goal state after:
case neg.a.a.h
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∈ n.divisors
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inr.f
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer ↑pi
⊢ v (↑πᵥ ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors) / v ((algebraMap K[X] K⟮X⟯) q) ≤
      1 ↔
    (exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors))⁻¹ *
        exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {q})).factors) ≤
      1

Tactic:
valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq0

Goal state after:
case inr.f
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer ↑pi
⊢ v (↑πᵥ ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors) /
        v (↑πᵥ ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {q})).factors) ≤
      1 ↔
    (exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors))⁻¹ *
        exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {q})).factors) ≤
      1
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: case mk
y : ℤ[i]
re✝ im✝ : ℤ
⊢ toComplex { re := re✝, im := im✝ } = toComplex y ↔ { re := re✝, im := im✝ } = y

Tactic:
cases y

Goal state after:
case mk.mk
re✝¹ im✝¹ re✝ im✝ : ℤ
⊢ toComplex { re := re✝¹, im := im✝¹ } = toComplex { re := re✝, im := im✝ } ↔
    { re := re✝¹, im := im✝¹ } = { re := re✝, im := im✝ }
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ 0 < norm x ↔ x ≠ 0

Tactic:
rw [lt_iff_le_and_ne, Ne, eq_comm, norm_eq_zero]

Goal state after:
x : ℤ[i]
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case mk
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.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h :
  ↑((p.powQuotSuccInclusion P i) ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z, hz✝⟩) =
    (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)
⊢ x - y ∈ P

Tactic:
rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.Quotient.quot_mk_eq_mk,
        Ideal.Quotient.mk_eq_mk, ← map_sub, Ideal.Quotient.eq, ← mul_sub] at h

Goal state after:
case mk
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.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
x✝ : S ⧸ P
x : S
y✝ : S ⧸ P
y : S
Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)
val✝ : S ⧸ P ^ e
z : S
hz✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))
hz : z ∈ P ^ (i + 1)
h : z - a * (x - y) ∈ P ^ e
⊢ x - y ∈ P
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
h : Liouville x
⊢ Irrational x

Tactic:
rintro ⟨⟨a, b, bN0, cop⟩, rfl⟩

Goal state after:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville ↑{ num := a, den := b, den_nz := bN0, reduced := cop }
⊢ False
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case neg
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
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)

Tactic:
have : j z a ∈ closedBall α ε := by
      refine mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))
      exact (le_div_iff₀ me0).mpr (not_le.mp dm1).le

Goal state after:
case neg
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
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |(-eval (↑z / (↑a + 1)) fR)|

Tactic:
abs_neg

Goal state after:
case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |eval (↑z / (↑a + 1)) fR|
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: n : ℕ
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

Tactic:
induction n using Nat.recOnMul with
  | zero => exact ⟨0, 0, 0, 0, rfl⟩
  | one => exact ⟨1, 0, 0, 0, rfl⟩
  | prime p hp => exact hp.sum_four_squares
  | mul m n hm hn =>
    rcases hm with ⟨a, b, c, d, rfl⟩
    rcases hn with ⟨w, x, y, z, rfl⟩
    exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩

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

Goal state before:
pp: case hbc
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 + 1) ^ r ≤ ↑b ^ r

Tactic:
rw [one_add_one_eq_two]

Goal state after:
case hbc
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
⊢ 2 ^ r ≤ ↑b ^ r
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x * ↑r - ↑(r.num * m) / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p

Tactic:
rw [A, ← sub_mul, abs_mul]

Goal state after:
case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x - ↑m / ↑n| * |↑r| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 ≤ x2) (s ∩ {b | ¬b ≤ a}) ↔ Bounded (fun x1 x2 ↦ x1 ≤ x2) s

Tactic:
bounded_le_inter_not_le

Goal state after:
Module: Mathlib.Order.Bounds.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ lowerBounds (range u) = lowerBounds (⋃ i, s i)

Tactic:
simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: δ : ℕ → ℝ
x : UnitAddCircle
⊢ x ∈ addWellApproximable UnitAddCircle δ ↔ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite

Tactic:
simp only [mem_add_wellApproximable_iff, ← Nat.cofinite_eq_atTop, cofinite.blimsup_set_eq,
    mem_ofPred_eq]

Goal state after:
δ : ℕ → ℝ
x : UnitAddCircle
⊢ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}.Infinite ↔
    {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
h : ∀ j < i, e j = sInf s j
⊢ sInf s i ≤ e i

Tactic:
by
  rw [sInf_apply]
  exact sInf_le ⟨⟨e, he, h⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝² : CompleteLattice α
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hs : CountableSupClosed s
A : ι → α
hA : ∀ (n : ι), A n ∈ s
⊢ ⨆ n, A n ∈ s

Tactic:
let i₀ := Nonempty.some (α := ι) inferInstance

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝² : CompleteLattice α
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hs : CountableSupClosed s
A : ι → α
hA : ∀ (n : ι), A n ∈ s
i₀ : ι := ⋯.some
⊢ ⨆ n, A n ∈ s