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
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
P₁ : Extension R S
P₂ : Extension R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₁.H1Cotangent
⊢ (map (f₂.comp f₁)) x = (map f₂ ∘ₗ map f₁) x

Tactic:
Extension.H1Cotangent.map_comp

Goal state after:
R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
P₁ : Extension R S
P₂ : Extension R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₁.H1Cotangent
⊢ (↑S (map f₂) ∘ₗ map f₁) x = (map f₂ ∘ₗ map f₁) x
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
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
P₁ : Extension R S
P₂ : Extension R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₂.H1Cotangent
⊢ (map (f₁.comp f₂)) x = (map f₁ ∘ₗ map f₂) x

Tactic:
Extension.H1Cotangent.map_comp

Goal state after:
R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
P₁ : Extension R S
P₂ : Extension R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₂.H1Cotangent
⊢ (↑S (map f₁) ∘ₗ map f₂) x = (map f₁ ∘ₗ map f₂) x
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: case e'_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
⊢ (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1).ker =
    (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker

pp: case e'_3
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
⊢ (⨅ i, I i) • ⊤ = (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range

Tactic:
·

Goal state after:
case e'_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
⊢ (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1).ker =
    (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n) →
    ∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)

pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n) →
    ∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: case e'_3.refine_1
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
r : R
hr : r ∈ ⨅ i, I i
m : M
x✝ : m ∈ ⊤
⊢ r ∈ (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker

pp: case e'_3.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range ≤ (⨅ i, I i) • ⊤

Tactic:
·

Goal state after:
case e'_3.refine_1
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
r : R
hr : r ∈ ⨅ i, I i
m : M
x✝ : m ∈ ⊤
⊢ r ∈ (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n) →
    ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)

pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n) →
    ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)) →
    ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: case e'_3.refine_2.refine_1
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
r : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker
m : M
⊢ ((LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype (r, m).1, LinearMap.id (r, m).2).1 ∈ ⨅ i, I i

pp: case e'_3.refine_2.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x x✝¹ x✝ : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝¹ ∈ (⨅ i, I i) • ⊤ →
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝ ∈ (⨅ i, I i) • ⊤ →
      (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) (x✝¹ + x✝) ∈
        (⨅ i, I i) • ⊤

Tactic:
·

Goal state after:
case e'_3.refine_2.refine_1
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
r : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker
m : M
⊢ ((LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype (r, m).1, LinearMap.id (r, m).2).1 ∈ ⨅ i, I i
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: case e'_3.refine_2.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x x✝¹ x✝ : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝¹ ∈ (⨅ i, I i) • ⊤ →
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝ ∈ (⨅ i, I i) • ⊤ →
      (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) (x✝¹ + x✝) ∈
        (⨅ i, I i) • ⊤

Tactic:
·

Goal state after:
case e'_3.refine_2.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x x✝¹ x✝ : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝¹ ∈ (⨅ i, I i) • ⊤ →
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝ ∈ (⨅ i, I i) • ⊤ →
      (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) (x✝¹ + x✝) ∈
        (⨅ i, I i) • ⊤
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
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
tfae_5_to_4 :
  (∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0) →
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
⊢ [Flat R M, ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I)),
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x,
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x,
      ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0].TFAE

Tactic:
tfae_finish

Goal state after:
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 = ⊤
⊢ p ∈ support R M → ∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal

pp: case mpr
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) → p ∈ support R M

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 = ⊤
⊢ p ∈ support R M → ∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mpr
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) → p ∈ support R M

Tactic:
·

Goal state after:
case mpr
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) → p ∈ support R M
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
f : R
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) → Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

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

Tactic:
·

Goal state after:
case mp
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.Support

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

Tactic:
·

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} → ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
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 : (R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

pp: case neg
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 = ⊤
⊢ ∃ 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 : (R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
x✝ : ∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0
x : R
hx : x ∈ RingHom.ker (algebraMap R A)
m : A
hm : ∀ r ∉ p.asIdeal, ¬r • m = 0
hx' : x ∉ p.asIdeal
⊢ False

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
H : RingHom.ker (algebraMap R A) ≤ p.asIdeal
r : R
hr : r ∉ p.asIdeal
e : r • 1 = 0
⊢ False

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
x✝ : ∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0
x : R
hx : x ∈ RingHom.ker (algebraMap R A)
m : A
hm : ∀ r ∉ p.asIdeal, ¬r • m = 0
hx' : x ∉ p.asIdeal
⊢ False
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
H : RingHom.ker (algebraMap R A) ≤ p.asIdeal
r : R
hr : r ∉ p.asIdeal
e : r • 1 = 0
⊢ False

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
H : RingHom.ker (algebraMap R A) ≤ p.asIdeal
r : R
hr : r ∉ p.asIdeal
e : r • 1 = 0
⊢ False
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case e'_3
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 • x' = ↑⟨(algebraMap R S) a, ⋯⟩ * x'

Tactic:
·

Goal state after:
case e'_3
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 • x' = ↑⟨(algebraMap R S) a, ⋯⟩ * x'
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: 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'
s : Set N
x : N
hx : x ∈ Submodule.span R' s
s' : Finset N
hss' : ↑s' ⊆ s
hs' : x ∈ Submodule.span R' ↑s'
t : ↥M
ht : t • x ∈ Submodule.span R ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R s

pp: 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'
s : Set N
x : N
hx : x ∈ Submodule.span R' s
s' : Finset N
hss' : ↑s' ⊆ s
hs' : x ∈ Submodule.span R' ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R ↑s'

Tactic:
·

Goal state after:
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'
s : Set N
x : N
hx : x ∈ Submodule.span R' s
s' : Finset N
hss' : ↑s' ⊆ s
hs' : x ∈ Submodule.span R' ↑s'
t : ↥M
ht : t • x ∈ Submodule.span R ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R s