mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
n p : α
⊢ (factorization n) p = Multiset.count p (normalizedFactors n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
⊢ factorization 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
⊢ factorization 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
n : α
⊢ (factorization n).support = (normalizedFactors n).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization (a * b) = factorization a + factorization b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
x : α
n : ℕ
⊢ factorization (x ^ n) = n • factorization x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : factorization a = factorization b
⊢ a ~ᵤ b

Tactic:
by

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

Goal state before:
pp: 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
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
⊢ map (algebraMap R Sq') p = map (↑(AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯)) (map (algebraMap R Sq) p)

Tactic:
by

Goal state after:
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
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
hRS : (RingHom.ker (algebraMap R S)).FG
inst✝ : q.LiesOver p
H : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
⊢ ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')

Tactic:
by

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

Goal state before:
pp: 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
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
by

Goal state after:
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
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
x : S
a b : R
hbp : b ∉ p
c : S
hcq : c ∉ q
hc : c * (algebraMap R S) a = c * (x * (algebraMap R S) b)
d : R
hd : d ∉ p
e : S
he : (algebraMap R S) d = c * e
⊢ (algebraMap R S) (d * a) = x * (algebraMap R S) (d * b)

Tactic:
by

Goal state after:
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
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
x : S
⊢ ∃ a, ∃ b ∉ p, (algebraMap R S) a = x * (algebraMap R S) b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
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
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ IsLocalization.mk' (Localization M') x ⟨s, hs⟩ =
    IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
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
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
⊢ Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
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
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ
⊢ F =
    ↑(LinearEquiv.restrictScalars P.Ring
          (LinearEquiv.ofEq
            (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker)
            (RingHom.ker fQ) this)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit (((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨y, hy⟩)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
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 ⋯
⊢ Function.Surjective ⇑fQ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
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 ⋯
⊢ (IsScalarTower.toAlgHom R Q.Ring T).comp (MvPolynomial.aeval Q.σ) =
    IsScalarTower.toAlgHom R (Generators.self R T).toExtension.Ring T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
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 ⋯
⊢ ∀ (x : (Generators.self R T).toExtension.Ring),
    (algebraMap Q.Ring T) ((MvPolynomial.aeval Q.σ).toRingHom x) =
      (algebraMap T T) ((algebraMap (Generators.self R T).toExtension.Ring T) x)

Tactic:
by

Goal state after:
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
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
⊢ (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).range ≤ (awayMapₐ (Algebra.ofId R S) r').range

Tactic:
by

Goal state after:
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
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
⊢ ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Bijective ⇑(awayMap (algebraMap R S) r')

Tactic:
by

Goal state after:
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
p : Ideal R
inst✝⁷ : p.IsPrime
q : Ideal S
inst✝⁶ : q.IsPrime
hq : p.primesOver S = {q}
inst✝⁵ : Module.Finite R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
⊢ (RingHom.ker (algebraMap R S)).FG

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
⊢ ↑(tensorH1CotangentOfIsLocalization R T M) = LinearMap.liftBaseChange T (H1Cotangent.map R R S T)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Encodable

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
⊢ Countable (Π₀ (i : ι), α i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
⊢ IsLocalizedModule M (map R R S T)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Countable

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Countable R
inst✝ : Countable ι
v : ι → M
⊢ Countable ↥(Submodule.span R (Set.range v))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Encodable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Countable α
inst✝¹ : Countable β
inst✝ : Zero β
⊢ Countable (α →₀ β)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Countable

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Countable R
inst✝ : Module.Finite R M
⊢ Countable M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Countable

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hM : Uncountable M
inst✝ : Module.Finite R M
⊢ Uncountable R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ x ∈ primaryComponent M I ↔ ∃ n, x ∈ torsionBySet A M ↑(I ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : ↥(primaryComponent M₁ I)
⊢ φ ↑c ∈ primaryComponent M₂ I

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : CommRing A
I : Ideal A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module A M
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : ↥(primaryComponent M₁ I)
⊢ (φ.domRestrict (primaryComponent M₁ I)) c ∈ primaryComponent M₂ I

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
⊢ Submodule.map (primaryComponent M₁ I).subtype (map I φ).ker =
    Submodule.map φ.ker.subtype (primaryComponent (↥φ.ker) I)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
I : Ideal A
⊢ Submodule.map (torsionBySet A M ↑I).subtype (primaryComponent (↥(torsionBySet A M ↑I)) I) =
    primaryComponent M I ⊓ torsionBySet A M ↑I

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
x : M
⊢ x = 0 → (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∀ a ∈ J, a • x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
⊢ primaryComponent (↥(torsionBySet A M ↑J)) I = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: 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
⊢ y ∈ N₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: 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
⊢ z ∈ N₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

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

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
⊢ a ∉ S i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: 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
a : A
ha : a ∈ I ^ max n₁ n₂
⊢ n₁ ≤ max n₁ n₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: 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₁ : ℕ
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
a : A
hy : a • y = 0
ha : a ∈ I ^ max n₁ n₂
⊢ n₂ ≤ max n₁ n₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha✝ : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
ha : a ∉ S i
⊢ (⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: 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₂
⊢ Submodule.map (N₁ ⊔ N₂).subtype (primaryComponent (↥(N₁ ⊔ N₂)) I) =
    Submodule.map N₁.subtype (primaryComponent (↥N₁) I) ⊔ Submodule.map N₂.subtype (primaryComponent (↥N₂) I)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : a • x = 0
⊢ x ∈ torsionBySet A M ↑(span {a})

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Preorder G
inst✝¹ : MulLeftMono G
inst✝ : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s / t) (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(span {a})
⊢ span {a} ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a - ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t.val, S i).indicator f a =
    ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a +
      ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a +
      ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ ∑ t ∈ s.powerset, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a = (∏ i ∈ s, (1 - (S i).indicator 1 a)) • f a

Tactic:
by

Goal state after: