mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)
n : ℕ
⊢ 2 * Complex.cos (2 * ↑π * ↑a * (↑n + 1)) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t) =
    (cexp (2 * ↑π * I * ↑a * (↑n + 1)) + cexp (-(2 * ↑π * I * ↑a * (↑n + 1)))) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t)

Tactic:
rw [Complex.cos, mul_div_cancel₀ _ two_ne_zero]

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)
n : ℕ
⊢ (cexp (2 * ↑π * ↑a * (↑n + 1) * I) + cexp (-(2 * ↑π * ↑a * (↑n + 1)) * I)) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t) =
    (cexp (2 * ↑π * I * ↑a * (↑n + 1)) + cexp (-(2 * ↑π * I * ↑a * (↑n + 1)))) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case H
b : ℝ
⊢ ∃ p, 0 < p ∧ (fun x ↦ evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b
  refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩
  filter_upwards [eventually_gt_atTop 0] with t h
  simp [← (hasSum_int_evenKernel b h).tsum_eq, HurwitzKernelBounds.F_int, HurwitzKernelBounds.f_int]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: case e'_5
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (Complex.cos (2 * ↑π * ↑a * ↑n) + Complex.sin (2 * ↑π * ↑a * ↑n) * I) / ↑n ^ s =
    Complex.cos (2 * ↑π * ↑a * ↑n) / ↑n ^ s + I * (Complex.sin (2 * ↑π * ↑a * ↑n) / ↑n ^ s)

Tactic:
add_div,

Goal state after:
case e'_5
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ Complex.cos (2 * ↑π * ↑a * ↑n) / ↑n ^ s + Complex.sin (2 * ↑π * ↑a * ↑n) * I / ↑n ^ s =
    Complex.cos (2 * ↑π * ↑a * ↑n) / ↑n ^ s + I * (Complex.sin (2 * ↑π * ↑a * ↑n) / ↑n ^ s)
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
⊢ riemannZeta s = (s * completedRiemannZeta₀ s - 1 - s / (1 - s)) / (2 * ↑π ^ (-s / 2) * Gamma (s / 2 + 1))

Tactic:
by
  rcases eq_or_ne s 0 with rfl | hs
  · simp [riemannZeta_zero]
  · rw [riemannZeta_eq_completedRiemannZeta₀ hs, Gamma_add_one (s / 2) (by grind)]
    field

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ ↑(1 / 2) ∨ (if a = 0 then 1 else 0) = 0

Tactic:
refine Or.imp (fun h ↦ ?_) (fun ha ↦ ?_) hs'

Goal state after:
case refine_2.refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
h : s ≠ 1
⊢ s / 2 ≠ ↑(1 / 2)

case refine_2.refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
ha : a ≠ 0
⊢ (if a = 0 then 1 else 0) = 0
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : deriv (L 1) s = deriv riemannZeta s
⊢ L (fun n ↦ ↑(Λ n)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
by
    rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a b : UnitAddCircle
⊢ Differentiable ℂ fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s

Tactic:
by
  intro z
  rcases ne_or_eq z 1 with hz | rfl
  · exact (differentiableAt_hurwitzZetaEven a hz).sub (differentiableAt_hurwitzZetaEven b hz)
  · convert!
    (differentiableAt_hurwitzZetaEven_sub_one_div a).fun_sub
      (differentiableAt_hurwitzZetaEven_sub_one_div b) using
    2 with s
    abel

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm (I * J).num) / ↑|(Algebra.norm ℤ) ↑(I * J).den| =
    ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| * (↑(Ideal.absNorm J.num) / ↑|(Algebra.norm ℤ) ↑J.den|)

Tactic:
by
    rw [absNorm_div_norm_eq_absNorm_div_norm (I.den * J.den) (I.num * J.num) (by
        have : Algebra.linearMap R K = (IsScalarTower.toAlgHom R R K).toLinearMap := rfl
        rw [coe_mul, this, Submodule.map_mul, ← this, ← den_mul_self_eq_num, ← den_mul_self_eq_num]
        exact Submodule.mul_smul_mul_eq_smul_mul_smul _ _ _ _),
      Submonoid.coe_mul, map_mul, map_mul, Nat.cast_mul, div_mul_div_comm,
      Int.cast_abs, Int.cast_abs, Int.cast_abs, ← abs_mul, Int.cast_mul]

Goal state after:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_1
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
j : { x // x ∈ closure (id '' ↑K) } → ↑↑K.topologicalClosure := fun x ↦ ⟨↑x, ⋯⟩
⊢ DenseRange ι

Tactic:
convert!
      DenseRange.comp (Function.Surjective.denseRange _) (IsDenseEmbedding.id.subtype (· ∈ K)).dense
        (by fun_prop : Continuous j)

Goal state after:
case refine_1
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
j : { x // x ∈ closure (id '' ↑K) } → ↑↑K.topologicalClosure := fun x ↦ ⟨↑x, ⋯⟩
⊢ Function.Surjective j
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h :
  (match x✝¹ with
    | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩) =
    match x✝ with
    | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩
⊢ x✝¹ = x✝

pp: case e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ∃ a,
    (match a with
      | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩) =
      ⟨φ, hφ⟩

Tactic:
· rwa [Subtype.mk_eq_mk, ← Subtype.ext_iff, ← Subtype.ext_iff] at h

Goal state after:
case e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ∃ a,
    (match a with
      | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩) =
      ⟨φ, hφ⟩
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : (f ζ).im = 0
⊢ (f ζ).re = 1 ∨ (f ζ).re = -1

Tactic:
rw [← Complex.abs_re_eq_norm] at him

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : |(f ζ).re| = ‖f ζ‖
⊢ (f ζ).re = 1 ∨ (f ζ).re = -1
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case e'_4
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' = b / gcd a b

Tactic:
exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2}

Tactic:
simp_rw [abs_lt]
    refine Convex.inter ((convex_halfSpace_re_gt _).inter (convex_halfSpace_re_lt _))
      ((convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _))

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ↑(univ.sup' ⋯ fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) = univ.sup' ⋯ fun w ↦ (normAtPlace w) x

Tactic:
← NNReal.val_eq_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ↑(univ.sup' ⋯ fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) = univ.sup' ⋯ fun w ↦ (normAtPlace w) x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ Nat.card ↥(Stab w) = 1 ∨ Nat.card ↥(Stab w) = 2

Tactic:
← SetLike.coe_sort_coe,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ Nat.card ↑↑(Stab w) = 1 ∨ Nat.card ↑↑(Stab w) = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖)

Tactic:
convexBodySumFun_apply',

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-(∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖)) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < volume (convexBodyLT K f)
⊢ ∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)

Tactic:
by
  obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_lt K ↑1 h
  obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
  exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * ↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))

Tactic:
simp_rw [NNReal.coe_inv, NNReal.coe_div, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_div,
        coe_real_pi, NNReal.coe_ofNat, NNReal.coe_natCast]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ ((latticeBasis K).repr ((mixedEmbedding K) x)) i = ↑(((integralBasis K).repr x) i)

Tactic:
rw [← Basis.restrictScalars_repr_apply ℚ _ ⟨_, mem_rat_span_latticeBasis K x⟩, eq_ratCast,
    Rat.cast_inj]
  let f := (mixedEmbedding K).toRatAlgHom.toLinearMap.codRestrict _
    (fun x ↦ mem_rat_span_latticeBasis K x)
  suffices ((latticeBasis K).restrictScalars ℚ).repr.toLinearMap ∘ₗ f =
    (integralBasis K).repr.toLinearMap from DFunLike.congr_fun (LinearMap.congr_fun this x) i
  refine Basis.ext (integralBasis K) (fun i ↦ ?_)
  have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i := by
    apply Subtype.val_injective
    rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]
    rfl
  simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, this, Basis.repr_self]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I := Fintype.equivOfCardEq ⋯
⊢ ¬FractionalIdeal.absNorm ↑I = 0

Tactic:
FractionalIdeal.absNorm_eq_zero_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I := Fintype.equivOfCardEq ⋯
⊢ ¬↑I = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
inst✝ : NumberField K
⊢ ⋃ s, ⇑(negAt s) '' plusPart A =ᵐ[volume] A

Tactic:
nth_rewrite 2 [← iUnion_negAt_plusPart_union A hA]

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
inst✝ : NumberField K
⊢ ⋃ s, ⇑(negAt s) '' plusPart A =ᵐ[volume] (⋃ s, ⇑(negAt s) '' plusPart A) ∪ A ∩ ⋃ w, {x | x.1 w = 0}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ ‖‖x.1 ⟨w, hw⟩‖‖ = ‖x.1 ⟨w, hw⟩‖

Tactic:
norm_norm

Goal state after:
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: case intro.refine_2
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
h_eval : (aeval d) (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) q)) = 0
h_splits : (Polynomial.map (algebraMap A B) p).Splits
⊢ (Polynomial.map ((algebraMap K L).comp ((algebraMap (A ⧸ P) K).comp (algebraMap A (A ⧸ P)))) p).comp
      (C ((algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a))) * X) ≠
    0

Tactic:
exact mt (comp_C_mul_X_eq_zero_iff (by simpa)).mp (map_monic_ne_zero h_monic)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
⊢ IsUnramifiedAt R p

Tactic:
let p₀ : Ideal R := p.under R
  have : P.LiesOver p₀ := .trans P p p₀
  let := Localization.AtPrime.algebraOfLiesOver p₀ p
  let := Localization.AtPrime.algebraOfLiesOver p P
  let := Localization.AtPrime.algebraOfLiesOver p₀ P
  have hp₀ : p₀ = P.under R := Ideal.LiesOver.over
  have : EssFiniteType S T := .of_comp R S T
  have := Algebra.EssFiniteType.isNoetherianRing S T
  rw [isUnramifiedAt_iff_map_eq R p₀ p]
  have ⟨h₁, h₂⟩ := (isUnramifiedAt_iff_map_eq R p₀ P).mp ‹_›
  refine ⟨Algebra.isSeparable_tower_bot_of_isSeparable _ _ P.ResidueField, ?_⟩
  by_cases hp : p = ⊥
  · have : p₀.map (algebraMap R S) = p := by
      subst hp
      exact le_bot_iff.mp (Ideal.map_comap_le)
    rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, this,
      Localization.AtPrime.map_eq_maximalIdeal]
  rw [← Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff hp Ideal.map_comap_le,
    ← not_ne_iff, Ideal.ramificationIdx'_ne_one_iff Ideal.map_comap_le]
  intro H
  have := Ideal.ramificationIdx'_eq_one_of_map_localization
    (hp₀ ▸ Ideal.map_comap_le) (hP₂ hp) hP₁ h₂
  rw [← not_ne_iff, Ideal.ramificationIdx'_ne_one_iff (hp₀ ▸ Ideal.map_comap_le)] at this
  replace H := Ideal.map_mono (f := algebraMap S T) H
  rw [Ideal.map_map, ← IsScalarTower.algebraMap_eq, Ideal.map_pow] at H
  refine this (H.trans (Ideal.pow_right_mono ?_ _))
  exact Ideal.map_le_iff_le_comap.mpr Ideal.LiesOver.over.le

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
n : ℕ
IH : (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i
⊢ ((Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i) ^ s.card * (Submodule.toAddSubgroup I).index ≤
    (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range (n + 1), s.card ^ i

Tactic:
rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case pos.hle
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ span {x} ≤ Q ^ 0

Tactic:
simp [hxQ _ hQp hQ]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case hlt
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ ¬span {x} ≤ Q ^ (0 + 1)

Tactic:
simp [hxQ _ hQp hQ]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.IsTorsionFree R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P ↦ P.IsPrime := Classical.decPred fun P ↦ P.IsPrime
P : Ideal Sₚ
⊢ P ∈ {P ∈ {⊥} ∪ (normalizedFactors (map (algebraMap R Sₚ) p)).toFinset | P.IsPrime} ↔ P ∈ {I | I.IsPrime}

Tactic:
Finset.mem_filter,

Goal state after:
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.IsTorsionFree R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P ↦ P.IsPrime := Classical.decPred fun P ↦ P.IsPrime
P : Ideal Sₚ
⊢ P ∈ {⊥} ∪ (normalizedFactors (map (algebraMap R Sₚ) p)).toFinset ∧ P.IsPrime ↔ P ∈ {I | I.IsPrime}
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Finite (S ⧸ I)
this : Fintype (S ⧸ I)
d : ℕ
⊢ ↑d ∈ I ↔ ∀ (x : S ⧸ I), ↑d * x = 0

Tactic:
← map_natCast (Ideal.Quotient.mk I),

Goal state after:
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Finite (S ⧸ I)
this : Fintype (S ⧸ I)
d : ℕ
⊢ ↑d ∈ I ↔ ∀ (x : S ⧸ I), (Ideal.Quotient.mk I) ↑d * x = 0
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
inst✝ : Algebra K L
⊢ discr K ^ finrank K L ∣ ↑(discr L).natAbs

Tactic:
natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow K (𝓞 K) L (𝓞 L),

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
inst✝ : Algebra K L
⊢ discr K ^ finrank K L ∣ ↑(Ideal.absNorm (differentIdeal (𝓞 K) (𝓞 L)) * (discr K).natAbs ^ finrank K L)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case pos
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : ⊥.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R I * spanNorm R J)

Tactic:
rw [spanNorm_mul_of_bot_or_top]

Goal state after:
case pos.eq_bot_or_top
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1 + 1)) (ZMod p)).comp (X + Polynomial.map (Int.castRingHom (ZMod p)) 1)).coeff i = 0

Tactic:
Polynomial.map_one,

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1 + 1)) (ZMod p)).comp (X + 1)).coeff i = 0