mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_2
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
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥A⁰
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L) x = m • z
⊢ ∃ x, z * (algebraMap C L) ↑x.2 = (algebraMap C L) x.1

Tactic:
refine ⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, ?_⟩

Goal state after:
case refine_2
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
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥A⁰
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L) x = m • z
⊢ z * (algebraMap C L) ↑(x, ⟨(algebraMap A C) ↑m, ⋯⟩).2 = (algebraMap C L) (x, ⟨(algebraMap A C) ↑m, ⋯⟩).1
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : L →ₐ[K] E), x pb.gen = _root_.id ↑(pb.liftEquiv' x)

Tactic:
intro σ
    rw [PowerBasis.liftEquiv'_apply_coe, id_def]

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

Goal state before:
pp: case refine_2
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
⊢ (h • (a - eval b r) - if h • Q = Q then a else 0) ∈ Q

Tactic:
← Ideal.smul_mem_pointwise_smul_iff (a := h⁻¹),

Goal state after:
case refine_2
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
⊢ h⁻¹ • (h • (a - eval b r) - if h • Q = Q then a else 0) ∈ h⁻¹ • Q
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
m : ℕ
hg₂ : (expand K (p ^ m)) g = minpoly K x
⊢ ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = 0 x

Tactic:
cases m with

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

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
g : G
⊢ (algebraMap B (B ⧸ Q)) (g • (b * b₀)) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)

Tactic:
smul_mul',

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
g : G
⊢ (algebraMap B (B ⧸ Q)) (g • b * g • b₀) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
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 ↦ ((traceForm A B) (b i)) (b j)) i j * replicateCol (Fin 1) (b.equivFun z) j 0 =
    (trace A B) (z * b i)

Tactic:
simp only [replicateCol_apply, traceForm_apply]

Goal state after:
ι : 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 = (trace A B) (z * b i)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case e_6
ι : 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, b i * b.equivFun z x • b x = z * b i

Tactic:
← Finset.mul_sum,

Goal state after:
case e_6
ι : 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 : ι
⊢ b i * ∑ i, b.equivFun z i • b i = z * b i
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
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ (traceMatrix K b).map ⇑(algebraMap K E) = embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ

Tactic:
by
  rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply,
    transpose_submatrix, ← submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]

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

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ ∑ x, ↑↑x ^ k = 0

Tactic:
Finset.sum_eq_multiset_sum

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case refine_1
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
x : L
⊢ x ^ q ^ Module.finrank K L = 1 x

Tactic:
AlgHom.one_apply,

Goal state after:
case refine_1
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
x : L
⊢ x ^ q ^ Module.finrank K L = x
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 : (fun x ↦ x ^ q ^ m) x = 1 x
⊢ X ^ q ^ m - X ≠ 0 ∧ x ^ q ^ m - x = 0

Tactic:
AlgHom.one_apply,

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
⊢ X ^ q ^ m - X ≠ 0 ∧ x ^ q ^ m - x = 0
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
⊢ Squarefree ↑n ∨ ↑n = 0 ↔ Squarefree n ∨ n = 0

Tactic:
Int.squarefree_natCast,

Goal state after:
n : ℕ
⊢ Squarefree n ∨ ↑n = 0 ↔ Squarefree n ∨ n = 0
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)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ (piQuotientLift p q f hf) (Pi.single i x) = ((p i).mapQ q (f i) ⋯) x

Tactic:
by
  simp_rw [piQuotientLift, lsum_apply, sum_apply, comp_apply, proj_apply]
  rw [Finset.sum_eq_single i]
  · rw [Pi.single_eq_same]
  · rintro j - hj
    rw [Pi.single_eq_of_ne hj, map_zero]
  · intros
    have := Finset.mem_univ i
    contradiction

Goal state after:
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
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ Fintype.card ↥⊥ = p

Tactic:
Fintype.card_eq_nat_card,

Goal state after:
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ Nat.card ↥⊥ = p
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: 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
⊢ (Matrix.diagonal a).det.natAbs = (∏ i, a i).natAbs

Tactic:
Matrix.det_diagonal

Goal state after:
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, a i).natAbs = (∏ i, a i).natAbs
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
⊢ ↑(L₁.relIndex L₂) = |b₂.det ⇑b₁|

Tactic:
rw [AddSubgroup.relIndex_eq_natAbs_det L₁ L₂ H (b₁.addSubgroupOfClosure L₁ h₁)
    (b₂.addSubgroupOfClosure L₂ h₂), Nat.cast_natAbs, Int.cast_abs]

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range ⇑b₁)
h₂ : L₂ = closure (Set.range ⇑b₂)
⊢ |↑((Basis.addSubgroupOfClosure L₂ b₂ h₂).det fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩)| = |b₂.det ⇑b₁|
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case succ.refine_2.h
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
hd' : (mkQ (P ^ i.succ)) (a * d) ∈ map (mkQ (P ^ i.succ)) (P ^ i)
⊢ a * f (k ((mkQ (P ^ i.succ)) (a * d)) ⋯) ⋯ + g (k ((mkQ (P ^ i.succ)) (a * d)) hd') ⋯ - (a * d + 0) ∈ P ^ (i + 1)

Tactic:
rw [hf, add_zero]

Goal state after:
case succ.refine_2.h
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
hd' : (mkQ (P ^ i.succ)) (a * d) ∈ map (mkQ (P ^ i.succ)) (P ^ i)
⊢ k ((mkQ (P ^ i.succ)) (a * d)) ⋯ - a * d ∈ P ^ (i + 1)
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) ∨ p ∣ ↑(absNorm I)
⊢ ∃ P_1, P_1.IsMaximal ∧ under ℤ P_1 = span {p} ∧ P_1 ∣ P * I

Tactic:
cases hI with

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
⊢ closure[inst✝¹] (S ∩ closedPoints X) = closure[inst✝¹] S

Tactic:
by
  refine (closure_mono (Set.inter_subset_left)).antisymm ?_
  rw [IsClosed.closure_subset_iff isClosed_closure]
  intro x hx
  by_contra H
  obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := nonempty_inter_closedPoints (Z := S \ closure (S ∩ closedPoints X))
    ⟨x, hx, H⟩ (.inter hS isClosed_closure.isOpen_compl.isLocallyClosed)
  exact hy₂ (subset_closure ⟨hy₁, hy₃⟩)

Goal state after:
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:
eq,

Goal state after:
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 ⧸ nilradical R)
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos.zero
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 : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length A ↥(s.toFun 0) = ↑↑0 * length (ResidueField A) (ResidueField B)

Tactic:
rw [← RelSeries.head, hs_bot]; simp

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✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = ↑s.length * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top, baseChange_top, length_top]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ Multiset.count P (normalizedFactors (map f p)) • {P} ≤ normalizedFactors (map f p)

Tactic:
Multiset.nsmul_singleton,

Goal state after:
case refine_1
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ Multiset.replicate (Multiset.count P (normalizedFactors (map f p))) P ≤ normalizedFactors (map f p)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case refine_2
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬(Multiset.count P (normalizedFactors (map f p)) + 1) • {P} ≤ normalizedFactors (map f p)

Tactic:
Multiset.nsmul_singleton,

Goal state after:
case refine_2
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬Multiset.replicate (Multiset.count P (normalizedFactors (map f p)) + 1) P ≤ normalizedFactors (map f p)
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case mp.refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
x : S ⊗[R] S
hx : 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 = e * x
⊢ (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0

Tactic:
rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i : I
⊢ ((f.sum fun i_1 y ↦ (a i_1) i • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b i) =
    f.sum fun i_1 y ↦ (b.repr y).sum fun j z ↦ (a i_1) i • z • b j ⊗ₜ[R] b i

Tactic:
Finsupp.sum_sum_index

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i : I
⊢ (f.sum fun a_1 b_1 ↦ ((a a_1) i • b.repr b_1).sum fun j z ↦ z • b j ⊗ₜ[R] b i) =
    f.sum fun i_1 y ↦ (b.repr y).sum fun j z ↦ (a i_1) i • z • b j ⊗ₜ[R] b i

case h_zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i : I
⊢ ∀ (a : I), 0 • b a ⊗ₜ[R] b i = 0

case h_add
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i : I
⊢ ∀ (a : I) (b₁ b₂ : R), (b₁ + b₂) • b a ⊗ₜ[R] b i = b₁ • b a ⊗ₜ[R] b i + b₂ • b a ⊗ₜ[R] b i
Module: Mathlib.RingTheory.QuasiFinite.Basic

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
inst✝¹ : QuasiFinite R S
inst✝ : QuasiFinite S T
P : Ideal R
hP : P.IsPrime
this✝ : Module.Finite (P.Fiber S) (P.Fiber S ⊗[S] T)
this : Module.Finite P.ResidueField (P.Fiber S ⊗[S] T)
e : P.Fiber S ≃ₐ[S] S ⊗[R] P.ResidueField :=
  let __spread.0 := TensorProduct.comm R P.ResidueField S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : P.Fiber S ⊗[S] T ≃ₐ[R] P.Fiber T :=
  (AlgEquiv.restrictScalars R (TensorProduct.congr e AlgEquiv.refl)).trans
    ((AlgEquiv.restrictScalars R (TensorProduct.comm S (S ⊗[R] P.ResidueField) T)).trans
      ((AlgEquiv.restrictScalars R (TensorProduct.cancelBaseChange R S T T P.ResidueField)).trans
        (TensorProduct.comm R T P.ResidueField)))
x✝ : P.ResidueField
⊢ e'.toFun ((algebraMap P.ResidueField (P.Fiber S ⊗[S] T)) x✝) = (algebraMap P.ResidueField (P.Fiber T)) x✝

Tactic:
by simp [e', e]

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
⊢ QuasiFiniteAt A q

Tactic:
by
  let f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
    Algebra.TensorProduct.lift (Algebra.ofId _ _) ⟨Localization.localRingHom _ _ _ hq, by
      simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime p),
        IsScalarTower.algebraMap_apply R (A ⊗[R] S) (Localization.AtPrime q)]⟩ fun _ _ ↦ .all _ _
  let g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
    Algebra.TensorProduct.map (.id _ _) (IsScalarTower.toAlgHom _ _ _)
  have : f.comp g = IsScalarTower.toAlgHom _ _ _ := by ext; simp [f, g]
  replace this (x : _) : f (g x) = algebraMap _ _ x := DFunLike.congr_fun this x
  refine .of_forall_exists_mul_mem_range f fun x ↦ ?_
  obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
  refine ⟨g s, this s ▸ IsLocalization.map_units _ ⟨s, hs⟩, ?_⟩
  rw [this, IsLocalization.mk'_spec_mk]
  exact ⟨g x, this x⟩

Goal state after: