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

Goal state before:
pp: case h
hp : Fact (Nat.Prime 2)
⊢ 0 ^ 2 + 1 ^ 2 = (fun i ↦ i) ⟨1, ⋯⟩

Tactic:
;

Goal state after:
case h
hp : Fact (Nat.Prime 2)
⊢ 0 ^ 2 + 1 ^ 2 = (fun i ↦ i) ⟨1, ⋯⟩
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x

Tactic:
;

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : (expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)
⊢ (expand (ZMod p) p) f = f ^ p

Tactic:
;

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : (expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)
⊢ (expand (ZMod p) p) f = f ^ p
Module: Mathlib.Data.ZMod.QuotientRing

Goal state before:
pp: n : ℕ
x✝ : ℤ
⊢ ((↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n))) x✝ = (Ideal.Quotient.mk (Ideal.span {↑n})) x✝

Tactic:
;

Goal state after:
n : ℕ
x✝ : ℤ
⊢ ((↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n))) x✝ = (Ideal.Quotient.mk (Ideal.span {↑n})) x✝
Module: Mathlib.Data.ZMod.QuotientRing

Goal state before:
pp: n x✝ : ℤ
⊢ ((↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs))) x✝ = (Ideal.Quotient.mk (Ideal.span {n})) x✝

Tactic:
;

Goal state after:
n x✝ : ℤ
⊢ ((↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs))) x✝ = (Ideal.Quotient.mk (Ideal.span {n})) x✝
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : F
⊢ (∃ a, { toFun := ⇑(castHom ⋯ F), inj' := ⋯ } a = x✝) ↔ x✝ ∈ (castHom ⋯ F).fieldRange

Tactic:
;

Goal state after:
K : Type u_1
R : Type u_2
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : F
⊢ (∃ a, { toFun := ⇑(castHom ⋯ F), inj' := ⋯ } a = x✝) ↔ x✝ ∈ (castHom ⋯ F).fieldRange
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Subgroup.zpowers g

Tactic:
;

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Subgroup.zpowers g
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
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
⊢ (fun x ↦ g ^ x) n ^ (Fintype.card F / 2) = 1 → IsSquare ((fun x ↦ g ^ x) n)

Tactic:
;

Goal state after:
case mpr
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
⊢ (fun x ↦ g ^ x) n ^ (Fintype.card F / 2) = 1 → IsSquare ((fun x ↦ g ^ x) n)
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
a : F
ha : a ≠ 0
y : Fˣ
hy : a = ↑y * ↑y
⊢ ∃ r, a = r * r

Tactic:
;

Goal state after:
case mp
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
y : Fˣ
hy : a = ↑y * ↑y
⊢ ∃ r, a = r * r
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
ha : 0 * 0 ≠ 0
⊢ False

Tactic:
;

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
ha : 0 * 0 ≠ 0
⊢ False
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy)

Tactic:
;

Goal state after:
case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy)
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
⊢ (LinearMap.toMatrix b' b') f = Matrix.diagonal a

Tactic:
;

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
⊢ (LinearMap.toMatrix b' b') f = Matrix.diagonal a
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
⊢ (norm R) 0 = 0

Tactic:
;

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
⊢ (norm R) 0 = 0
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₂)
⊢ (algebraMap ℤ ℚ).mapMatrix
      ((Basis.addSubgroupOfClosure L₂ b₂ h₂).toMatrix fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩) =
    b₂.toMatrix ⇑b₁

Tactic:
;

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₂)
⊢ (algebraMap ℤ ℚ).mapMatrix
      ((Basis.addSubgroupOfClosure L₂ b₂ h₂).toMatrix fun i ↦ ⟨↑((Basis.addSubgroupOfClosure L₁ b₁ h₁) i), ⋯⟩) =
    b₂.toMatrix ⇑b₁
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
L : Type u_7
inst✝² : DivisionRing L
inst✝¹ : Algebra K L
inst✝ : Module.Finite K L
x : L
⊢ (norm K) x⁻¹ = ((norm K) x)⁻¹

Tactic:
by_cases hx : x = 0
  · simp [hx]
  exact mul_left_injective₀ (norm_ne_zero_iff.mpr hx) (by simp [hx, ← map_mul])

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

Goal state before:
pp: case pos
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
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

pp: case neg
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
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

Tactic:
;

Goal state after:
case pos
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
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

case neg
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
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ (algebraMap R F) ((norm R) pb.gen) = ∏ σ, σ pb.gen

Tactic:
rw [PowerBasis.norm_gen_eq_prod_roots pb hE]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).prod = ∏ σ, σ pb.gen
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case hfg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
x : { x // x ∈ (minpoly R pb.gen).aroots F }
⊢ ↑x = _root_.id ↑x

Tactic:
;

Goal state after:
case hfg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
x : { x // x ∈ (minpoly R pb.gen).aroots F }
⊢ ↑x = _root_.id ↑x
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
σ : S →ₐ[R] F
⊢ σ pb.gen = ↑(pb.liftEquiv' σ)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
σ : S →ₐ[R] F
⊢ σ pb.gen = ↑(pb.liftEquiv' σ)
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ comap ((↑e).comp f) P = p ↔ comap (algebraMap R S₁) P = p

Tactic:
← e.toAlgHom_toRingHom,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ comap ((↑↑e).comp f) P = p ↔ comap (algebraMap R S₁) P = p
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P

Tactic:
rw [inertiaDeg'_algebraMap, inertiaDeg'_algebraMap]
    exact (Quotient.algEquivOfEqComap p e rfl).toLinearEquiv.finrank_eq

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ LinearMap.det ((lmul R T) (e x)) = LinearMap.det (↑↑e ∘ₗ (lmul R S) x ∘ₗ ↑(↑e).symm)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ LinearMap.det ((lmul R T) (e x)) = LinearMap.det (↑↑e ∘ₗ (lmul R S) x ∘ₗ ↑(↑e).symm)
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ (lmul R T) (e x) = ↑↑e ∘ₗ (lmul R S) x ∘ₗ ↑(↑e).symm

Tactic:
;

Goal state after:
case e_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ (lmul R T) (e x) = ↑↑e ∘ₗ (lmul R S) x ∘ₗ ↑(↑e).symm
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
x✝ : T
⊢ ((lmul R T) (e x)) x✝ = (↑↑e ∘ₗ (lmul R S) x ∘ₗ ↑(↑e).symm) x✝

Tactic:
;

Goal state after:
case e_6
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
x : S
x✝ : T
⊢ ((lmul R T) (e x)) x✝ = (↑↑e ∘ₗ (lmul R S) x ∘ₗ ↑(↑e).symm) x✝
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: case mk
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 S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this✝ : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
x✝ : R ⧸ p
x : R
⊢ (algebraMap (R ⧸ p) (T ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel p)) x) =
    (algebraMap (S ⧸ P) (T ⧸ I)) ((algebraMap (R ⧸ p) (S ⧸ P)) (Quot.mk (⇑(Submodule.quotientRel p)) x))

Tactic:
;

Goal state after:
case mk
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 S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this✝ : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
x✝ : R ⧸ p
x : R
⊢ (algebraMap (R ⧸ p) (T ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel p)) x) =
    (algebraMap (S ⧸ P) (T ⧸ I)) ((algebraMap (R ⧸ p) (S ⧸ P)) (Quot.mk (⇑(Submodule.quotientRel p)) x))
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case refine_2
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst✝⁵ : CommRing A₁
inst✝⁴ : Ring B₁
inst✝³ : CommRing A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra' ?refine_1
⊢ (norm A₁) x = e₁.symm ((norm A₂) (e₂ x))

Tactic:
let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }

Goal state after:
case refine_2
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst✝⁵ : CommRing A₁
inst✝⁴ : Ring B₁
inst✝³ : CommRing A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra' ?refine_1
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (norm A₁) x = e₁.symm ((norm A₂) (e₂ x))
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case zero
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)
⊢ Module.Finite R (S ⧸ ⊤)

Tactic:
;

Goal state after:
case zero
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)
⊢ Module.Finite R (S ⧸ ⊤)
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
r : S
⊢ absNorm (span {r}) = ((Algebra.norm ℤ) r).natAbs

Tactic:
Algebra.norm_apply

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case 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
hn : ⊤ ≤ Module.annihilator R M
⊢ P M

Tactic:
;

Goal state after:
case 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
hn : ⊤ ≤ Module.annihilator R M
⊢ P M
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 ≤ Module.annihilator R M
⊢ P M

Tactic:
;

Goal state after:
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 ≤ Module.annihilator R M
⊢ P M
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case e'_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
x : ↑s
e_1✝ : ↑s = { x // x ∈ s }
⊢ {x} = Subtype.val ⁻¹' {↑x}

Tactic:
;

Goal state after:
case e'_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
x : ↑s
e_1✝ : ↑s = { x // x ∈ s }
⊢ {x} = Subtype.val ⁻¹' {↑x}
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 : ℕ
x✝ : Ideal S
⊢ x✝ ∈ {I | absNorm I ≤ n} ↔ x✝ ∈ ⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
x✝ : Ideal S
⊢ x✝ ∈ {I | absNorm I ≤ n} ↔ x✝ ∈ ⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}