mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  ((torsion K).equivMapOfInjective (Units.complexEmbedding φ) ⋯).symm.toEquiv
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))

Tactic:
Complex.card_rootsOfUnity,

Goal state after:
case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  ((torsion K).equivMapOfInjective (Units.complexEmbedding φ) ⋯).symm.toEquiv
⊢ torsionOrder K ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
this : Fintype ↥(torsion K) := Fintype.ofFinite ↥(torsion K)
⊢ 1 ≠ ⟨-1, ⋯⟩

Tactic:
by simp [← Subtype.coe_ne_coe]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ M = N.transpose

Tactic:
{

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ M = N.transpose
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
F : Type u_3
inst✝ : Field F
w : InfinitePlace K
f : k →+* K
⊢ place (w.embedding.comp f) = (↑w).comp ⋯

Tactic:
{

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
F : Type u_3
inst✝ : Field F
w : InfinitePlace K
f : k →+* K
⊢ place (w.embedding.comp f) = (↑w).comp ⋯
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1

Tactic:
trans Nat.card ({1} : Set Gal(K/k))

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = Nat.card ↑{1}

k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑{1} = 1
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

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:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective fun r ↦ r • 1

Tactic:
{

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective fun r ↦ r • 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
⊢ (negAt s).symm = negAt s

Tactic:
ext x w

Goal state after:
case fst
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
k : K
hk : (algebraMap K L) k = (algebraMap B L) b
hb : IsIntegral A b
⊢ ∃ a, (algebraMap A B) a = b

Tactic:
← isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective B L),

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
k : K
hk : (algebraMap K L) k = (algebraMap B L) b
hb : IsIntegral A ((algebraMap B L) b)
⊢ ∃ a, (algebraMap A B) a = b
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Group G
inst✝¹⁰ : MulSemiringAction G S
inst✝⁹ : IsGaloisGroup G R S
inst✝⁸ : Finite G
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Flat R S
p : Ideal R
P : Ideal S
inst✝³ : P.LiesOver p
inst✝² : p.IsPrime
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
H : Nat.card ↥(inertia G P) * p.inertiaDegIn S = p.ramificationIdxIn S * p.inertiaDegIn S
h1 : (p.primesOver S).ncard ≠ 0
h2 : p.inertiaDegIn S ≠ 0
⊢ Nat.card ↥(inertia G P) = p.ramificationIdxIn S

Tactic:
mul_left_inj' h2

Goal state after:
R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Group G
inst✝¹⁰ : MulSemiringAction G S
inst✝⁹ : IsGaloisGroup G R S
inst✝⁸ : Finite G
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Flat R S
p : Ideal R
P : Ideal S
inst✝³ : P.LiesOver p
inst✝² : p.IsPrime
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
H : Nat.card ↥(inertia G P) = p.ramificationIdxIn S
h1 : (p.primesOver S).ncard ≠ 0
h2 : p.inertiaDegIn S ≠ 0
⊢ Nat.card ↥(inertia G P) = p.ramificationIdxIn S
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0

Tactic:
let e : (N ⧸ (I • N).comap N.subtype) ≃ₗ[R] (R ⧸ I) ⊗[R] N :=
    Submodule.quotEquivOfEq _ (I • (⊤ : Submodule R N)) (Submodule.map_injective_of_injective
      N.injective_subtype (by simp [Submodule.smul_le_right])) ≪≫ₗ
        (quotTensorEquivQuotSMul N I).symm

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
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:
{

Goal state after:
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)
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:
{

Goal state after:
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
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: 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ₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) ((intTrace Rₚ Sₚ) ((algebraMap S Sₚ) x)) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))

Tactic:
← Algebra.intTrace_eq_of_isLocalization R S p.primeCompl (Aₘ := Rₚ) (Bₘ := Sₚ) x,

Goal state after:
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ₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) ((algebraMap R Rₚ) ((intTrace R S) x)) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
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 : ι
⊢ (Ideal.Quotient.mk pS) x =
    (Fintype.linearCombination (R ⧸ p) ⇑(basisQuotient b)) (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x))

Tactic:
Fintype.linearCombination_apply

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 : ι
⊢ (Ideal.Quotient.mk pS) x = ∑ i, (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)) i • (basisQuotient b) i
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case refine_1
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ Submodule.toAddSubgroup 1 ≤ (↑(FractionalIdeal.dual ℤ ℚ 1)).toAddSubgroup

Tactic:
rw [Submodule.toAddSubgroup_le, ← FractionalIdeal.coe_one]

Goal state after:
case refine_1
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ ↑1 ≤ ↑(FractionalIdeal.dual ℤ ℚ 1)

K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := ⋯
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := ⋯
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ Submonoid 𝒪
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ insert i (t ∪ u) = insert i s

Tactic:
htus

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ insert i s = insert i s
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
⊢ p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)

Tactic:
have aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n := by grind

Goal state after:
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
⊢ p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = b * d
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ insert i (t ∪ u) = insert i s

Tactic:
htus

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = b * d
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ insert i s = insert i s
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) - p • ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) =
    (algebraMap R K) p ^ n.succ * (algebraMap R K) r

Tactic:
← smul_sub,

Goal state after:
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, Q.coeff x • f (x + n))) =
    (algebraMap R K) p ^ n.succ * (algebraMap R K) r
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case pos.inr
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
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H₁ : z = 0
⊢ z ∈ R[B.gen]

Tactic:
· rw [H₁]
      exact Subalgebra.zero_mem _

Goal state after: