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

Goal state before:
pp: case mp
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : (Q.comp P).Ring
hx : (aeval (Q.comp P).val) x = 0
⊢ (aeval (Q.comp P).val) x = (aeval (Q.comp P).val) x

Tactic:
]

Goal state after:
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
⊢ (∀ (y : ↥P.cotangentComplex.ker), y = 0) ↔ ∀ (x : ↥P.cotangentComplex.ker), ↑x = 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (∀ (y : ↥P.cotangentComplex.ker), y = 0) ↔ ∀ (x : ↥P.cotangentComplex.ker), ↑x = 0
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
⊢ Subsingleton P.H1Cotangent ↔ Function.Injective ⇑P.cotangentComplex

Tactic:
delta Extension.H1Cotangent
  rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff, subsingleton_iff_forall_eq 0, Subtype.forall']
  simp only [Subtype.ext_iff, Submodule.coe_zero]

Goal state after:
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
⊢ P.cotangentComplex.ker = h1Cotangentι.range

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex.ker = h1Cotangentι.range
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
⊢ (Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ ((Q.comp P).ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom ⊥)

Tactic:
]

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
⊢ (Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ ((Q.comp P).ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom ⊥)
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'
f : P.Hom P'
x : P.Cotangent
hx : P'.cotangentComplex ((Cotangent.map f) x) = (CotangentSpace.map f) 0
⊢ P'.cotangentComplex ((Cotangent.map f) x) = 0

Tactic:
]

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'
f : P.Hom P'
x : P.Cotangent
hx : P'.cotangentComplex ((Cotangent.map f) x) = (CotangentSpace.map f) 0
⊢ P'.cotangentComplex ((Cotangent.map f) x) = 0
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'
f : P.Hom P'
x : P.Cotangent
hx : P'.cotangentComplex ((Cotangent.map f) x) = (CotangentSpace.map f) 0
⊢ (CotangentSpace.map f) 0 = 0

Tactic:
]

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'
f : P.Hom P'
x : P.Cotangent
hx : P'.cotangentComplex ((Cotangent.map f) x) = (CotangentSpace.map f) 0
⊢ (CotangentSpace.map f) 0 = 0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
⊢ (Q.comp P).ker = RingHom.ker (Q.ofComp P).toAlgHom ⊔ (Q.comp P).ker ⊔ RingHom.ker (Q.ofComp P).toAlgHom

Tactic:
]

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
⊢ (Q.comp P).ker = RingHom.ker (Q.ofComp P).toAlgHom ⊔ (Q.comp P).ker ⊔ RingHom.ker (Q.ofComp P).toAlgHom
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : P.H1Cotangent
⊢ ((f.sub g ∘ₗ P.cotangentComplex) ↑x).val = 0

Tactic:
]

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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : P.H1Cotangent
⊢ ((f.sub g ∘ₗ P.cotangentComplex) ↑x).val = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: 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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0
⊢ ∑ x ∈ s.attach, (↑x).1 ⊗ₜ[R] (↑x).2 = 0

Tactic:
]

Goal state after:
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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0
⊢ ∑ x ∈ s.attach, (↑x).1 ⊗ₜ[R] (↑x).2 = 0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ (algebraMap T T) ((aeval (Q.comp P).val) x) = 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ (algebraMap T T) ((aeval (Q.comp P).val) x) = 0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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
⊢ (↑S (map f₂) ∘ₗ map f₁) x = (map f₂ ∘ₗ map f₁) x

Tactic:
]

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.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: 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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
⊢ VanishesTrivially R (fun i ↦ (↑i).1) fun i ↦ (↑i).2

Tactic:
]

Goal state after:
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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
⊢ VanishesTrivially R (fun i ↦ (↑i).1) fun i ↦ (↑i).2
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
⊢ (↑S (map f₁) ∘ₗ map f₂) x = (map f₁ ∘ₗ map f₂) x

Tactic:
]

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.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: 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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this : VanishesTrivially R (fun i ↦ ↑(↑(e i)).1) fun i ↦ (↑(e i)).2
⊢ VanishesTrivially R ((fun i ↦ (↑i).1) ∘ ⇑e) ((fun i ↦ (↑i).2) ∘ ⇑e)

Tactic:
]

Goal state after:
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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this : VanishesTrivially R (fun i ↦ ↑(↑(e i)).1) fun i ↦ (↑(e i)).2
⊢ VanishesTrivially R ((fun i ↦ (↑i).1) ∘ ⇑e) ((fun i ↦ (↑i).2) ∘ ⇑e)
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: 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 :
  Surjective
    ⇑(↑(piLeft R M fun i ↦ R ⧸ I i).symm ∘ₗ
        (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1) ∘ₗ ↑(TensorProduct.lid R M))
⊢ Surjective ⇑(LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1)

Tactic:
]

Goal state after:
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 :
  Surjective
    ⇑(↑(piLeft R M fun i ↦ R ⧸ I i).symm ∘ₗ
        (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1) ∘ₗ ↑(TensorProduct.lid R M))
⊢ Surjective ⇑(LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1)
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
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S' ι'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : ι
j : ι'
⊢ (P'.cotangentSpaceBasis.repr ((CotangentSpace.map f.toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))) j =
    (aeval P'.val) ((pderiv j) (f.val i))

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S' ι'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : ι
j : ι'
⊢ (P'.cotangentSpaceBasis.repr ((CotangentSpace.map f.toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))) j =
    (aeval P'.val) ((pderiv j) (f.val i))
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: 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 = (⨅ i, I i) • ⊤

Tactic:
]

Goal state after:
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 = (⨅ i, I i) • ⊤
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
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S' ι'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : ι
j : ι'
⊢ (P'.cotangentSpaceBasis.repr
        (1 ⊗ₜ[{ Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
              algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring]
          (D R'
              { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                  algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring)
            (f.toExtensionHom.toAlgHom (X i))))
      j =
    (aeval P'.val) ((pderiv j) (f.val i))

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S' ι'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : ι
j : ι'
⊢ (P'.cotangentSpaceBasis.repr
        (1 ⊗ₜ[{ Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
              algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring]
          (D R'
              { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                  algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring)
            (f.toExtensionHom.toAlgHom (X i))))
      j =
    (aeval P'.val) ((pderiv j) (f.val i))
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
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S' ι'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : ι
j : ι'
⊢ (aeval P'.val) ((pderiv j) (f.val i)) = (aeval P'.val) ((pderiv j) (f.val i))

Tactic:
]

Goal state after:
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
h : ∀ (M' : Submodule R M), Injective ⇑(rTensor N M'.subtype)
k : ℕ
m : Fin k → M
n : Fin k → N
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n

Tactic:
exact vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R (h _) hmn

Goal state after:
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
P : Generators R S ι
i : ι
⊢ P.toExtension.toKaehler (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)) = (D R S) (P.val i)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type w
P : Generators R S ι
i : ι
⊢ P.toExtension.toKaehler (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)) = (D R S) (P.val i)
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
inst✝ : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ (Submodule.map P.toExtension.cotangentComplex ⊤).FG

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ (Submodule.map P.toExtension.cotangentComplex ⊤).FG
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: