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

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ -(algebraMap F E) ((minpoly F x).coeff 0) = x ^ q ^ n

Tactic:
h,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ -(-1 * x ^ q ^ n) = x ^ q ^ n
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
m₀ : M
U : Set M
U_in : U ∈ BM.sets
V : Set R
V_in : V ∈ BR
H : V ⊆ (fun x ↦ x • m₀) ⁻¹' U
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) H

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set Gal(L/K)
⊢ s ∈ (galGroupBasis K L).filter → ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
rintro ⟨-, ⟨-, ⟨E, fin, rfl⟩, rfl⟩, hE⟩

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set Gal(L/K)
E : IntermediateField K L
fin : E ∈ finiteExts K L
hE : (fun g ↦ g.carrier) E.fixingSubgroup ⊆ s
⊢ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g

Tactic:
have hφx : φ x ≠ x := by
        apply ne_of_apply_ne f
        change f (f.symm (g x)) ≠ f x
        rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]
        exact hx

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' = L'.fixingSubgroup.index
⊢ finrank F ↥(restrict hle) = L.fixingSubgroup.index

Tactic:
h,

Goal state after:
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' = L'.fixingSubgroup.index
⊢ L'.fixingSubgroup.index = L.fixingSubgroup.index
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ map φ f = ?m.53 a b h * ?m.54 a b h

Tactic:
h,

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ map φ (a * b) = ?m.53 a b h * ?m.54 a b h
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
⊢ (Polynomial.map (algebraMap R K) p).leadingCoeff = 1

Tactic:
Monic.leadingCoeff (h.map <| algebraMap R K)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
⊢ 1 = 1
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case a.ind
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
⊢ i ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))

Tactic:
have : coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) ∈
        Submodule.span R (Set.range (coeff (minpolyDiv R x))) :=
      Submodule.subset_span (Set.mem_range_self _)

Goal state after:
case a.ind
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ i ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ IsUnit (map (algebraMap R K) (C ((integerNormalization R⁰ p).content * ↑u)))

Tactic:
isUnit_iff

Goal state after:
case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ ∃ r, IsUnit r ∧ C r = map (algebraMap R K) (C ((integerNormalization R⁰ p).content * ↑u))
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
h : n = 0
⊢ False

Tactic:
h,

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑0
h : n = 0
⊢ False
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
q : ℕ
inst✝² : ExpChar F✝ q
inst✝¹ : IsPurelyInseparable F✝ E
inst✝ : FiniteDimensional F✝ E
F : Type v
⊢ ∀ (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q]
    [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n

Tactic:
E

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
q : ℕ
inst✝² : ExpChar F✝ q
inst✝¹ : IsPurelyInseparable F✝ E✝
inst✝ : FiniteDimensional F✝ E✝
F E : Type v
⊢ ∀ [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E]
    [FiniteDimensional F E], ∃ n, finrank F E = q ^ n
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
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : f ((algebraMap F E) y) = g ((algebraMap F E) y)
⊢ f x = g x

Tactic:
h,

Goal state after:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
x : E
q : ℕ := ringExpChar F
n : ℕ
y : F
h : (algebraMap F E) y = x ^ q ^ n
heq : f (x ^ q ^ n) = g (x ^ q ^ n)
⊢ f x = g x
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
inst✝ : IsAlgClosure F E
H : separableClosure F E = ⊥
this : IsAlgClosed E
⊢ IsSepClosed F

Tactic:
IsSepClosed.separableClosure_eq_bot_iff

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosure F E
H : IsSepClosed F
this : IsAlgClosed E
⊢ IsSepClosed F
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral ℤ (f x)
⊢ restrict (⇑f) h 1 = 1

Tactic:
simp only [restrict, map_one]; rfl

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: 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
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
F : IntermediateField K L
⊢ Subgroup.map (↑(mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) = F.fixingSubgroup

Tactic:
by
  ext g
  obtain ⟨g, rfl⟩ := (mulEquivAlgEquiv G K L).surjective g
  simp [mem_fixingSubgroup_iff]

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

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
h : u = 1
⊢ 1 = orderOf u

Tactic:
h,

Goal state after:
case inl
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
h : u = 1
⊢ 1 = orderOf 1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ (x ^ i) ^ j = 1

Tactic:
h,

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ 1 ^ j = 1
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit ↑(a.gcd b)

Tactic:
h,

Goal state after:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit ↑1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ derivative (X ^ q) - derivative X = -1

Tactic:
derivative_X,

Goal state after:
case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ derivative (X ^ q) - 1 = -1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0

Tactic:
h,

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ ringChar F ^ ↑n % 2 = 0
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: case pos
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
h : i = j
⊢ (Finsupp.single j (a j)) i = Matrix.diagonal a i j

Tactic:
h,

Goal state after:
case pos
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
h : i = j
⊢ (Finsupp.single j (a j)) j = Matrix.diagonal a j j
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case pos
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ e ((norm A) x) = (norm B) x

Tactic:
Algebra.norm_eq_matrix_det b,

Goal state after:
case pos
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ e ((norm A) x) = ((leftMulMatrix b) x).det
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
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
⊢ (f '' {I | absNorm I = n}).Finite

Tactic:
let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))
        refine Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn
        exact Set.Finite.subset Set.finite_univ (Set.subset_univ _)

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_2
M✝ : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M✝
inst✝¹ : Module R M✝
inst✝ : IsSemiprimaryRing R
M : Type u
x✝³ : AddCommGroup M
x✝² x✝¹ : Module R M
x✝ : IsScalarTower R R M
h : IsNoetherian R ↥(Ring.jacobson R • ⊤) ↔ IsArtinian R ↥(Ring.jacobson R • ⊤)
h' : IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
N : Submodule R M := Ring.jacobson R • ⊤
⊢ IsNoetherian R ↥(Ring.jacobson R • ⊤) ∧ IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔
    IsArtinian R ↥(Ring.jacobson R • ⊤) ∧ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)

Tactic:
h,

Goal state after:
R : Type u_2
M✝ : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M✝
inst✝¹ : Module R M✝
inst✝ : IsSemiprimaryRing R
M : Type u
x✝³ : AddCommGroup M
x✝² x✝¹ : Module R M
x✝ : IsScalarTower R R M
h : IsNoetherian R ↥(Ring.jacobson R • ⊤) ↔ IsArtinian R ↥(Ring.jacobson R • ⊤)
h' : IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
N : Submodule R M := Ring.jacobson R • ⊤
⊢ IsArtinian R ↥(Ring.jacobson R • ⊤) ∧ IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔
    IsArtinian R ↥(Ring.jacobson R • ⊤) ∧ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos
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 = ⊤
⊢ ∀ (k : Fin (s.length + 1)), length A ↥(s.toFun k) = ↑↑k * length (ResidueField A) (ResidueField B)

Tactic:
intro k

Goal state after:
case pos
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 = ⊤
k : Fin (s.length + 1)
⊢ length A ↥(s.toFun k) = ↑↑k * length (ResidueField A) (ResidueField B)
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]

Goal state after:
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 ↥⊥ = ↑↑0 * length (ResidueField A) (ResidueField B)
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 = ⊤
ne : length (ResidueField A) (ResidueField B) ≠ 0
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

Tactic:
h,

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 (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
q : Ideal S
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Algebra R S
hq : q.IsPrime
inst✝ : Module.Finite R S
this : Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (under R q) q
⊢ 0 < q.inertiaDeg R

Tactic:
rw [inertiaDeg_def]

Goal state after:
S : Type u_1
inst✝³ : CommRing S
q : Ideal S
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Algebra R S
hq : q.IsPrime
inst✝ : Module.Finite R S
this : Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (under R q) q
⊢ 0 < Module.finrank (under R q).ResidueField q.ResidueField
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hle : map f p ≤ P ^ n
hgt : ¬map f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun m ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m
⊢ Q n

Tactic:
intro k

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hle : map f p ≤ P ^ n
hgt : ¬map f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun m ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m
k : ℕ
⊢ map f p ≤ P ^ k → k ≤ n
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos
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 = ⊤
⊢ ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
intro k

Goal state after:
case pos
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 = ⊤
k : Fin (s.length + 1)
⊢ length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))