mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
S : Submodule R M
hS : IsSimpleModule R ↥S
⊢ Nonempty (↥S ≃ₗ[R] M)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
⊢ IsIsotypicOfType R (↥N) S ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], Nonempty (↥m ≃ₗ[R] S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
⊢ g.IsWeierstrassFactorization (Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - r) ↑⋯.unit⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ IsIsotypic R ↥N ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], IsIsotypicOfType R ↥N ↥m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n).degree = ↑((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup S
inst✝² : Module R M
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R M
h : IsIsotypicOfType R M S
⊢ ∃ ι, Nonempty (M ≃ₗ[R] ι →₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
h : IsIsotypic R M
⊢ ∃ ι, ∃ (_ : Nonempty ι), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] ι →₀ ↥S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R S
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
h : IsIsotypicOfType R M S
⊢ ∃ n, Nonempty (M ≃ₗ[R] Fin n → S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
n : ℕ
e : Nonempty (M ≃ₗ[R] Fin n → ↥S)
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
⊢ ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
h : m ∈ isotypicComponents R M
⊢ ⊥ < m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
⊢ IsSemisimpleModule R ↥(isotypicComponent R M S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁸ : CommSemiring R₀
inst✝⁷ : Ring R
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup S
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R S
c : ↑(isotypicComponents R M)
⊢ IsSemisimpleModule R ↥↑c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Submodule R M
inst✝¹ : IsSimpleModule R ↥N
s : Set (Submodule R M)
inst✝ : IsSemisimpleModule R M
hs : sSup s = ⊤
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
⊢ (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g (↑⋯.unit⁻¹)
    (Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : ↑⋯.unit = ↑⋯.unit
h2 :
  Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f =
    Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f'
⊢ f = f'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
⊢ f = f' ∧ h = h'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this✝ : IsSimpleModule R ↥(inclusion hN).range
this : IsSemisimpleModule R ↥(⨆ i ∈ s, i)
⊢ sSup (comap (⨆ i ∈ s, i).subtype '' s) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
⊢ ∃ f h, g.IsWeierstrassFactorization f h

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g g' : A⟦X⟧
f : A[X]
h✝ : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
h : (map (IsLocalRing.residue A)) g = 0
⊢ (map (IsLocalRing.residue A)) (g * g') = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g g' : A⟦X⟧
f : A[X]
h✝ : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
h : (map (IsLocalRing.residue A)) g' = 0
⊢ (map (IsLocalRing.residue A)) (g * g') = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
h : (map (IsLocalRing.residue A)) g = 0
⊢ (map (IsLocalRing.residue A)) (g * g') = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
h : (map (IsLocalRing.residue A)) g' = 0
⊢ (map (IsLocalRing.residue A)) (g * g') = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ sSup s
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
⊢ (g * g').weierstrassDistinguished hg = g.weierstrassDistinguished ⋯ * g'.weierstrassDistinguished ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
h : m ∈ isotypicComponents R M
⊢ IsIsotypic R ↥m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
S c : Submodule R M
hc : c ∈ isotypicComponents R M
inst✝ : IsSimpleModule R ↥S
le : S ≤ c
⊢ c = isotypicComponent R M ↥S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g g' : A⟦X⟧
f : A[X]
h✝ : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
h : (map (IsLocalRing.residue A)) g = 0
⊢ (map (IsLocalRing.residue A)) (a • g) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
h : (map (IsLocalRing.residue A)) g = 0
⊢ (map (IsLocalRing.residue A)) (a • g) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
⊢ IsSemisimpleModule R ↥c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
h : (IsLocalRing.residue A) a = 0
⊢ (map (IsLocalRing.residue A)) (a • g) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
ha : (IsLocalRing.residue A) a ≠ 0
⊢ IsUnit a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
⊢ Disjoint ↑pc ↑p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c✝ : Submodule R M
hc : c✝ ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c✝}
ne : ¬c✝ ⊓ sSup s = ⊥
this✝ : IsSemisimpleModule R ↥c✝
this : IsSemisimpleModule R ↥(c✝ ⊓ sSup s)
c : ↑s
⊢ IsSemisimpleModule R ↥↑c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝¹ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝ : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this : pS.IsPrime
⊢ IsLocalization.AtPrime (Localization.AtPrime pS) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: S : Type u_2
inst✝³ : DivisionRing S
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module S N
inst✝ : IsSimpleModule S N
⊢ Nonempty (N ≃ₗ[S] S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsSimpleModule R M
N : Type v
x✝¹ : AddCommGroup N
x✝ : Module R N
f : M →ₗ[R] N
h : f.ker = ⊥
⊢ Function.Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsSimpleModule R M
N : Type v
x✝¹ : AddCommGroup N
x✝ : Module R N
f : M →ₗ[R] N
h : f.ker = ⊤
⊢ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Nontrivial M ∧
    ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
hM1 : Nontrivial M
hM2 : ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
p : Submodule R M
h : p.mkQ = 0
⊢ p = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ comap C pS = maximalIdeal (Localization.AtPrime q)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Nontrivial M ∧
    ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
hM1 : Nontrivial M
hM2 : ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
p : Submodule R M
h : Function.Injective ⇑p.mkQ
x : M
hx : x ∈ p
⊢ p.mkQ x = p.mkQ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝³ : Ring R
inst✝² : Ring S
e : ModuleCat R ⥤ ModuleCat S
inst✝¹ : e.IsEquivalence
M : ModuleCat R
inst✝ : IsSimpleModule R ↑M
⊢ IsSimpleModule S ↑(e.obj M)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
⊢ IsRegularRing R[X]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularRing R
ι : Type u_2
inst✝ : Finite ι
⊢ IsRegularRing (MvPolynomial ι R)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
ne : ¬c ⊓ sSup (isotypicComponents R M \ {c}) = ⊥
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
⊢ map f S ≤ isotypicComponent R N ↥S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_5
inst✝ : Semiring R
I : Ideal R
⊢ Submodule.IsFullyInvariant I ↔ I.IsTwoSided

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N✝ : Type u_3
S : Type u_4
inst✝¹⁰ : CommSemiring R₀
inst✝⁹ : Ring R
inst✝⁸ : Algebra R₀ R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N✝
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x✝ : M
i : ι
x : M
h : x ∈ N i
⊢ ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i ↦ LinearMap.restrict f ⋯) f))
      x =
    f x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N✝ : Type u_3
S : Type u_4
inst✝¹⁰ : CommSemiring R₀
inst✝⁹ : Ring R
inst✝⁸ : Algebra R₀ R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N✝
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x : M
⊢ ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i ↦ LinearMap.restrict f ⋯) f))
      0 =
    f 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N✝ : Type u_3
S : Type u_4
inst✝¹⁰ : CommSemiring R₀
inst✝⁹ : Ring R
inst✝⁸ : Algebra R₀ R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N✝
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x x✝¹ x✝ : M
h₁ :
  ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i ↦ LinearMap.restrict f ⋯) f))
      x✝¹ =
    f x✝¹
h₂ :
  ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i ↦ LinearMap.restrict f ⋯) f))
      x✝ =
    f x✝
⊢ ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i ↦ LinearMap.restrict f ⋯) f))
      (x✝¹ + x✝) =
    f (x✝¹ + x✝)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N✝ : Type u_3
S : Type u_4
inst✝¹⁰ : CommSemiring R₀
inst✝⁹ : Ring R
inst✝⁸ : Algebra R₀ R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N✝
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : Module.End R M
x : M
⊢ ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i ↦ LinearMap.restrict f ⋯) f))
      x =
    f x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N✝ : Type u_3
S : Type u_4
inst✝¹⁰ : CommSemiring R₀
inst✝⁹ : Ring R
inst✝⁸ : Algebra R₀ R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N✝
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : (i : ι) → Module.End R ↥(N i)
⊢ (fun f i ↦ LinearMap.restrict f ⋯)
      ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
h : m ∈ isotypicComponents R M
⊢ m.IsFullyInvariant

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSimpleModule R S
s : Set ↑(isotypicComponents R M)
c : ↑(isotypicComponents R M)
hc : c ∈ {c | ↑c ≤ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩)}
hcs : c ∉ s
⊢ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩) ≤ sSup (isotypicComponents R M \ {↑c})

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
⊢ isotypicComponent R M S = ⊤ ↔ IsIsotypicOfType R M S

Tactic:
by

Goal state after: