mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
hc : IsRelPrime a 0
⊢ primeFactors (a * 0) = (primeFactors a).disjUnion (primeFactors 0) ⋯

pp: case inr.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
· rw [isRelPrime_zero_right] at hc
    simp only [mul_zero, primeFactors_zero, primeFactors_of_isUnit hc, Finset.disjUnion_empty]

Goal state after:
case inr.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : ComplexEmbedding.conjugate (mk φ).embedding = φ
⊢ ComplexEmbedding.IsReal φ

Tactic:
← ComplexEmbedding.isReal_conjugate_iff,

Goal state after:
case inr
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (ComplexEmbedding.conjugate (mk φ).embedding)
h : ComplexEmbedding.conjugate (mk φ).embedding = φ
⊢ ComplexEmbedding.IsReal φ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding

Tactic:
by
  refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
  rintro ⟨φ, ⟨hφ, rfl⟩⟩
  contrapose hφ
  cases mk_eq_iff.mp (mk_embedding (mk φ)) with
  | inl h => rwa [h] at hφ
  | inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
cases h₃ with
    | inl hw =>
      rw [conjugate_embedding_eq_of_isReal hw, or_self] at main
      exact congr_arg RingHom.toRatAlgHom main
    | inr hw =>
      refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)
      have : (embedding w x).im = 0 := by
        rw [← Complex.conj_eq_iff_im]
        have := RingHom.congr_fun h' x
        simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this
        rw [this]
        exact hψ.symm
      rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K

Tactic:
by
  classical
  rw [← card_real_embeddings, ← card_complex_embeddings, Fintype.card_subtype_compl,
    ← Embeddings.card K ℂ, Nat.add_sub_of_le]
  exact Fintype.card_subtype_le _

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
heq : (expand k ch) (C u * ca ^ p) + (expand k ch) (C v * cb ^ q) + (expand k ch) (C w * cc ^ r) = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0

Tactic:
← map_add

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
heq : (expand k ch) (C u * ca ^ p + C v * cb ^ q + C w * cc ^ r) = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case refine_1
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hca : IsCoprime c a
⊢ a.natDegree = 0

Tactic:
apply flt_catalan_aux heq <;> assumption

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case refine_2
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : r * p + p * q + q * r ≤ q * r * p
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hbc : IsCoprime b c
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hca : IsCoprime c a
⊢ b.natDegree = 0

Tactic:
apply flt_catalan_aux heq <;> assumption

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case refine_3
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : p * q + q * r + r * p ≤ r * p * q
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C w * c ^ r + C u * a ^ p + C v * b ^ q = 0
hbc : IsCoprime b c
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hca : IsCoprime c a
⊢ c.natDegree = 0

Tactic:
apply flt_catalan_aux heq <;> assumption

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
w : InfinitePlace K
h : IsUnramified k w
⊢ IsUnmixed k w.embedding

Tactic:
by
  intro hw
  rw [← isReal_mk_iff, ← comap_mk, mk_embedding] at hw
  exact isReal_iff.1 <| (isUnramified_iff.1 h).resolve_right (not_isComplex_iff_isReal.2 hw)

Goal state after:
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 ⋯
⊢ ⇑((fractionalIdealLatticeBasis K I).reindex e) = ⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e.symm

Tactic:
ext1; simp only [Basis.coe_reindex, Function.comp_apply, fractionalIdealLatticeBasis_apply]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑(NNReal.sqrt B ^ 2)

Tactic:
NNReal.sq_sqrt

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
left✝ : w.LiesOver v
hw : IsUnramified K w
h : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ v.embeddingConjugateIte w ∈ unmixedEmbeddingsOver L v.embedding

Tactic:
simpa [embeddingConjugateIte_pos h] using ⟨h, hw.isUnmixed⟩

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
⊢ #⋯.toFinset = Fintype.card (L →ₐ[K] ℂ)

Tactic:
apply (card_nbij AlgHom.toRingHom (fun σ _ ↦ by simpa using ⟨by aesop⟩)
    AlgHom.coe_ringHom_injective.injOn (fun ψ hψ ↦ ?_)).symm

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
ψ : L →+* ℂ
hψ : ψ ∈ ↑⋯.toFinset
⊢ ψ ∈ AlgHom.toRingHom '' ↑univ
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✝ : Algebra.IsAlgebraic K L
⊢ galLift K L L (AlgHom.id A B) = AlgHom.id K L

Tactic:
ext; simp [galLift]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = ‖x.1 w‖

Tactic:
rw [negAt_apply_isReal_and_mem _ hw, Real.norm_of_nonpos hw]

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
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝¹ : Algebra.IsIntegral A C
this✝ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
orbit_eq : orbit (↥H) Q = P.primesOver C
stabilizer_eq : stabilizer (↥H) Q = (stabilizer GAC Q).subgroupOf H
⊢ (stabilizer G P).index * (stabilizer GAC Q).relIndex H = (stabilizer GAC Q).index

Tactic:
← (stabilizer G P).index_comap_of_surjective (restrictHom_surjective GAC G A B C),

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝¹ : Algebra.IsIntegral A C
this✝ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
orbit_eq : orbit (↥H) Q = P.primesOver C
stabilizer_eq : stabilizer (↥H) Q = (stabilizer GAC Q).subgroupOf H
⊢ (Subgroup.comap (restrictHom GAC G A B C) (stabilizer G P)).index * (stabilizer GAC Q).relIndex H =
    (stabilizer GAC Q).index
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_1
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| = |↑((minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i)|

Tactic:
Int.cast_abs

Goal state after:
case refine_2.refine_1
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)| = |↑((minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i)|
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsDedekindDomain R
inst✝ : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : P₁ ∈ p.primesOver S
hP₂ : P₂ ∈ p.primesOver S
⊢ ∃ σ, comap ((galRestrict R K L S) σ) P₁ = P₂

Tactic:
by
  have : IsDomain S :=
    (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R L)
  have := IsIntegralClosure.isDedekindDomain R K L S
  have : Module.Finite R S := IsIntegralClosure.finite R K L S
  have := hP₁.1
  have := hP₁.2
  have := hP₂.1
  have := hP₂.2
  have : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
  let : MulSemiringAction Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
  have : IsGaloisGroup Gal(L/K) R S := IsGaloisGroup.of_isFractionRing _ _ _ K L
  obtain ⟨σ, rfl⟩ := exists_smul_eq_of_isGaloisGroup p P₂ P₁ Gal(L/K)
  exact ⟨σ, comap_map_of_bijective _ ((galRestrict R K L S σ).bijective)⟩

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

Goal state before:
pp: case mp
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
x : L
⊢ x ∈ extended L hf I → x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)

Tactic:
{ intro hx; simpa }

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

Goal state before:
pp: case mpr
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
x : L
⊢ x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I) → x ∈ extended L hf I

Tactic:
{ intro hx; simpa }

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √↑|discr K|) < 2
this : 0 < finrank ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)

Tactic:
Int.cast_abs

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2
this : 0 < finrank ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_1
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| = |↑((minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i)|

Tactic:
Int.cast_abs

Goal state after:
case refine_2.refine_1
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)| = |↑((minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i)|
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: 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
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ ⇑((basisQuotient b).repr ((Ideal.Quotient.mk pS) x)) = ⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)

Tactic:
apply (Finsupp.linearEquivFunOnFinite (R ⧸ p) _ _).symm.injective

Goal state after:
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
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm ⇑((basisQuotient b).repr ((Ideal.Quotient.mk pS) x)) =
    (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x))
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : IsArtinianRing (R ⧸ I)
hI : ¬I = ⊤
this✝² : Nontrivial (R ⧸ I)
this✝¹ : IsLocalRing (R ⧸ I)
this✝ : IsLocalHom (Ideal.Quotient.mk I)
n : ℕ
hn : ⊥.jacobson ^ n = 0
this : Ideal.map (Ideal.Quotient.mk I) p = maximalIdeal (R ⧸ I)
⊢ ∃ n, p ^ n ≤ I

Tactic:
rw [jacobson_eq_maximalIdeal _ bot_ne_top, ← this, ← Ideal.map_pow, Ideal.zero_eq_bot,
    Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker] at hn

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : IsArtinianRing (R ⧸ I)
hI : ¬I = ⊤
this✝² : Nontrivial (R ⧸ I)
this✝¹ : IsLocalRing (R ⧸ I)
this✝ : IsLocalHom (Ideal.Quotient.mk I)
n : ℕ
hn : p ^ n ≤ I
this : Ideal.map (Ideal.Quotient.mk I) p = maximalIdeal (R ⧸ I)
⊢ ∃ n, p ^ n ≤ I
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Algebra.IsIntegral ℤ R
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : NeZero P
this : P ≠ ⊥
⊢ ¬under ℤ P = ⊥

Tactic:
contrapose this

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Algebra.IsIntegral ℤ R
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : NeZero P
this : under ℤ P = ⊥
⊢ P = ⊥
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 ∣ ↑(Ideal.absNorm (differentIdeal (𝓞 K) (𝓞 L))) * ↑(discr K).natAbs ^ finrank K L

Tactic:
← Int.mul_sign_self,

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 * (discr K).sign) ^ finrank K L
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)
  · rw [h, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff, spanNorm_eq_bot_iff.mp h]
  · exact h ▸ (eq_top_iff_one _).mpr <| le_spanNorm_spanNorm R T I <| (eq_top_iff_one _).mp h

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

Goal state before:
pp: 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 : CharZero 𝒪
⊢ ¬p ∣ discr K ↔ Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p})

Tactic:
not_dvd_discr_iff_forall_liesOver K 𝒪 hp

Goal state after:
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 : CharZero 𝒪
⊢ (∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P) ↔
    Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p})