mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S'
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.QuotSMulTop

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
H₁ : Surjective (⇑(r • ⊤).mkQ ∘ ⇑f)
⊢ Surjective (⇑(r • ⊤).mkQ ∘ ⇑f)

Tactic:
]

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
H₁ : Surjective (⇑(r • ⊤).mkQ ∘ ⇑f)
⊢ Surjective (⇑(r • ⊤).mkQ ∘ ⇑f)
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hx₁ : y' • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hx₁ : y' • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, (R ∙ m).annihilator ≤ p.asIdeal

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, (R ∙ m).annihilator ≤ p.asIdeal
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : PrimeSpectrum R
H : p ≤ q
hp : ∃ m, (R ∙ m).annihilator ≤ p.asIdeal
⊢ ∃ m, (R ∙ m).annihilator ≤ q.asIdeal

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : PrimeSpectrum R
H : p ≤ q
hp : ∃ m, (R ∙ m).annihilator ≤ p.asIdeal
⊢ ∃ m, (R ∙ m).annihilator ≤ q.asIdeal
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ P.toExtension.cotangentComplex.rangeRestrict.ker.FG

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ P.toExtension.cotangentComplex.rangeRestrict.ker.FG
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal) → ∀ x ∈ s, x ∈ ↑(LocalizedModule.mkLinearMap p.asIdeal.primeCompl M).ker

Tactic:
]

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (¬∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal) → ∀ x ∈ s, x ∈ ↑(LocalizedModule.mkLinearMap p.asIdeal.primeCompl M).ker
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Flat R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : N
x : N →ₗ[R] M
h : x f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a (e.symm f) = 0
⊢ x ∘ₗ ↑e = y ∘ₗ a

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Flat R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : N
x : N →ₗ[R] M
h : x f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a (e.symm f) = 0
⊢ x ∘ₗ ↑e = y ∘ₗ a
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this✝ : FiniteType R P.toExtension.Ring
this : Module.Finite S P.toExtension.Cotangent
⊢ Module.FinitePresentation S ↥P.toExtension.toKaehler.ker

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this✝ : FiniteType R P.toExtension.Ring
this : Module.Finite S P.toExtension.Cotangent
⊢ Module.FinitePresentation S ↥P.toExtension.toKaehler.ker
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx :
  (Algebra.linearMap S S') (y' • x) ∈
    Submodule.map g.toLinearMap (Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx :
  (Algebra.linearMap S S') (y' • x) ∈
    Submodule.map g.toLinearMap (Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
K : Type u_3
inst✝² : AddCommGroup K
inst✝¹ : Module R K
inst✝ : Module.Finite R K
K' K₁ K₂ : Submodule R K
hN₁✝ : K₁.FG
hN₂✝ : K₂.FG
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M}, x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ K₁ ≤ (a ∘ₗ f).ker
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M}, x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ K₂ ≤ (a ∘ₗ f).ker
n : ℕ
f : K →ₗ[R] Fin n →₀ R
k₁ : ℕ
a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R
y₁ : (Fin k₁ →₀ R) →ₗ[R] M
ha₁ : K₁ ≤ (a₁ ∘ₗ f).ker
h : (y₁ ∘ₗ a₁) ∘ₗ f = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : m = 0
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
]

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : m = 0
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(R ∙ m).annihilator = ⊤
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J | (R ∙ m).annihilator ≤ J ∧ J.IsPrime} → f ∈ I

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(R ∙ m).annihilator = ⊤
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J | (R ∙ m).annihilator ≤ J ∧ J.IsPrime} → f ∈ I
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers 1, r • m = 0) ↔ ∀ (y : M), y = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers 1, r • m = 0) ↔ ∀ (y : M), y = 0
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ¬Subsingleton M ↔ ¬Subsingleton M

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case e'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
x' : S
hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx'' : (algebraMap S S') x' = (Algebra.linearMap S S') (y' • x)
a : R
ha₁ : a ∈ ↑M
ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
⊢ ↑⟨a, ha₁⟩ • ↑⟨y', hy'⟩ • x = (algebraMap R S) a * y' • x

Tactic:
]

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
x' : S
hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx'' : (algebraMap S S') x' = (Algebra.linearMap S S') (y' • x)
a : R
ha₁ : a ∈ ↑M
ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
⊢ ↑⟨a, ha₁⟩ • ↑⟨y', hy'⟩ • x = (algebraMap R S) a * y' • x
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case insert
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
y : R'
z : N
hz : z ∈ Submodule.span R' ↑s
y' : R
s' : ↥M
e✝ : y * (algebraMap R R') ↑(y', s').2 = (algebraMap R R') (y', s').1
e : (y * (algebraMap R R') ↑s') • a = y' • a
t : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ t • s' • y • a + s' • t • z = ↑t • (↑s' • y) • a + ↑s' • t • z

Tactic:
]

Goal state after:
case insert
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
y : R'
z : N
hz : z ∈ Submodule.span R' ↑s
y' : R
s' : ↥M
e✝ : y * (algebraMap R R') ↑(y', s').2 = (algebraMap R R') (y', s').1
e : (y * (algebraMap R R') ↑s') • a = y' • a
t : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ t • s' • y • a + s' • t • z = ↑t • (↑s' • y) • a + ↑s' • t • z
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
e₁ : r • m ∈ Set.range ⇑f
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
e₁ : r • m ∈ Set.range ⇑f
⊢ ∃ r ∉ x.asIdeal, r • m = 0
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case h
R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤
sf : ↥t → Finset M := fun x ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)
⊢ ⊤ ≤ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
]

Goal state after:
case h
R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤
sf : ↥t → Finset M := fun x ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)
⊢ ⊤ ≤ ⨆ x, Submodule.span R ↑(sf x)
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : Flat R M
K : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a ∘ₗ ↑e.symm ∘ₗ f = 0
⊢ x ∘ₗ ↑e = y ∘ₗ a

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : Flat R M
K : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a ∘ₗ ↑e.symm ∘ₗ f = 0
⊢ x ∘ₗ ↑e = y ∘ₗ a