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

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
⊢ LSeriesSummable (fun n ↦ χ ↑n) s ↔ 1 < s.re

Tactic:
refine ⟨fun H ↦ ?_, LSeriesSummable_of_one_lt_re χ⟩

Goal state after:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n ↦ χ ↑n) s
⊢ 1 < s.re
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: case neg
r : ℝ
h : ¬r < -1
H : Summable fun p ↦ ↑↑p ^ r
⊢ ∀ (b : Primes), 1 / ↑↑b ≤ ↑↑b ^ r

Tactic:
intro p

Goal state after:
case neg
r : ℝ
h : ¬r < -1
H : Summable fun p ↦ ↑↑p ^ r
p : Primes
⊢ 1 / ↑↑p ≤ ↑↑p ^ r
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 0 < riemannZeta ↑x

Tactic:
by
  have hx' : 1 < (x : ℂ).re := by simpa using hx
  rw [← LSeries_one_eq_riemannZeta hx']
  refine LSeries.positive (fun _ ↦ by simp) (by simp) ?_
  simpa [LSeries.abscissaOfAbsConv_one] using (by exact_mod_cast hx : (1 : EReal) < x)

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ (Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0))
    s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
exact this

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖-I‖ * ‖cexp (↑(2 * π * a * ↑n) * I)‖ / 2 = 1 / 2

Tactic:
norm_neg,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖I‖ * ‖cexp (↑(2 * π * a * ↑n) * I)‖ / 2 = 1 / 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z : ℤ
this : ¬z * z % ↑4 = 2 % ↑4
⊢ z * z % 4 ≠ 2

Tactic:
exact this

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case mp
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha✝ : Irreducible a
hb : b ≠ 0
ha : a ∣ radical b
⊢ a ∣ b

Tactic:
exact ha.trans radical_dvd_self

Goal state after:
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x₁✝ x₂✝ : ↥↑↑I
h : (↑ℤ (↑↑I).subtype) x₁✝ = (↑ℤ (↑↑I).subtype) x₂✝
⊢ x₁✝ = x₂✝

Tactic:
← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x₁✝ x₂✝ : ↥↑↑I
h : (↑ℤ (↑↑I).subtype) x₁✝ = (↑ℤ (↑↑I).subtype) x₂✝
⊢ (↑↑I).subtype x₁✝ = (↑↑I).subtype x₂✝
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
this : ↑(K.toIntermediateField this✝) = ↑⊥ ∨ ↑(K.toIntermediateField this✝) = ↑⊤
⊢ ↑K = ↑ofRealHom.fieldRange ∨ ↑K = ↑⊤

Tactic:
exact this

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
⊢ ↑(Ideal.absNorm (num 1)) / ↑|(Algebra.norm ℤ) ↑(den 1)| = 1

Tactic:
by
    rw [absNorm_div_norm_eq_absNorm_div_norm 1 ⊤ (by simp [Submodule.one_eq_range]),
      Ideal.absNorm_top, Nat.cast_one, OneMemClass.coe_one, map_one, abs_one,
      Int.cast_one,
      one_div_one]

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ z ↑a ^ z.mult < 1

Tactic:
· refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)
      by_cases hz : z = w
      · rwa [hz]
      · exact h hz

Goal state after:
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 : w.IsReal
⊢ False

Tactic:
NumberField.InfinitePlace.isReal_iff

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
⊢ False
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
⊢ IsUnramified k w ↔ w.mult ≤ (w.comap (algebraMap k K)).mult

Tactic:
by
  rw [IsUnramified, le_antisymm_iff, and_iff_right]
  exact mult_comap_le _ _

Goal state after:
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
φ : K →+* ℂ
⊢ IsRamified k (mk φ) ↔ IsMixed k φ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsRamified k (mk φ)
⊢ IsMixed k φ

case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
⊢ IsRamified k (mk φ)
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
φ : K →+* ℂ
⊢ IsUnramified k (mk φ) ↔ IsUnmixed k φ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
⊢ IsUnmixed k φ

