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

Goal state before:
pp: N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
⊢ (toArithmeticFunction fun x ↦ χ ↑x).IsMultiplicative

Tactic:
by
  refine IsMultiplicative.iff_ne_zero.mpr ⟨?_, fun {m} {n} hm hn _ ↦ ?_⟩
  · simp [toArithmeticFunction]
  · simp [toArithmeticFunction, hm, hn]

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

Goal state before:
pp: case inl
χ : DirichletCharacter ℂ 0
⊢ χ 0 = δ 0

Tactic:
χ.map_nonunit not_isUnit_zero,

Goal state after:
case inl
χ : DirichletCharacter ℂ 0
⊢ 0 = δ 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)

Tactic:
simpa only [Gammaℝ_one, inv_one, mul_one] using! (completedHurwitzZetaEven_residue_one a).mul
      <| (differentiable_Gammaℝ_inv.continuous.tendsto _).mono_left nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ Summable fun n ↦ ‖(riemannZetaSummandHom ⋯) n‖

Tactic:
by
  simp only [riemannZetaSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
  convert! Real.summable_nat_rpow_inv.mpr hs with n
  rw [← ofReal_natCast,
    norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
    neg_re, Real.rpow_neg <| Nat.cast_nonneg n]

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Summable fun n ↦ ‖(dirichletSummandHom χ ⋯) n‖

Tactic:
simp only [dirichletSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, norm_mul]

Goal state after:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Summable fun n ↦ ‖χ ↑n‖ * ‖↑n ^ (-s)‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ s ≠ 0

Tactic:
simpa using hs 0

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ (x * x + y * y) * (k * k) = z * z * (k * k)

Tactic:
convert! h using 1 <;> ring

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : wronskian 0 b ≠ 0
⊢ False

Tactic:
rw [wronskian_zero_left] at hw

Goal state after:
R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : 0 ≠ 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
by
  by_cases ha : a = 0
  · simp [ha]
  · exact natDegree_le_of_dvd radical_dvd_self ha

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl
m n : ℤ
h : m.gcd n = 1
h1 : m % 2 = 0 ∧ n % 2 = 1
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

pp: case inr
m n : ℤ
h : m.gcd n = 1
h2 : m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
· exact coprime_sq_sub_mul_of_even_odd h h1.left h1.right

Goal state after:
case inr
m n : ℤ
h : m.gcd n = 1
h2 : m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
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
⊢ ↑1 / ↑|(Algebra.norm ℤ) ↑1| = 1

Tactic:
Nat.cast_one,

Goal state after:
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
⊢ 1 / ↑|(Algebra.norm ℤ) ↑1| = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht1 : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
⊢ ∃ m n,
    x = m ^ 2 - n ^ 2 ∧
      y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
use m, n
    rcases ht1 with h_odd | h_even
    · apply And.intro h_odd.1
      apply And.intro h_odd.2
      rcases ht2 with h_pos | h_neg
      · apply And.intro h_pos (And.intro ht3 (And.intro ht4 hm))
      · exfalso
        revert h_pos
        rw [h_neg]
        exact imp_false.mpr (not_lt.mpr (neg_nonpos.mpr (by positivity)))
    exfalso
    rcases h_even with ⟨rfl, -⟩
    rw [mul_assoc, Int.mul_emod_right] at h_parity
    exact zero_ne_one h_parity

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
this : ∀ (w : InfinitePlace K), ∀ φ ∈ {φ | mk φ = w}, ‖φ x‖ = w x
⊢ ∏ w, w x ^ w.mult = ∏ j, ∏ i with mk i = j, ‖i x‖

Tactic:
Finset.prod_congr rfl (this _),

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
this : ∀ (w : InfinitePlace K), ∀ φ ∈ {φ | mk φ = w}, ‖φ x‖ = w x
⊢ ∏ w, w x ^ w.mult = ∏ x_1, ∏ x_2 with mk x_2 = x_1, x_1 x
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
⊢ |↑((RingOfIntegers.norm ℚ) x)| = 1 ↔ IsUnit ((RingOfIntegers.norm ℚ) x)

Tactic:
rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff]

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf ⟨ζ, hζ⟩ ∣ torsionOrder K

Tactic:
apply orderOf_dvd_natCard

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : orderOf ⟨-1, ⋯⟩ = 2
⊢ orderOf ⟨-1, ⋯⟩ ∣ torsionOrder K

Tactic:
apply orderOf_dvd_natCard

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #{φ | mkComplex φ = ⟨w, hw⟩} = #{φ | mk φ = w}

Tactic:
← Fintype.card_subtype,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ card { x // mkComplex x = ⟨w, hw⟩ } = #{φ | mk φ = w}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case neg.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : ((commMap K) x).2 ⟨InfinitePlace.mk φ, ⋯⟩ = 0.2 ⟨InfinitePlace.mk φ, ⋯⟩
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ (starRingEnd ℂ) (x φ) = (starRingEnd ℂ) 0

Tactic:
rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ∑ x_1, ↑1 * (normAtPlace ↑x_1) x + ∑ x_1, ↑2 * (normAtPlace ↑x_1) x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖

Tactic:
Nat.cast_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ∑ x_1, 1 * (normAtPlace ↑x_1) x + ∑ x_1, ↑2 * (normAtPlace ↑x_1) x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ Continuous ⇑(normAtPlace w)

Tactic:
simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ Continuous fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
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:
rw [← SetLike.coe_sort_coe, ← mk_embedding w]

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 (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
⊢ ENNReal.ofReal |(Basis.det ?b₀) ⇑((fractionalIdealLatticeBasis K I).reindex e)| * volume (fundamentalDomain ?b₀) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))

pp: case b₀
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := ⋯
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)

Tactic:
· rw [show (fractionalIdealLatticeBasis K I).reindex e = (mixedEmbedding K) ∘
        (basisOfFractionalIdeal K I) ∘ e.symm by
      ext1; simp only [Basis.coe_reindex, Function.comp_apply, fractionalIdealLatticeBasis_apply]]
    rw [mixedEmbedding.det_basisOfFractionalIdeal_eq_norm]

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

Goal state before:
pp: case inl
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ unmixedEmbeddingsOver L v.embedding
h✝ : (mk ψ).embedding = ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ

pp: case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ unmixedEmbeddingsOver L v.embedding
hψ : (mk ψ).embedding = conjugate ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ

Tactic:
· aesop (add simp [embeddingConjugateIte, unmixedEmbeddingsOver])

Goal state after:
case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ unmixedEmbeddingsOver L v.embedding
hψ : (mk ψ).embedding = conjugate ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ
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
this :
  (latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) =
    (algebraMap ℚ ℝ) ((integralBasis K).det (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))
⊢ |(latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)| = ↑(FractionalIdeal.absNorm ↑I)

Tactic:
by
    rw [this, eq_ratCast, ← Rat.cast_abs, ← Equiv.symm_symm e, ← Basis.coe_reindex,
      det_basisOfFractionalIdeal_eq_absNorm K I e]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsIntegralClosure B A L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsIntegrallyClosed A
x : B
⊢ ∏ σ, ((galRestrict A K L B) σ) x =
    (algebraMap A B) (IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) x)) ⋯)

Tactic:
apply IsIntegralClosure.algebraMap_injective B A L
  rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_eq A K L]
  simp only [map_prod, algebraMap_galRestrict_apply, IsIntegralClosure.algebraMap_mk',
    Algebra.norm_eq_prod_automorphisms, RingHom.coe_comp, Function.comp_apply]

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

Goal state before:
pp: 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
h_eval : (aeval b) p = 0
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)
⊢ (aeval d) (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) q)) = 0

Tactic:
simp_rw [q, map_comp, Polynomial.map_mul, map_C, map_X, aeval_comp, aeval_mul, aeval_C, aeval_X,
      ← RingHom.comp_apply, ← RingHom.comp_assoc, comm₁, RingHom.comp_apply, d, mul_div, ← map_mul]

Goal state after:
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
h_eval : (aeval b) p = 0
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)
⊢ (aeval
        ((algebraMap (B ⧸ Q) L) ((algebraMap (A ⧸ P) (B ⧸ Q)) ((algebraMap A (A ⧸ P)) a) * x) /
          (algebraMap (B ⧸ Q) L) y))
      (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) p)) =
    0
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg.refine_2
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 : IsTorsionFree B E
a : E
ha : a ∈ (minpoly K ((algebraMap B L) x)).aroots E
⊢ eval₂ (algebraMap A E) a (minpoly A x) = 0

Tactic:
suffices (aeval a) ((minpoly A x).map (algebraMap A K)) = 0 by simpa

Goal state after:
case neg.refine_2
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 : IsTorsionFree B E
a : E
ha : a ∈ (minpoly K ((algebraMap B L) x)).aroots E
⊢ (aeval a) (map (algebraMap A K) (minpoly A x)) = 0
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
I₀ : Ideal (𝓞 K)
h_nm :
  ↑(Submodule.cardQuot ↑J) * ↑(absNorm I₀) ≤
    ↑(absNorm ↑J) * ((4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|))
hI : span {a} = ↑J * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ := ⟨I₀, ⋯⟩
⊢ 0 < ↑(Submodule.cardQuot ↑J)

Tactic:
exact cast_pos.mpr <| pos_of_ne_zero <| absNorm_ne_zero_of_nonZeroDivisors J

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

Goal state before:
pp: case 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 J : FractionalIdeal M K
x✝ : L
h : x✝ ∈ ⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J
⊢ x✝ ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(I * J)))

Tactic:
· rcases Set.mem_mul.mp h with ⟨y, ⟨i, hi, rfl⟩, z, ⟨j, hj, rfl⟩, rfl⟩
    exact Submodule.subset_span ⟨i * j, mul_mem_mul hi hj, by simp⟩

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

Goal state before:
pp: case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (√(1 + ↑(boundOfDiscBdd N) ^ 2)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑C

Tactic:
· refine le_trans ?_ (Nat.le_ceil _)
        rw [val_eq_coe, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_max, NNReal.coe_one,
          Real.coe_sqrt, NNReal.coe_add 1, NNReal.coe_one, NNReal.coe_pow]
        gcongr
        · exact le_max_right _ 1
        · exact rank_le_rankOfDiscrBdd hK₂
        · rw [NNReal.coe_natCast, Nat.cast_le]
          exact (Nat.choose_le_choose _ (rank_le_rankOfDiscrBdd hK₂)).trans
            (Nat.choose_le_middle _ _)

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := ⋯
h : J = ⊤
⊢ ↑↑I * (R ∙ v) ≤ (Algebra.linearMap R A).range

Tactic:
← Submodule.one_eq_range,

Goal state after:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
⊢ ↑↑I * (R ∙ v) ≤ 1
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case mpr
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝⁴ : IsDomain 𝒪
this✝³ : IsDedekindDomain 𝒪
this✝² : IsFractionRing 𝒪 K
this✝¹ : Module.Finite ℤ 𝒪
this✝ : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this : Ideal.absNorm P ∣ Ideal.absNorm (differentIdeal ℤ 𝒪)
⊢ p ∣ discr K

Tactic:
rw [absNorm_differentIdeal K, ← Ideal.natAbs_pow_inertiaDeg p,
      ← Int.natAbs_pow, Int.natAbs_dvd_natAbs] at this

Goal state after:
case mpr
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝⁴ : IsDomain 𝒪
this✝³ : IsDedekindDomain 𝒪
this✝² : IsFractionRing 𝒪 K
this✝¹ : Module.Finite ℤ 𝒪
this✝ : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this : p ^ P.inertiaDeg ℤ ∣ discr K
⊢ p ∣ discr K
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime p

pp: case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime (-p)

Tactic:
· exact hp

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime (-p)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case neg
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))
htwo : ¬p = 2
⊢ Prime (hζ.toInteger - 1)

Tactic:
apply hζ.zeta_sub_one_prime_of_ne_two htwo

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

Goal state before:
pp: case pos.zero
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this✝ : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
q : ℕ
hn : 2 < 2
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
hμ : IsPrimitiveRoot μ (q ^ (0 + 1))
hC : IsCyclotomicExtension {q ^ (0 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (0 + 1) = n
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
exact hn.false.elim

Goal state after: