mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = pB.gen ^ 1

Tactic:
powerBasis_gen hPirr.ne_zero,

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ root P ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = root P ^ 1
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
key : ↑n = ∑ i ∈ range n, (1 - ζ ^ i)
⊢ ζ - 1 ∣ ∑ i ∈ range n, (1 - ζ ^ i)

Tactic:
refine Finset.dvd_sum fun i _ ↦ ?_

Goal state after:
n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
key : ↑n = ∑ i ∈ range n, (1 - ζ ^ i)
i : ℕ
x✝ : i ∈ range n
⊢ ζ - 1 ∣ 1 - ζ ^ i
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : (Quotient.mk I) ↑ζ = ↑1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := ↑↑ζ
hμ : IsPrimitiveRoot μ t
⊢ False

Tactic:
Units.val_one

Goal state after:
K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : (Quotient.mk I) ↑ζ = 1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := ↑↑ζ
hμ : IsPrimitiveRoot μ t
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
w : InfinitePlace K
h : w = w₀
⊢ Real.log c ∈ Set.Iic 0

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ y w ∈ Set.Icc 0 1

Tactic:
· refine Real.log_nonpos hc.1 hc.2

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ y w ∈ Set.Icc 0 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (closure (normLeOne K) \ interior (normLeOne K)) = 0

Tactic:
measure_sdiff,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (closure (normLeOne K)) - volume (interior (normLeOne K)) = 0

case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ interior (normLeOne K) ⊆ closure (normLeOne K)

case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ NullMeasurableSet (interior (normLeOne K)) volume

case h_fin
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (interior (normLeOne K)) ≠ ∞
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
⊢ q ≠ ⊥ → ∀ (x : q.IsPrime), IsDiscreteValuationRing (Localization.AtPrime q)

Tactic:
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 ≠ ⊥
⊢ ∀ (x : q.IsPrime), IsDiscreteValuationRing (Localization.AtPrime q)
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
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝³ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ (σ : Gal(K/ℚ)), (∀ x ∈ F, σ x = x) → χ ↑((galEquivZMod n K) σ) = 1) ↔
    ∀ (a : Gal(K/ℚ)), (∀ x ∈ F, a x = x) → χ ↑((galEquivZMod n K) a) = ↑1

Tactic:
Units.val_one

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

Goal state before:
pp: case e'_5
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
⊢ π ^ nrComplexPlaces K * regulator K * (↑(torsionOrder K))⁻¹ * (√|↑(discr K)|)⁻¹ * 2 ^ nrRealPlaces K *
      2 ^ nrComplexPlaces K =
    π ^ nrComplexPlaces K * regulator K * (↑(torsionOrder K))⁻¹ * (√|↑(discr K)|)⁻¹ * ↑(absNorm ↑J) *
          (↑(absNorm ↑J))⁻¹ *
        2 ^ nrRealPlaces K *
      2 ^ nrComplexPlaces K

Tactic:
rw [mul_inv_cancel_right₀ h₃]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
⊢ 0 ≤ s →
    ∑ c, ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = c }) / s = ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s

Tactic:
hs

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
hs : 0 ≤ s
⊢ ∑ c, ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = c }) / s = ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this :
  Tendsto (fun x ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ x }) / x + x⁻¹) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))
s : ℝ
⊢ 0 ≤ s → ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s + s⁻¹ = ↑(Nat.card { I // ↑(absNorm I) ≤ s }) / s

Tactic:
hs

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this :
  Tendsto (fun x ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ x }) / x + x⁻¹) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))
s : ℝ
hs : 0 ≤ s
⊢ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s + s⁻¹ = ↑(Nat.card { I // ↑(absNorm I) ≤ s }) / s
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
⊢ s ∈ 𝓝 1 → ∃ a, ∀ (b : ℕ × ℕ), a ≤ b → f b.2 / f b.1 ∈ s

Tactic:
hs

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
⊢ ∃ a, ∀ (b : ℕ × ℕ), a ≤ b → f b.2 / f b.1 ∈ s
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_6
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * supOfBasis K ≤ c₂ K * A

Tactic:
rw [mul_right_comm, c₂]
      gcongr
      exacts [supOfBasis_nonneg _, le_max_right ..]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬real.IsEquiv (padic p)

Tactic:
by
  rw [isEquiv_iff_exists_rpow_eq]
  rintro ⟨c, hc₀, hc⟩
  apply_fun (· 2) at hc
  simp only [real_eq_abs, abs_ofNat, cast_ofNat] at hc
  exact ((padic_le_one p 2).trans_lt <| one_lt_rpow one_lt_two hc₀).ne' hc

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖f ↑n‖ ≤ ‖↑k.factorial‖

Tactic:
f,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖Polynomial.eval (↑n) (ascPochhammer ℤ_[p] k)‖ ≤ ‖↑k.factorial‖
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
p : Nat.Primes
⊢ Ideal.span {↑↑p} ≠ ⊥

Tactic:
simp [p.2.ne_zero]

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ (fun p ↦
        have h := ⋯;
        HeightOneSpectrum.ofPrime h)
      ((fun v ↦ ⟨natGenerator v, ⋯⟩) v) =
    v

Tactic:
by
    simp only [Ideal.map_symm]
    congr
    rw [← v.asIdeal.comap_map_of_bijective _ (IsIntegralClosure.intEquiv R).bijective,
      ← span_natGenerator]

Goal state after:
Module: Mathlib.NumberTheory.PowModTotient

Goal state before:
pp: x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ k % n = x ^ (k % φ n) % n

Tactic:
rw [← div_add_mod' k (φ n), add_comm, pow_add_mul_totient_mod_eq hn h, add_mul_mod_self_right,
    mod_mod k (φ n)]

Goal state after:
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
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Tactic:
have hm₀ : m ≠ 0 := by
    rintro rfl
    obtain ⟨q, hq⟩ := hm.nonempty
    rw [mem_ofPred, sub_eq_zero, mul_comm] at hq
    obtain ⟨a, ha⟩ := (Int.pow_dvd_pow_iff two_ne_zero).mp ⟨d, hq⟩
    rw [ha, mul_pow, mul_right_inj' (pow_pos (Int.natCast_pos.mpr q.pos) 2).ne'] at hq
    exact hd ⟨a, sq a ▸ hq.symm⟩

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
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : mk x y prop = 1
⊢ False

Tactic:
apply_fun Solution₁.y at H

Goal state after:
case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : (mk x y prop).y = Solution₁.y 1
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : mk x y prop = -1
⊢ False

Tactic:
apply_fun Solution₁.y at H

Goal state after:
case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : (mk x y prop).y = (-1).y
⊢ False
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✝²⁸ : Algebra A K
inst✝²⁷ : IsFractionRing A K
inst✝²⁶ : Algebra A L
inst✝²⁵ : IsScalarTower A K L
inst✝²⁴ : Algebra B L
inst✝²³ : IsScalarTower A B L
inst✝²² : IsFractionRing B L
inst✝²¹ : MulSemiringAction Gal(L/K) B
inst✝²⁰ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝¹⁹ : Field D
inst✝¹⁸ : Algebra D L
inst✝¹⁷ : IsDecompositionField K L P D
inst✝¹⁶ : CommRing 𝓞D
inst✝¹⁵ : Algebra 𝓞D D
inst✝¹⁴ : IsFractionRing 𝓞D D
inst✝¹³ : Algebra 𝓞D B
inst✝¹² : Algebra 𝓞D L
inst✝¹¹ : IsScalarTower 𝓞D D L
inst✝¹⁰ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
inst✝⁹ : IsGalois K L
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Algebra A 𝓞D
inst✝³ : Module.Finite A 𝓞D
inst✝² : IsScalarTower A 𝓞D B
inst✝¹ : IsDedekindDomain 𝓞D
inst✝ : 𝓟D.LiesOver p
hp : p ≠ ⊥
inst₁ : Module.Finite 𝓞D B
inst₂ : Module.IsTorsionFree 𝓞D B
inst₃ : Module.IsTorsionFree A 𝓞D
inst₄ : IsGaloisGroup Gal(L/K) A B
⊢ Module.Finite 𝓞D B ∧
    Module.IsTorsionFree 𝓞D B ∧
      Module.IsTorsionFree A 𝓞D ∧ IsGaloisGroup Gal(L/K) A B ∧ IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B ∧ 𝓟D ≠ ⊥

Tactic:
have inst₅ : IsGaloisGroup (stabilizer Gal(L/K) P) 𝓞D B := .of_isFractionRing _ _ _ D L

Goal state after:
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✝²⁸ : Algebra A K
inst✝²⁷ : IsFractionRing A K
inst✝²⁶ : Algebra A L
inst✝²⁵ : IsScalarTower A K L
inst✝²⁴ : Algebra B L
inst✝²³ : IsScalarTower A B L
inst✝²² : IsFractionRing B L
inst✝²¹ : MulSemiringAction Gal(L/K) B
inst✝²⁰ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝¹⁹ : Field D
inst✝¹⁸ : Algebra D L
inst✝¹⁷ : IsDecompositionField K L P D
inst✝¹⁶ : CommRing 𝓞D
inst✝¹⁵ : Algebra 𝓞D D
inst✝¹⁴ : IsFractionRing 𝓞D D
inst✝¹³ : Algebra 𝓞D B
inst✝¹² : Algebra 𝓞D L
inst✝¹¹ : IsScalarTower 𝓞D D L
inst✝¹⁰ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
inst✝⁹ : IsGalois K L
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Algebra A 𝓞D
inst✝³ : Module.Finite A 𝓞D
inst✝² : IsScalarTower A 𝓞D B
inst✝¹ : IsDedekindDomain 𝓞D
inst✝ : 𝓟D.LiesOver p
hp : p ≠ ⊥
inst₁ : Module.Finite 𝓞D B
inst₂ : Module.IsTorsionFree 𝓞D B
inst₃ : Module.IsTorsionFree A 𝓞D
inst₄ : IsGaloisGroup Gal(L/K) A B
inst₅ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
⊢ Module.Finite 𝓞D B ∧
    Module.IsTorsionFree 𝓞D B ∧
      Module.IsTorsionFree A 𝓞D ∧ IsGaloisGroup Gal(L/K) A B ∧ IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B ∧ 𝓟D ≠ ⊥
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
s✝ : ℝ
⊢ s✝ ≥ 0 → (j ∈ {x | ∃ k > 0, beattySeq s✝ k = x} ↔ j ∈ {x | ∃ k, beattySeq s✝ k = x})

Tactic:
hs

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
s✝ : ℝ
hs : s✝ ≥ 0
⊢ j ∈ {x | ∃ k > 0, beattySeq s✝ k = x} ↔ j ∈ {x | ∃ k, beattySeq s✝ k = x}
Module: Mathlib.NumberTheory.Rayleigh

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

Tactic:
hs

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
s✝ : ℝ
hs : s✝ ≥ 0
⊢ j ∈ {x | ∃ k > 0, beattySeq' s✝ k = x} ↔ j ∈ {x | ∃ k, beattySeq' s✝ k = x}
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case hg
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
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
⊢ v ↑πᵥ < ↑1

Tactic:
Units.val_one

Goal state after:
case hg
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
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
⊢ v ↑πᵥ < 1
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inl
hp : Fact (Nat.Prime 2)
⊢ ∃ a b k, 0 < k ∧ k < 2 ∧ a ^ 2 + b ^ 2 + 1 = k * 2

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
· use 1, 0, 1; simp

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ ↑(f 0) ^ 2 + ↑(f 1) ^ 2 + ↑(f 2) ^ 2 + ↑(f 3) ^ 2 = 0

Tactic:
rw [← @zero_mul (ZMod 2) _ m, ← show ((2 : ℤ) : ZMod 2) = 0 from rfl, ← Int.cast_mul, ← h]
    simp only [Int.cast_add, Int.cast_pow]
    rfl

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
⊢ p % 4 ≠ 3

Tactic:
have : Fact p.Prime := ⟨Nat.prime_of_mem_primeFactors hp⟩

Goal state after:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
this : Fact (Prime p)
⊢ p % 4 ≠ 3
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine congr_arg Submodule.Quotient.mk ?_

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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 : z - a * (x - y) ∈ P ^ e
⊢ x - y ∈ P

Tactic:
exact
        (Ideal.IsPrime.mem_pow_mul _
              ((Submodule.sub_mem_iff_right _ hz).mp (Pe_le_Pi1 h))).resolve_left
          a_notMem

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
⊢ ∃ n,
    ¬↑p ∣ n ∧
      ∃ gp,
        gp.natDegree ≤ p * f.natDegree - 1 ∧
          ∀ {r : ℂ},
            r ∈ f.aroots ℂ →
              ‖↑n * cexp r - ↑p * (aeval r) gp‖ ≤
                (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then
                      (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
                    else 0) ^
                    p /
                  ↑(p - 1)!

Tactic:
obtain ⟨gp', -, h'⟩ := eval_sumIDeriv_of_pos (X ^ (p - 1) * f ^ p) prime_p.pos

Goal state after:
case h
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' :
  ∀ (r : ℤ) {p' : ℤ[X]},
    X ^ (p - 1) * f ^ p = (X - C r) ^ (p - 1) * p' →
      eval r (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval r p' + p ! • eval r gp'
⊢ ∃ n,
    ¬↑p ∣ n ∧
      ∃ gp,
        gp.natDegree ≤ p * f.natDegree - 1 ∧
          ∀ {r : ℂ},
            r ∈ f.aroots ℂ →
              ‖↑n * cexp r - ↑p * (aeval r) gp‖ ≤
                (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then
                      (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
                    else 0) ^
                    p /
                  ↑(p - 1)!
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
P : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
let : NeZero e := ⟨he⟩
  have := rank_pow_quot p P hP0 0 (Nat.zero_le e)
  rw [pow_zero, Nat.sub_zero, Ideal.one_eq_top, Ideal.map_top] at this
  exact (rank_top (R ⧸ p) _).symm.trans this

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

Goal state before:
pp: p x : ℝ
m : ℤ
hm : m ≠ 0
⊢ LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x

Tactic:
by
  rw [← Rat.cast_intCast, mul_rat_iff (Int.cast_ne_zero.2 hm)]

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ -↑1 = -1

Tactic:
Units.val_one

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

Goal state before:
pp: r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
this : 1 - r ≠ 0
⊢ (↑b + 1) * (2 / ↑b ^ r) = 2 * (↑b ^ (1 - r) + ↑b ^ (-r))

Tactic:
simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' this, mul_add,
          mul_left_comm]

Goal state after:
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

Goal state before:
pp: J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
⊢ (ConcreteCategory.hom m) t =
    (ConcreteCategory.hom
        { toFun := fun t j ↦ (ConcreteCategory.hom (s.π.app { as := j })) t, monotone' := ⋯, map_ωSup' := ⋯ })
      t

Tactic:
funext j

Goal state after:
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ (product f).π.app j = s.π.app j
t : s.pt.carrier
j : J
⊢ (ConcreteCategory.hom m) t j =
    (ConcreteCategory.hom
        { toFun := fun t j ↦ (ConcreteCategory.hom (s.π.app { as := j })) t, monotone' := ⋯, map_ωSup' := ⋯ })
      t j