case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
⊢ IsUnramified k (mk φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
⊢ (normAtPlace w) (fun x ↦ c, fun x ↦ ↑c) = |c|

Tactic:
show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp,

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
⊢ (normAtPlace w) (c • 1) = |c|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : mixedSpace K
⊢ (∀ (w : InfinitePlace K), (normAtPlace w) x = 0) ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
⊢ x = 0

case refine_2
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e'_3.e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal |B ^ finrank ℝ (mixedSpace K)|

Tactic:
rw [abs_pow, ofReal_pow (abs_nonneg _), abs_eq_self.mpr (le_of_lt hB),
          mixedEmbedding.finrank]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ mixedEmbedding.norm (fun x ↦ c, fun x ↦ ↑c) = |c| ^ finrank ℚ K

Tactic:
show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ mixedEmbedding.norm (c • 1) = |c| ^ finrank ℚ K
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
inst✝ : IsGalois k K
⊢ ¬IsUnramified k w ↔ Nat.card ↥(Stab w) = 2

Tactic:
rw [isUnramified_iff_card_stabilizer_eq_one]
  obtain (e | e) := nat_card_stabilizer_eq_one_or_two k w <;> rw [e] <;> decide

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) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)| =
    (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
rw [div_pow B, ← Real.rpow_natCast B, ← Real.rpow_mul (by positivity), div_mul_cancel₀ _
    (Nat.cast_ne_zero.mpr <| ne_of_gt finrank_pos), Real.rpow_one, mul_comm_div, mul_div_assoc']

Goal state after:
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) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial * √|↑(discr K)| /
      ↑(finrank ℚ K) ^ finrank ℚ K =
    (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal / ↑(finrank ℚ K) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_2.inr
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
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w // w.IsReal }), ¬x.1 a = 0
⊢ (∃ i, x ∈ ⇑(negAt i) '' plusPart A) ∨ x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}

Tactic:
refine Or.inl ⟨signSet x,
        (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
      · exact lt_of_le_of_ne hw (hx w)
      · exact lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ ↑|discr K|

Tactic:
by
  refine le_trans ?_ (abs_discr_ge' K)
  -- The sequence `a n` is a lower bound for `|discr K|`. We prove below by induction a uniform
  -- lower bound for this sequence from which we deduce the result.
  rw [mul_comm 2 _]
  let a : ℕ → ℝ := fun n => (n : ℝ) ^ (n * 2) / ((4 / π) ^ n * (n.factorial : ℝ) ^ 2)
  suffices ∀ n, 2 ≤ n → (4 / 9 : ℝ) * (3 * π / 4) ^ n ≤ a n by
    refine le_trans (this (finrank ℚ K) h) ?_
    simp only [a]
    gcongr
    · exact (one_le_div Real.pi_pos).2 Real.pi_le_four
    · rw [← card_add_two_mul_card_eq_rank, mul_comm]
      exact Nat.le_add_left _ _
  intro n hn
  induction n, hn using Nat.le_induction with
  | base => exact le_of_eq <| by simp [a, Nat.factorial_two]; field
  | succ m _ h_m =>
      suffices (3 : ℝ) ≤ (1 + 1 / m : ℝ) ^ (2 * m) by
        convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)
        · simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]
          field_simp
          simp [field, div_pow]
          ring
        · rw [_root_.le_div_iff₀ (by positivity), pow_succ]
          convert! (mul_le_mul h_m this (by positivity) (by positivity)) using 1
          field
      refine le_trans (le_of_eq (by simp [field]; norm_num)) (one_add_mul_le_pow ?_ (2 * m))
      exact le_trans (by norm_num : (-2 : ℝ) ≤ 0) (by positivity)

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
B₂ : Type u_7
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : CommRing B₂
inst✝¹³ : Algebra A B
inst✝¹² : Algebra A B₂
inst✝¹¹ : IsIntegrallyClosed A
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Algebra.IsIntegral A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain B₂
inst✝⁴ : IsIntegrallyClosed B₂
inst✝³ : Algebra.IsIntegral A B₂
inst✝² : IsTorsionFree A B₂
inst✝¹ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
inst✝ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B₂)
x : B
σ : B ≃ₐ[A] B₂
⊢ (intNorm A B₂) (σ x) = (intNorm A B) x

Tactic:
apply FaithfulSMul.algebraMap_injective A (FractionRing A)
  rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
    ← galLiftEquiv_algebraMap_apply (FractionRing A) (FractionRing B), norm_eq_of_algEquiv]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsIntegral A (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x))
⊢ x ∣ (algebraMap A B) ((intNorm A B) x)

Tactic:
obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this

Goal state after:
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this : IsIntegral A (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x))
y : B
hy : (algebraMap B L) y = ((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x)
⊢ x ∣ (algebraMap A B) ((intNorm A B) x)
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case hs
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ ↑(I + J)
⊢ (IsLocalization.map L f hf) (i + j) ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))

Tactic:
map_add

Goal state after:
case hs
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ ↑(I + J)
⊢ (IsLocalization.map L f hf) i + (IsLocalization.map L f hf) j ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: case he
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x✝ : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
x : R
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) x) =
    (algebraMap S (Sₚ ⧸ pSₚ)) ((algebraMap R S) x)

Tactic:
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ → span R s = ⊤

Tactic:
intro hs
    rw [← top_le_iff]
    apply le_of_le_smul_of_le_jacobson_bot
    · exact Module.finite_def.mp ‹_›
    · exact (jacobson_eq_maximalIdeal ⊥ bot_ne_top).ge
    · rw [Ideal.smul_top_eq_map]
      rintro x -
      have : LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS) : S →ₗ[R] S ⧸ pS) =
          Submodule.restrictScalars R pS := by
        ext; simp [Ideal.Quotient.eq_zero_iff_mem]
      rw [← this, ← comap_map_eq, mem_comap, ← H, hs, restrictScalars_top]
      exact mem_top

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

Goal state before:
pp: case refine_1.refine_2
A : Type u_1
inst✝¹¹ : CommRing A
B : Type u_2
inst✝¹⁰ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁹ : CommRing K
inst✝⁸ : Algebra A K
inst✝⁷ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝⁶ : CommRing L
inst✝⁵ : Algebra B L
inst✝⁴ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
y z : L
x✝¹ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
x✝ : z ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
hz : (IsLocalization.map W g hg) z ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ (IsLocalization.map W g hg) (y + z) ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))

Tactic:
map_add

Goal state after:
case refine_1.refine_2
A : Type u_1
inst✝¹¹ : CommRing A
B : Type u_2
inst✝¹⁰ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁹ : CommRing K
inst✝⁸ : Algebra A K
inst✝⁷ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝⁶ : CommRing L
inst✝⁵ : Algebra B L
inst✝⁴ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
y z : L
x✝¹ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
x✝ : z ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
hz : (IsLocalization.map W g hg) z ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ (IsLocalization.map W g hg) y + (IsLocalization.map W g hg) z ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : Ideal R
d : ℤ
⊢ ↑d ∈ I ↔ ↑(absNorm (under ℤ I)) ∣ d

Tactic:
by
  rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]

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

Goal state before:
pp: case refine_2
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑v * ↑(discr K₂) ∈ Ideal.map (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂))

Tactic:
apply Ideal.mul_mem_left
    rw [← map_intCast (algebraMap (𝓞 K₂) (𝓞 L))]
    exact Ideal.mem_map_of_mem (algebraMap (𝓞 K₂) (𝓞 L)) <| discr_mem_differentIdeal _ _

Goal state after:
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 K ^ finrank K L * (↑(Ideal.absNorm (differentIdeal (𝓞 K) (𝓞 L))) * (discr K).sign ^ finrank K L)

Tactic:
exact Int.dvd_mul_right _ _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen) Q = p • z
hzint : IsIntegral R z
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
this : Module.Finite K L := finite B
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : (minpoly K B.gen).natDegree = B.dim
deg_R_P : P.natDegree = B.dim
f : ℕ → L
hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
r : R
hr :
  (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
i : ℕ
hi : i ∈ (range (Q.natDegree + 1)).erase 0
⊢ Q.coeff i • (B.gen ^ i * B.gen ^ n) = p • Q.coeff i • f (i + n)

Tactic:
rw [← pow_add, ← (hf _ (aux i hi)).2, ← Algebra.smul_def, smul_smul, mul_comm _ p, smul_smul]

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

Goal state before:
pp: p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]

Goal state after:
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ p ^ s - 1)) = (algebraMap ℤ ℚ) (↑p ^ p ^ s)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]

Goal state after:
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ 2 ^ k - 1)) = (algebraMap ℤ ℚ) ((-2) ^ 2 ^ k)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h : (if ⟨1, hdim⟩ = ⟨1, hdim⟩ then 1 else 0) = (pB.basis.repr (↑p * x + ↑n)) ⟨1, hdim⟩
this : pB.gen = hζ.toInteger
⊢ False

Tactic:
simp only [↓reduceIte, map_add, Finsupp.coe_add, Pi.add_apply] at h

Goal state after:
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = (pB.basis.repr (↑p * x)) ⟨1, hdim⟩ + (pB.basis.repr ↑n) ⟨1, hdim⟩
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case pos
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ -1 - 1 ∣ ↑2

Tactic:
exact ⟨-1, by ring⟩

Goal state after: