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

Goal state before:
pp: case intro
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 Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
val✝ : Fintype G
this : ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g ∈ ⊤, Q ≤ g • P
g : G
hg : Q ≤ g • P
⊢ ∃ g, Q = g • P

Tactic:
obtain ⟨g', -, hg'⟩ := this Q (g • P) ((P.under_smul A g).trans hPQ).symm

Goal state after:
case intro
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 Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
val✝ : Fintype G
this : ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g ∈ ⊤, Q ≤ g • P
g : G
hg : Q ≤ g • P
g' : G
hg' : g • P ≤ g' • Q
⊢ ∃ g, Q = g • P
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 K F
inst✝ : FiniteDimensional K L
x : L
hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ (algebraMap ℕ K) (finrank (↥K⟮x⟯) L) • ((minpoly K x).aroots F).sum = finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum

Tactic:
IsScalarTower.algebraMap_smul

Goal state after:
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 K F
inst✝ : FiniteDimensional K L
x : L
hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum = finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ False

Tactic:
← a.valMinAbs_nonneg_iff,

Goal state after:
n : ℕ
a : ZMod (n + 1)
h : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ False
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩
    · linarith only [h]
    · grind

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ -↑n ≤ -(↑x.valMinAbs.natAbs * 2)

Tactic:
← neg_mul,

Goal state after:
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ -↑n ≤ -↑x.valMinAbs.natAbs * 2
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case refine_2
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ x ∈ FixedPoints.intermediateField ↥H

Tactic:
have := congr_arg (restrictScalars K) <| IsGaloisGroup.fixedPoints_eq_bot H F L

Goal state after:
case refine_2
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
this : IntermediateField.restrictScalars K (FixedPoints.intermediateField ↥H) = IntermediateField.restrictScalars K ⊥
⊢ x ∈ FixedPoints.intermediateField ↥H
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case h.inl
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

Tactic:
rw [hu']
      simp

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

Goal state before:
pp: case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

Tactic:
rw [hu']
      simp

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

Goal state before:
pp: a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : a = d ^ k ∨ a = -d ^ k
⊢ ∃ d, a = d ^ k

Tactic:
← hk.neg_pow

Goal state after:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : a = d ^ k ∨ a = (-d) ^ k
⊢ ∃ d, a = d ^ k
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : frobeniusAlgHom K L ^ m = 1
x : L
x✝ : x ∈ univ.val
this : (frobeniusAlgHom K L ^ m) x = 1 x
⊢ X ^ q ^ m - X ≠ 0 ∧ x ^ q ^ m - x = 0

Tactic:
rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply, ← sub_eq_zero] at this

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : frobeniusAlgHom K L ^ m = 1
x : L
x✝ : x ∈ univ.val
this : (fun x ↦ x ^ q ^ m) x - x = 0
⊢ X ^ q ^ m - X ≠ 0 ∧ x ^ q ^ m - x = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]

Tactic:
simpa [← ZMod.intCast_eq_intCast_iff] using ZMod.pow_card_sub_one_eq_one this

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
x : M
⊢ ∀ (c : ι → R) (i : ι), (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i

Tactic:
intro c i

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
x : M
c : ι → R
i : ι
⊢ (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
⊢ Nat.card (ZMod p) = p

Tactic:
Nat.card_zmod

Goal state after:
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
⊢ p = p
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mp
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 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x ↦ g ^ x) n = y * y
⊢ y ^ (2 * (Fintype.card F / 2)) = 1

Tactic:
hodd

Goal state after:
case mp
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 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x ↦ g ^ x) n = y * y
⊢ y ^ (Fintype.card F - 1) = 1
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: case calc_1
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
i j : Free.ChooseBasisIndex ℤ M
⊢ (LinearMap.toMatrix b' b') f i j = Matrix.diagonal a i j

Tactic:
rw [LinearMap.toMatrix_apply, ha, map_smul, Basis.repr_self, Finsupp.smul_single,
      smul_eq_mul, mul_one]

Goal state after:
case calc_1
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
i j : Free.ChooseBasisIndex ℤ M
⊢ (Finsupp.single j (a j)) i = Matrix.diagonal a i j
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_notMem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ d - d' ∈ P

Tactic:
by
  have h' : a * (d - d') ∈ P ^ (i + 1) := by
    convert! Ideal.add_mem _ h (Ideal.sub_mem _ e'_mem e_mem) using 1
    ring
  exact Ideal.mem_prime_of_mul_mem_pow hP a_notMem h'

Goal state after:
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
this : ∀ (i : ℕ), Module.Finite R (S ⧸ I ^ i)
n : ℕ
hn : I ^ n = ⊥
⊢ Module.Finite R S

Tactic:
let e : (S ⧸ I ^ n) ≃ₐ[R] S := hn ▸ (AlgEquiv.quotientBot R S)

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
this : ∀ (i : ℕ), Module.Finite R (S ⧸ I ^ i)
n : ℕ
hn : I ^ n = ⊥
e : (S ⧸ I ^ n) ≃ₐ[R] S := ⋯ ▸ AlgEquiv.quotientBot R S
⊢ Module.Finite R S
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝¹ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this✝ : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
ψ : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1) :=
  (I • ⊤).liftQ (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n)) ⋯ ∘ₗ ↑(quotTensorEquivQuotSMul (↥(I ^ n)) I)
e_3✝ : inst✝⁵.toSemiring = CommRing.toCommSemiring.toSemiring
e_4✝ : (Submodule.Quotient.addCommGroup (I ^ (n + 1))).toAddCommMonoid = Submodule.Quotient.addCommMonoid (I ^ (n + 1))
e_5✝ : Submodule.Quotient.module' (I ^ (n + 1)) ≍ Submodule.Quotient.module' (I ^ (n + 1))
this : φ.toLinearMap.ker = Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n)
⊢ ⊤ ⊓ (↑R φ.toLinearMap).ker = Submodule.map (↑R ψ) ⊤

Tactic:
simpa [LinearMap.range_restrictScalars, ψ, LinearMap.range_comp, Submodule.range_liftQ]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ (toPiLocalization R) (r * r) = (toPiLocalization R) r

Tactic:
simp [map_mul, hr, ← Pi.single_mul]

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
⊢ cardQuot 0 = 0

Tactic:
have : Infinite S := Module.Free.infinite ℤ S
    rw [Ideal.zero_eq_bot, cardQuot_bot]

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R₀ M
inst✝² : Module R M
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
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
hn : Jac ^ n ≤ Module.annihilator R 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
⊢ P M

Tactic:
induction n generalizing M with
  | zero => rw [Jac.pow_zero, Ideal.one_eq_top] at hn; exact this (le_top.trans hn)
  | succ n ih => ?_

Goal state after:
case succ
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
n : ℕ
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ^ n ≤ 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
hn : Jac ^ (n + 1) ≤ Module.annihilator R M
⊢ P M
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ ((Algebra.norm ℤ) ↑n).natAbs ≠ 0

Tactic:
simpa only [Ne, Int.natAbs_eq_zero, Algebra.norm_eq_zero_iff, Nat.cast_eq_zero] using
        ne_of_gt hn

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
⊢ ∀ (x : ↥(U j)), x ∉ Subtype.val ⁻¹' {↑y}

Tactic:
intro z (hz : z.1 = y.1)

Goal state after:
case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
z : ↥(U j)
hz : ↑z = ↑y
⊢ False
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Ring.KrullDimLE 0 R
eq : Ring.jacobson R = nilradical R
Spec : Set (Ideal R) := {I | I.IsPrime}
this✝¹ : Finite ↑Spec
this✝ : ∀ (I : ↑Spec), (↑I).IsPrime
this : ∀ (I : ↑Spec), IsSemisimpleRing (R ⧸ ↑I)
⊢ IsSemisimpleRing (R ⧸ Ring.jacobson R)

Tactic:
by
    rw [eq, nilradical_eq_sInf, sInf_eq_iInf']
    exact (Ideal.quotientInfRingEquivPiQuotient _ fun I J ne ↦
      Ideal.isCoprime_of_isMaximal <| Subtype.coe_ne_coe.mpr ne).symm.isSemisimpleRing

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
h : IsNoetherian A M ∧ IsArtinian A M
⊢ IsNoetherian B M ∧ IsArtinian B M

Tactic:
exact h.imp (isNoetherian_of_tower A) (isArtinian_of_tower A)

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

Goal state before:
pp: case neg
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
h : length B M = ⊤
this : length A M = ⊤
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

Tactic:
have ne : length (ResidueField A) (ResidueField B) ≠ 0 := by
      simpa [pos_iff_ne_zero] using Module.length_pos

Goal state after:
case neg
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
h : length B M = ⊤
this : length A M = ⊤
ne : length (ResidueField A) (ResidueField B) ≠ 0
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

Tactic:
by
  by_cases hr : r.IsPrime
  · have : q.IsPrime := isPrime_of_liesOver r q
    have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
    let := Localization.AtPrime.algebraOfLiesOver (r.under R) r
    let := Localization.AtPrime.algebraOfLiesOver (r.under R) q
    let := Localization.AtPrime.algebraOfLiesOver q r
    rw [inertiaDeg_def, inertiaDeg_eq (r.under R), inertiaDeg_eq q, eq_comm]
    apply Module.finrank_mul_finrank
  · rw [inertiaDeg_of_not_isPrime r R hr, inertiaDeg_of_not_isPrime r S hr, mul_zero]

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

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
⊢ g₁ = g₂

Tactic:
have (i : ℕ) :
      (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂ := by
    by_cases hi : i = 0
    · ext x
      have : Subsingleton (B ⧸ I ^ i) := by
        rw [hi, pow_zero, Ideal.one_eq_top]
        infer_instance
      exact Subsingleton.elim _ _
    apply ext (I.map (algebraMap _ _)) ⟨i, by simp [← Ideal.map_pow]⟩
    intro x
    dsimp
    rw [Ideal.Quotient.eq, ← map_sub, ← Ideal.mem_comap, Ideal.comap_map_of_surjective',
      sup_eq_left.mpr, ← Ideal.Quotient.eq]
    · exact H _
    · simpa using Ideal.pow_le_self hi
    · exact Ideal.Quotient.mk_surjective

Goal state after:
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
⊢ g₁ = g₂
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
I : Ideal R
hI : I.IsPrime
J : Ideal S
⊢ J ∈ (fun x ↦ x.asIdeal) '' PrimeSpectrum.comap (algebraMap R S) ⁻¹' {(PrimeSpectrum.equivSubtype R).symm ⟨I, hI⟩} ↔
    J ∈ I.primesOver S

Tactic:
simp [(PrimeSpectrum.equivSubtype S).exists_congr_left, PrimeSpectrum.ext_iff, eq_comm,
    PrimeSpectrum.equivSubtype, Ideal.primesOver, and_comm, Ideal.liesOver_iff, Ideal.under]

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
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
⊢ ∀ (r : R),
    (↑↑(Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq)).toFun
        ((algebraMap R (Localization.AtPrime p)) r) =
      (algebraMap R (Localization.AtPrime q)) r

Tactic:
by
      simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime p),
        IsScalarTower.algebraMap_apply R (A ⊗[R] S) (Localization.AtPrime q)]

Goal state after: