mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := ⋯
Sq : Type u_1 := ⋯
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    0

pp: case hxt
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := ⋯
Sq : Type u_1 := ⋯
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    ⊤

Tactic:
·

Goal state after:
case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := ⋯
Sq : Type u_1 := ⋯
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    0
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case hxt
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := ⋯
Sq : Type u_1 := ⋯
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    ⊤

Tactic:
·

Goal state after:
case hxt
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := ⋯
Sq : Type u_1 := ⋯
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    ⊤
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ IsUnramifiedAt R q ↔ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)

pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = maximalIdeal (Localization.AtPrime q)

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ IsUnramifiedAt R q ↔ FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case left
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))

pp: case right
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Surjective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))

Tactic:
·

Goal state after:
case left
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case right
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Surjective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))

Tactic:
·

Goal state after:
case right
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Surjective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case e'_4
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ ↑(equiv W (Q.comp P)) ∘ₗ LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)

pp: case e'_5
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Extension.H1Cotangent.map f.toExtensionHom ∘ₗ ↑(equiv W (Q.comp P)).symm =
    Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom

Tactic:
·

Goal state after:
case e'_4
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ ↑(equiv W (Q.comp P)) ∘ₗ LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom) =
    LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case e'_5
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Extension.H1Cotangent.map f.toExtensionHom ∘ₗ ↑(equiv W (Q.comp P)).symm =
    Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom

Tactic:
·

Goal state after:
case e'_5
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Extension.H1Cotangent.map f.toExtensionHom ∘ₗ ↑(equiv W (Q.comp P)).symm =
    Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
hq : ¬q.IsPrime
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))

pp: case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
hq : q.IsPrime
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))

Tactic:
·

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
hq : ¬q.IsPrime
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : r.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

pp: case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : ¬r.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

Tactic:
·

Goal state after:
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : r.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : ¬r.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

Tactic:
·

Goal state after:
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : ¬r.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
·

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
·

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case refine_2
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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
⊢ Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer ⋯))

Tactic:
·

Goal state after:
case refine_2
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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
⊢ Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer ⋯))
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ x ∈ ⨆ i, torsionBySet A M ↑(I ^ i) → ∃ n, ∀ a ∈ I ^ n, a • x = 0

pp: case mpr
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ (∃ n, ∀ a ∈ I ^ n, a • x = 0) → x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)

Tactic:
·

Goal state after:
case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ x ∈ ⨆ i, torsionBySet A M ↑(I ^ i) → ∃ n, ∀ a ∈ I ^ n, a • x = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)
⊢ ∃ n, ∀ a ∈ I ^ n, a • x = 0

Tactic:
Submodule.mem_iSup_of_directed

Goal state after:
case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : ∃ i, x ∈ torsionBySet A M ↑(I ^ i)
⊢ ∃ n, ∀ a ∈ I ^ n, a • x = 0

case mp.H
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ torsionBySet A M ↑(I ^ i)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : ∃ i, x ∈ torsionBySet A M ↑(I ^ i)
⊢ ∃ n, ∀ a ∈ I ^ n, a • x = 0

pp: case mp.H
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ torsionBySet A M ↑(I ^ i)

Tactic:
·

Goal state after:
case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : ∃ i, x ∈ torsionBySet A M ↑(I ^ i)
⊢ ∃ n, ∀ a ∈ I ^ n, a • x = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp.H
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ torsionBySet A M ↑(I ^ i)

Tactic:
·

Goal state after:
case mp.H
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ torsionBySet A M ↑(I ^ i)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ (∃ n, ∀ a ∈ I ^ n, a • x = 0) → x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)

Tactic:
·

Goal state after:
case mpr
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ (∃ n, ∀ a ∈ I ^ n, a • x = 0) → x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
⊢ ((∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x) →
    ∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x

pp: case mpr
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
⊢ (∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x) →
    (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x

Tactic:
·

Goal state after:
case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
⊢ ((∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x) →
    ∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

pp: case neg
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
·

Goal state after:
case pos
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp.refine_1
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • y = 0

pp: case mp.refine_2
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • z = 0

Tactic:
·

Goal state after:
case mp.refine_1
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • y = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp.refine_2
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • z = 0

Tactic:
·

Goal state after:
case mp.refine_2
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • z = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
⊢ (∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x) →
    (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x

Tactic:
·

Goal state after:
case mpr
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
x : M
⊢ (∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x) →
    (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr.left
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
⊢ ∃ n, ∀ a ∈ I ^ n, a • (y + z) = 0

pp: case mpr.right
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
⊢ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z

Tactic:
·

Goal state after:
case mpr.left
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
⊢ ∃ n, ∀ a ∈ I ^ n, a • (y + z) = 0