mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K := ⋯
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
⊢ ∀ y ∈ ↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)),
    (restrictNormalHom ↥L'.toIntermediateField) σ • y = y

Tactic:
intro y

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
y : ↥L'.toIntermediateField
⊢ y ∈ ↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)) →
    (restrictNormalHom ↥L'.toIntermediateField) σ • y = y
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq✝ : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K := ⋯
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : Gal(K/k)
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
⊢ ∀ y ∈ ↑L'.toIntermediateField, (σ⁻¹ * h) • y = y

Tactic:
intro y

Goal state after:
case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq✝ : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : Gal(K/k)
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
y : K
⊢ y ∈ ↑L'.toIntermediateField → (σ⁻¹ * h) • y = y
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : IsPurelyInseparable (↥L) E
y : ↥L
hx : (algebraMap (↥L) E) y ∈ separableClosure F E
⊢ (algebraMap (↥L) E) y ∈ L

Tactic:
exact y.2

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E ↑S
this✝³ : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x✝¹ : Algebra ↥S ↥L := i.toAlgebra
this✝² : IsScalarTower (↥S) (↥L) K
this✝¹ : Algebra.IsAlgebraic F K
this✝ : IsPurelyInseparable (↥S) K
this : IsPurelyInseparable (↥L) K
y : ↥L
x✝ : (algebraMap (↥L) K) y ∈ ⊤
⊢ (algebraMap (↥L) K) y ∈ L

Tactic:
exact y.2

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
⊢ IsLocalization (algebraMapSubmonoid C A⁰) L

Tactic:
by
  have : IsDomain C :=
    (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
  have : IsTorsionFree A L := .trans_faithfulSMul A K L
  have : IsTorsionFree A C := IsIntegralClosure.isTorsionFree A L
  refine ⟨?_, fun z => ?_, fun {x y} h => ⟨1, ?_⟩⟩
  · rintro ⟨_, x, hx, rfl⟩
    rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L),
      Subtype.coe_mk, map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective A C)]
    exact mem_nonZeroDivisors_iff_ne_zero.mp hx
  · obtain ⟨m, hm⟩ :=
      IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z
        (Algebra.IsIntegral.isIntegral (R := K) z)
    obtain ⟨x, hx⟩ : ∃ x, algebraMap C L x = m • z := IsIntegralClosure.isIntegral_iff.mp hm
    refine ⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, ?_⟩
    rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]
  · simp only [IsIntegralClosure.algebraMap_injective C A L h]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁷ : Group G
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : IsGaloisGroup G A B
g : G
x✝ : ↥(algebraMap A B).range
b a' : B
a : A
ha : (algebraMap A B) a = a'
⊢ g • ⟨a', ⋯⟩ • b = ⟨a', ⋯⟩ • g • b

Tactic:
by simp [Subring.smul_def, ← ha]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ (Algebra.trace K ↥K⟮x⟯) (gen K x) = 0

Tactic:
rw [trace_eq_zero_of_not_exists_basis, LinearMap.zero_apply]
  contrapose hx
  obtain ⟨s, ⟨b⟩⟩ := hx
  refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
  · exact (Submodule.fg_iff_finiteDimensional _).mpr (b.finiteDimensional_of_finite)
  · exact subset_adjoin K _ (Set.mem_singleton x)

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

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
hP : Q.LiesOver P
hQ : Q.IsPrime
⊢ MulAction.orbit G Q = P.primesOver B

Tactic:
refine Set.ext fun R ↦ ⟨fun ⟨g, hg⟩ ↦ hg ▸ ⟨hQ.smul g, hP.smul g⟩, fun h ↦ ?_⟩
  have : R.IsPrime := h.1
  obtain ⟨g, hg⟩ := exists_smul_of_under_eq A B G Q R (hP.over.symm.trans h.2.over)
  exact ⟨g, hg.symm⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ ∀ x_1 ∈ (minpoly L x).aroots (AlgebraicClosure F), IsIntegral R x_1

Tactic:
intro y

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
⊢ y ∈ (minpoly L x).aroots (AlgebraicClosure F) → IsIntegral R y
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen

Tactic:
intro σ
    simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.domRestrict, AlgHom.comp_apply,
      IsScalarTower.coe_toAlgHom']

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

Goal state before:
pp: ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
| ∑ j, of (fun i j ↦ (trace A B) (b i * b j)) i j * b.equivFun z j

Tactic:
congr
    rfl
    ext
    rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← map_smul]

Goal state after:
case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i x✝ : ι
| (trace A B) (b.equivFun z x✝ • (b i * b x✝))
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ Nat.card K - 1 ∣ i

Tactic:
← Nat.card_units,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ Nat.card Kˣ ∣ i
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : Ms i ⧸ p i
⊢ (quotientPiLift p (fun i ↦ (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) (Pi.single i x) =
    LinearMap.id (Pi.single i x)

Tactic:
induction x using Submodule.Quotient.induction_on with | _ x'

Goal state after:
case H
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x' : Ms i
⊢ (quotientPiLift p (fun i ↦ (p i).mkQ) ⋯ ∘ₗ piQuotientLift p (pi Set.univ p) (single R Ms) ⋯)
      (Pi.single i (Quotient.mk x')) =
    LinearMap.id (Pi.single i (Quotient.mk x'))
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: case H
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x' : Ms i
j : ι
⊢ (quotientPiLift p (fun i ↦ (p i).mkQ) ⋯)
      ((piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) (Pi.single i (Quotient.mk x'))) j =
    LinearMap.id (Pi.single i (Quotient.mk x')) j

Tactic:
piQuotientLift_single,

Goal state after:
case H
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x' : Ms i
j : ι
⊢ (quotientPiLift p (fun i ↦ (p i).mkQ) ⋯) (((p i).mapQ (pi Set.univ p) (single R Ms i) ⋯) (Quotient.mk x')) j =
    LinearMap.id (Pi.single i (Quotient.mk x')) j
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:

Tactic:
_ = (LinearMap.det (N.subtype ∘ₗ
            (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N))).natAbs := rfl
      _ = (LinearMap.det (N.subtype ∘ₗ _)).natAbs :=
            Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _)
      _ = Nat.card (M ⧸ N) := this

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : g ^ (n * (Nat.card F / 2)) = 1
⊢ Nat.card F - 1 ∣ n * (Nat.card F / 2)

Tactic:
← Nat.card_units,

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : g ^ (n * (Nat.card F / 2)) = 1
⊢ Nat.card Fˣ ∣ n * (Nat.card F / 2)
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen

Tactic:
intro σ
    simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.domRestrict, AlgHom.comp_apply,
      IsScalarTower.coe_toAlgHom']

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
J : Ideal S
⊢ (toAddSubgroup I).IsFiniteRelIndex (toAddSubgroup J)

Tactic:
have := finiteIndex hI
  exact isFiniteRelIndex_of_finiteIndex

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm (P * I))
⊢ ∃ P_1, P_1.IsMaximal ∧ under ℤ P_1 = span {p} ∧ P_1 ∣ P * I

Tactic:
simp only [_root_.map_mul, Nat.cast_mul, hp.dvd_mul] at hI
    cases hI with
    | inr h =>
      obtain ⟨Q, h₁, h₂, h₃⟩ := IH h
      exact ⟨Q, h₁, h₂, dvd_mul_of_dvd_right h₃ _⟩
    | inl hI =>
      have := (Ideal.isPrime_of_prime hP).isMaximal hP.ne_zero
      refine ⟨P, this, (hpMax.eq_of_le (by simpa using this.ne_top) ?_).symm, dvd_mul_right _ _⟩
      obtain ⟨q, n, hn, hqP, hq, H⟩ := Ideal.exists_prime_and_absNorm_eq_pow P
      rw [H, Nat.cast_pow, dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)] at hI
      obtain ⟨m, hmn, hp⟩ := hI
      rw [Ideal.span_singleton_le_iff_mem]
      have : m ≠ 0 := fun h ↦ hpMax.ne_top (Ideal.span_singleton_eq_top.mpr (by simpa [h] using hp))
      exact Ideal.mem_of_dvd _ hp.symm.dvd (Ideal.pow_mem_of_mem _ (by simpa) _ this.bot_lt)

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case succ.zero
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ^ 0 ≤ Module.annihilator R M → P M
hn : Jac ^ (0 + 1) ≤ Module.annihilator R M
⊢ P M

Tactic:
rw [Jac.pow_one] at hn; exact this hn

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
⊢ f ⁻¹' closedPoints Y = closedPoints X

Tactic:
apply subset_antisymm (preimage_closedPoints_subset hf.injective hf.continuous)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
⊢ closedPoints X ⊆ f ⁻¹' closedPoints Y
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1

Tactic:
have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOfPred_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOfPred_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
    (fun I ↦ absNorm I ≤ n))]
  let e : {I : Ideal S // absNorm I ≤ n} ≃ {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} ⊕
      {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} := by
    refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)
    · intro _
      simp_rw [← or_and_right, em, true_and]
    · exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)
  simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]
  conv_lhs =>
    enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]
  rw [Nat.card_unique]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
⊢ IsSimpleModule B (↥q ⧸ f.range)

Tactic:
range_inclusion,

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
⊢ IsSimpleModule B (↥q ⧸ comap q.subtype p)
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
f : ↥p →ₗ[A] ↥q := inclusion ⋯
⊢ IsSimpleModule A (↥q ⧸ f.range)

Tactic:
range_inclusion,

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
f : ↥p →ₗ[A] ↥q := inclusion ⋯
⊢ IsSimpleModule A (↥q ⧸ comap q.subtype p)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hp_bot : map f p ≠ ⊥
hvp : ¬v = p
⊢ emultiplicity w (map f p) = ↑(v.ramificationIdx' w) * emultiplicity v p

Tactic:
· rw [emultiplicity_eq_zero_of_irreducible_ne hv hp.irreducible hvp, mul_zero,
      emultiplicity_map_eq_zero_of_ne hv hp hvp]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
⊢ (∀ (b : { I // I.IsPrime }),
      (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(PrimeSpectrum.equivSubtype R).symm b}).Finite) ↔
    ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite

Tactic:
Subtype.forall

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩}).Finite) ↔
    ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
⊢ ∀ {x₁ x₂ : Localization.AtPrime p}, LinearMap.id x₁ = LinearMap.id x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
simpa using ⟨1, p.primeCompl.one_mem⟩

Goal state after: