mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K =
    (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K * (π * 2 ^ (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K

Tactic:
rw [integral_comp_abs (f := fun x => exp (-x)), ← integral_exp_neg_rpow zero_lt_one,
          ← Complex.integral_exp_neg_mul_rpow le_rfl zero_lt_two]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K =
    (2 * ∫ (x : ℝ) in Set.Ioi 0, rexp (-x ^ 1)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖ ^ 1)) ^ nrComplexPlaces 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
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #({a ∈ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) =
    #(MulAction.orbit Gal(K/k) w).toFinset

pp: k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card Gal(K/k)

Tactic:
· congr; ext w'
      rw [mem_filter, mem_filter_univ, Set.mem_toFinset, mem_orbit_iff, @eq_comm _ (comap w' _),
        and_iff_right_iff_imp]
      intro e; rwa [← isUnramifiedIn_comap, ← e]

Goal state after:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card Gal(K/k)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (euclidean.mixedSpace K) = finrank ℚ K

Tactic:
rw [LinearEquiv.finrank_eq (toMixed K).toLinearEquiv, mixedEmbedding.finrank]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝²⁹ : CommRing A
inst✝²⁸ : CommRing B
inst✝²⁷ : CommRing B₂
inst✝²⁶ : CommRing B₃
inst✝²⁵ : Algebra A B
inst✝²⁴ : Algebra A B₂
inst✝²³ : Algebra A B₃
inst✝²² : Field K
inst✝²¹ : Field L
inst✝²⁰ : Field L₂
inst✝¹⁹ : Field L₃
inst✝¹⁸ : Algebra A K
inst✝¹⁷ : Algebra K L
inst✝¹⁶ : Algebra A L
inst✝¹⁵ : IsScalarTower A K L
inst✝¹⁴ : Algebra K L₂
inst✝¹³ : Algebra A L₂
inst✝¹² : IsScalarTower A K L₂
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✝⁵ : Algebra B₂ L₂
inst✝⁴ : IsScalarTower A B₂ L₂
inst✝³ : IsIntegralClosure B₂ A L₂
inst✝² : Algebra B₃ L₃
inst✝¹ : IsScalarTower A B₃ L₃
inst✝ : IsIntegralClosure B₃ A L₃
σ : L →ₐ[K] L₂
σ' : L₂ →ₐ[K] L₃
x : B
⊢ ↑((IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃).symm ((galRestrict' A B B₃ (σ'.comp σ)) x)) =
    ↑((IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃).symm
        (((galRestrict' A B₂ B₃ σ').comp (galRestrict' A B B₂ σ)) x))

Tactic:
simp [galRestrict', Subalgebra.algebraMap_eq]

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
⊢ (aeval b) p = 0

Tactic:
rw [← eval_map_algebraMap, hp, MulSemiringAction.eval_charpoly]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
σ : G
hQp : (σ • P).IsPrime
inst✝ : (σ • P).LiesOver p
⊢ P.ramificationIdx A = (σ • P).ramificationIdx A

Tactic:
ramificationIdx_smul

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
σ : G
hQp : (σ • P).IsPrime
inst✝ : (σ • P).LiesOver p
⊢ P.ramificationIdx A = P.ramificationIdx A
Module: Mathlib.NumberTheory.RamificationInertia.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✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : IsGaloisGroup G A B
inst✝² : Module.Finite A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
inst✝ : p.IsPrime
P : ↑(p.primesOver B)
⊢ p.ramificationIdxIn B ≠ 0

Tactic:
ramificationIdxIn_eq_ramificationIdx p P G

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✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : IsGaloisGroup G A B
inst✝² : Module.Finite A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
inst✝ : p.IsPrime
P : ↑(p.primesOver B)
⊢ (↑P).ramificationIdx A ≠ 0
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : IsDomain A
p : Ideal A
inst✝⁹ : p.IsPrime
B : Type u_2
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : Algebra A B
inst✝⁵ : Module.Finite A B
inst✝⁴ : Flat A B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
this : Fintype ↑(p.primesOver B)
⊢ ∑ _x, p.ramificationIdxIn B * p.inertiaDegIn B = ∑ q, (↑q).ramificationIdx A * (↑q).inertiaDeg A

Tactic:
apply Finset.sum_congr rfl

Goal state after:
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : IsDomain A
p : Ideal A
inst✝⁹ : p.IsPrime
B : Type u_2
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : Algebra A B
inst✝⁵ : Module.Finite A B
inst✝⁴ : Flat A B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
this : Fintype ↑(p.primesOver B)
⊢ ∀ x ∈ Finset.univ, p.ramificationIdxIn B * p.inertiaDegIn B = (↑x).ramificationIdx A * (↑x).inertiaDeg A
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))
y : B
hy : (algebraMap B L) y = ((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x)
⊢ (algebraMap A L) ((intNorm A B) x) = (algebraMap B L) x * (algebraMap B L) y

Tactic:
hy,

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)
⊢ (algebraMap A L) ((intNorm A B) x) =
    (algebraMap B L) x * (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

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

Tactic:
← abs_le,

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I).IsPrime →
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) →
        Submodule.IsPrincipal ↑I
I : ↥(Ideal (𝓞 K))⁰
hI : ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors ↑I
hJ0 : J = 0
⊢ J ∈ isPrincipalSubmonoid (𝓞 K)

Tactic:
simpa [hJ0] using! bot_isPrincipal

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : (under ℤ P).IsPrime → _root_.Prime p
hlies : P.LiesOver (span {p})
hspan : span {↑p.natAbs} = span {p}
⊢ Submodule.IsPrincipal ↑⟨P, HP⟩

Tactic:
have hple : p.natAbs ^ P.inertiaDeg ℤ ≤ ⌊(M K)⌋₊ := by
    refine le_floor ?_
    have : P.IsMaximal := hP.isMaximal (by simpa using HP.2)
    have : (span {p}).IsMaximal := (hpprime (.under ℤ P)).isMaximal_span_singleton
    simpa only [hspan, ← cast_pow, ← natAbs_pow_inertiaDeg p P] using hPN

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : (under ℤ P).IsPrime → _root_.Prime p
hlies : P.LiesOver (span {p})
hspan : span {↑p.natAbs} = span {p}
hple :
  p.natAbs ^ P.inertiaDeg ℤ ≤
    ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
⊢ Submodule.IsPrincipal ↑⟨P, HP⟩
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, (I i).FG) → (∀ i ∈ s, Finite (R ⧸ I i)) → Finite (R ⧸ ∏ i ∈ s, I i)
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite (R ⧸ I i)
this✝ : Finite (R ⧸ I a)
this : Finite (R ⧸ ∏ i ∈ s, I i)
⊢ Finite (R ⧸ (∏ x ∈ s, I x) * I a)

Tactic:
exact Submodule.finite_quotient_smul _ (hI a (by simp))

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

Goal state before:
pp: 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
inst✝ : IsDomain B
hf' : Function.Injective ⇑f
hI : I ≠ 0
hN : 0 ∉ N
⊢ extended L hf I ≠ 0

Tactic:
by
  simp only [ne_eq, ← coeToSubmodule_inj, coe_extended_eq_span, coe_zero, Submodule.span_eq_bot,
    Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    not_forall]
  obtain ⟨x, hx₁, hx₂⟩ : ∃ x ∈ I, x ≠ 0 := by simpa [ne_eq, eq_zero_iff] using hI
  refine ⟨x, hx₁, ?_⟩
  exact (map_ne_zero_iff _ (IsLocalization.map_injective_of_injective' _ _ _ _ hN hf')).mpr hx₂

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

Goal state before:
pp: case 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 : ℕ
⊢ -↑C ≤ (minpoly ℤ ↑x).coeff i ∧ (minpoly ℤ ↑x).coeff i ≤ ↑C

Tactic:
← abs_le,

Goal state after:
case 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 : ℕ
⊢ |(minpoly ℤ ↑x).coeff i| ≤ ↑C
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : IsTorsionFree Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
⊢ IsPrincipalIdealRing Rₚ

Tactic:
have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : IsTorsionFree Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
this : IsDiscreteValuationRing (Localization.AtPrime p)
⊢ IsPrincipalIdealRing Rₚ
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case refine_1
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
⊢ ↑u * ↑(discr K₁) ∈ Ideal.map (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁))

Tactic:
apply Ideal.mul_mem_left

Goal state after:
case refine_1
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
⊢ ↑(discr K₁) ∈ Ideal.map (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁))
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

Goal state after:
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
⊢ ↑(discr K₂) ∈ Ideal.map (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂))
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: 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
T : Type u_4
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain T
inst✝⁷ : IsIntegrallyClosed T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T S
inst✝⁴ : Module.Finite R T
inst✝³ : Module.Finite T S
inst✝² : IsTorsionFree R T
inst✝¹ : IsTorsionFree T S
inst✝ : IsScalarTower R T S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
⊢ spanNorm R (spanNorm T I) = spanNorm R I

Tactic:
obtain h | h := eq_bot_or_top (spanNorm R I)

Goal state after:
case inl
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
T : Type u_4
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain T
inst✝⁷ : IsIntegrallyClosed T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T S
inst✝⁴ : Module.Finite R T
inst✝³ : Module.Finite T S
inst✝² : IsTorsionFree R T
inst✝¹ : IsTorsionFree T S
inst✝ : IsScalarTower R T S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : spanNorm R I = ⊥
⊢ spanNorm R (spanNorm T I) = spanNorm R I

case inr
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
T : Type u_4
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain T
inst✝⁷ : IsIntegrallyClosed T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T S
inst✝⁴ : Module.Finite R T
inst✝³ : Module.Finite T S
inst✝² : IsTorsionFree R T
inst✝¹ : IsTorsionFree T S
inst✝ : IsScalarTower R T S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I : Ideal S
h : spanNorm R I = ⊤
⊢ spanNorm R (spanNorm T I) = spanNorm R I
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
⊢ #t + #u = n

Tactic:
by rw [← card_union_of_disjoint htu, htus, card_range]

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

Goal state before:
pp: case h.calc_3
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))
⊢ (Algebra.norm K) (p • (z * B.gen ^ n) - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n)) =
    (algebraMap R K) p ^ n.succ * (algebraMap R K) r

Tactic:
simp_rw [← smul_sum, ← smul_sub, Algebra.smul_def p, algebraMap_apply R K L, map_mul,
      Algebra.norm_algebraMap, finrank_K_L, hr, ← hn]

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

Goal state before:
pp: case pos
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : restrictScalars A (Algebra.trace K L).range ≤ 1
⊢ ⊤ᵛ = ⊤

Tactic:
rw [_root_.eq_top_iff]

Goal state after:
case pos
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : restrictScalars A (Algebra.trace K L).range ≤ 1
⊢ ⊤ ≤ ⊤ᵛ