mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case refine_2
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ 1 ≤
    emultiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))

Tactic:
exact Order.one_le_iff_pos.mpr <| emultiplicity_pos_of_dvd h₂.2.2

Goal state after:
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) → (toUnitHom χ) ((galEquivZMod n K) a) = 1

Tactic:
Units.ext_iff,

Goal state after:
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) → ↑((toUnitHom χ) ((galEquivZMod n K) a)) = ↑1
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ↑↑(toMixed K) x ∈ ↑(idealLattice K ((FractionalIdeal.mk0 K) J))) ∧
        (↑(toMixed K)).toEquiv x = x✝) ↔
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s

Tactic:
SetLike.mem_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ↑↑(toMixed K) x ∈ idealLattice K ((FractionalIdeal.mk0 K) J)) ∧
        (↑(toMixed K)).toEquiv x = x✝) ↔
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case hbc
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := ⋯
j : K →+* ℂ
a✝ : j ∈ univ
⊢ ‖(basisMatrix K)ᵀ⁻¹ i j‖ ≤ ‖(basisMatrix K)ᵀ⁻¹‖

Tactic:
exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
this : closedBall 0 1 ∈ 𝓝 0
⊢ LocallyCompactSpace ℚ_[p]

Tactic:
simp only [closedBall, dist_eq_norm_sub, sub_zero] at this

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : {y | ‖y‖ ≤ 1} ∈ 𝓝 0
⊢ LocallyCompactSpace ℚ_[p]
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ ↑n₀ * (↑(Nat.log n₀ m) + 1) ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)

Tactic:
gcongr
      exact natLog_le_logb ..

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
⊢ 0 < Fintype.card (α × (K →+* ℂ))

Tactic:
by rwa [hfinp]

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ 1 < ‖↑((algebraMap ℚ_[p] (PadicAlgCl p)) x)‖

Tactic:
simpa only [norm_extends']

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsDenseInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

Tactic:
by
  refine Padic.isUniformInducing_cast_withVal.isDenseInducing ?_
  intro
  -- nhds_discrete causes timeouts on TC search
  simpa [-nhds_discrete] using Padic.denseRange_ratCast p _

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < (a * b).x

Tactic:
simp only [x_mul]

Goal state after:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < a.x * b.x + d * (a.y * b.y)
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']; exact y_mul_pos hax hay (x_pow_pos hax _) ih

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ Int.negSucc n).x

Tactic:
rw [zpow_negSucc]

Goal state after:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ (n + 1))⁻¹.x
Module: Mathlib.NumberTheory.Pell

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

Tactic:
rw [zpow_negSucc]

Goal state after:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1))⁻¹.y.sign = (Int.negSucc n).sign
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : n ≤ m
⊢ (a ^ n).y ≤ (a ^ m).y

Tactic:
exact h.y_strictMono.monotone H

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 : x ≠ 0
⊢ exp (-↑(multiplicity v.asIdeal (Ideal.span {x}))) ^ v.asIdeal.ramificationIdx' w.asIdeal =
    exp (-↑(multiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x}))))

Tactic:
exp_neg,

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 : x ≠ 0
⊢ (exp ↑(multiplicity v.asIdeal (Ideal.span {x})))⁻¹ ^ v.asIdeal.ramificationIdx' w.asIdeal =
    exp (-↑(multiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x}))))
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 : x ≠ 0
⊢ (exp ↑(multiplicity v.asIdeal (Ideal.span {x})))⁻¹ ^ v.asIdeal.ramificationIdx' w.asIdeal =
    exp (-↑(multiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x}))))

Tactic:
exp_neg,

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 : x ≠ 0
⊢ (exp ↑(multiplicity v.asIdeal (Ideal.span {x})))⁻¹ ^ v.asIdeal.ramificationIdx' w.asIdeal =
    (exp ↑(multiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x}))))⁻¹
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ v ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    v X ^ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).intDegree

Tactic:
rw [intDegree_div (by grind only) (by grind only), v.map_div, zpow_sub₀ (ne_zero_of_lt hlt)]
    simp_rw [intDegree_polynomial, zpow_natCast, ← coePolynomial_eq_algebraMap]
    have hp : p ≠ 0 := by contrapose hf; simp [hf]
    rw [valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hp,
      valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hq]

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
m : ℤ
h₂ : beattySeq' s m = j
⊢ False

Tactic:
rw [beattySeq, Int.floor_eq_iff, ← div_le_iff₀ hrs.pos, ← lt_div_iff₀ hrs.pos] at h₁

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : beattySeq' s m = 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✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
this : v ((algebraMap K[X] K⟮X⟯) q) = 1
⊢ v ((algebraMap K[X] K⟮X⟯) π) ^ k * v ((algebraMap K[X] K⟮X⟯) q) =
    v ↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors

Tactic:
simp only [this, mul_one]
    congr
    exact (Ideal.count_associates_eq (irreducible_iff_prime.mp hπirr) hnq heq).symm

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
          (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|

Tactic:
rw [toComplex_re_div]

Goal state after:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑↑(round (toComplex x / toComplex y).re) +
          (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case refine_1
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ 0 ∣ n → 0 % 4 ≠ 3

Tactic:
exact fun _ => by simp

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case refine_2
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ 1 ∣ n → 1 % 4 ≠ 3

Tactic:
exact fun _ => by simp

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case pos
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : 2 ∣ m
⊢ False

Tactic:
rcases hm with ⟨m, rfl⟩
    rw [mul_pos_iff_of_pos_left two_pos] at hm₀
    have hm₂ : m < 2 * m := by simpa [two_mul]
    apply_fun (Nat.cast : ℕ → ℤ) at habcd
    push_cast [mul_assoc] at habcd
    obtain ⟨_, _, _, _, h⟩ := sum_four_squares_of_two_mul_sum_four_squares habcd
    exact hmin m hm₂ ⟨hm₂.trans hmp, hm₀, _, _, _, _, natAbs_iff.2 h⟩

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

Goal state before:
pp: f : ℂ[X]
s : ℂ
⊢ P f s = -(cexp s * (cexp (-s) * eval s (sumIDeriv f))) + cexp s * eval 0 (sumIDeriv f)

Tactic:
exp_neg,

Goal state after:
f : ℂ[X]
s : ℂ
⊢ P f s = -(cexp s * ((cexp s)⁻¹ * eval s (sumIDeriv f))) + cexp s * eval 0 (sumIDeriv f)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case mk.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
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : S ∙ a ≤ P ^ i
a_notMem : ¬S ∙ a ≤ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ x ∈ span {a} ⊔ P ^ (i + 1)

Tactic:
submodule_span_eq

Goal state after:
case mk.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
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : span {a} ≤ P ^ i
a_notMem : ¬span {a} ≤ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ x ∈ span {a} ⊔ P ^ (i + 1)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case mk.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
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : span {a} ≤ P ^ i
a_notMem : ¬span {a} ≤ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
hspan0 : span {a} ≠ ⊥
⊢ x ∈ P ^ min i (i + 1)

Tactic:
min_eq_left i.le_succ

Goal state after:
case mk.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
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : span {a} ≤ P ^ i
a_notMem : ¬span {a} ≤ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
hspan0 : span {a} ≠ ⊥
⊢ x ∈ P ^ i
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
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
hP : P ∈ IsDedekindDomain.primesOverFinset p S
⊢ p.inertiaDeg' P ≤ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx' P * p.inertiaDeg' P

Tactic:
← Finset.add_sum_erase _ _ hP

Goal state after:
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p ≠ ⊥
hP : P ∈ IsDedekindDomain.primesOverFinset p S
⊢ p.inertiaDeg' P ≤
    p.ramificationIdx' P * p.inertiaDeg' P +
      ∑ x ∈ (IsDedekindDomain.primesOverFinset p S).erase P, p.ramificationIdx' x * p.inertiaDeg' x
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : ¬p = ⊥
hP : P ∈ IsDedekindDomain.primesOverFinset p S
⊢ p.ramificationIdx' P ≤ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx' P * p.inertiaDeg' P

Tactic:
← Finset.add_sum_erase _ _ hP

Goal state after:
case neg
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : ¬p = ⊥
hP : P ∈ IsDedekindDomain.primesOverFinset p S
⊢ p.ramificationIdx' P ≤
    p.ramificationIdx' P * p.inertiaDeg' P +
      ∑ x ∈ (IsDedekindDomain.primesOverFinset p S).erase P, p.ramificationIdx' x * p.inertiaDeg' x
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
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : IsLocalRing S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
⊢ p.ramificationIdx' (IsLocalRing.maximalIdeal S) * p.inertiaDeg' (IsLocalRing.maximalIdeal S) = finrank K L

Tactic:
have := FaithfulSMul.of_field_isFractionRing R S K L
  simp_rw [← sum_ramification_inertia S K L hp0, IsLocalRing.primesOverFinset_eq S hp0,
    Finset.sum_singleton]

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

Goal state before:
pp: x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
⊢ x ∈
    ⋃ m,
      (fun x ↦ x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

Tactic:
rcases exists_nat_one_div_lt (sub_pos.2 hp) with ⟨n, hn⟩

Goal state after:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 1 / (↑n + 1) < p - 2
⊢ x ∈
    ⋃ m,
      (fun x ↦ x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x)

Tactic:
by
  rw [mul_comm]; exact h.mul_nat hn

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b

Tactic:
refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩

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

case refine_3.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ (↑(Units.mk0 ↑b ?refine_3.refine_1)).val = b
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:
rw [sInf_apply]
  exact sInf_le ⟨⟨e, he, h⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L M : CompleteSublattice α
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ } =
    (fun L ↦ L.carrier) M
⊢ { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ } = M

Tactic:
cases M

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice✝¹ : Sublattice α
sSupClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sSup s ∈ toSublattice✝¹.carrier
sInfClosed'✝¹ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝¹.carrier → sInf s ∈ toSublattice✝¹.carrier
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝¹, sSupClosed' := sSupClosed'✝¹, sInfClosed' := sInfClosed'✝¹ } =
    (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ }
⊢ { toSublattice := toSublattice✝¹, sSupClosed' := sSupClosed'✝¹, sInfClosed' := sInfClosed'✝¹ } =
    { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ }
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ sSup {x | ∃ s ∈ S, ↑s = x} = ⨆ N ∈ S, ↑N

Tactic:
← Set.image,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ sSup (Subtype.val '' S) = ⨆ N ∈ S, ↑N
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ sInf {x | ∃ s ∈ S, ↑s = x} = ⨅ N ∈ S, ↑N

Tactic:
← Set.image,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ sInf (Subtype.val '' S) = ⨅ N ∈ S, ↑N
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ ↑(iInf f) = ⨅ i, ↑(f i)

Tactic:
by
  rw [iInf, coe_sInf', iInf_range]

Goal state after: