mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
g₁ : relations₁.G
r₂ : relations₂.R
⊢ (Finsupp.linearCombination A s.var)
      (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) =
    0

Tactic:
]

Goal state after:
A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
g₁ : relations₁.G
r₂ : relations₂.R
⊢ (Finsupp.linearCombination A s.var)
      (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) =
    0
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
r₁ : relations₁.R
g₂ : relations₂.G
⊢ (Finsupp.linearCombination A
        (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }))
      (relations₁.relation r₁) =
    0

Tactic:
]

Goal state after:
A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
r₁ : relations₁.R
g₂ : relations₂.G
⊢ (Finsupp.linearCombination A
        (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }))
      (relations₁.relation r₁) =
    0
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
r₁ : relations₁.R
g₂ : relations₂.G
this : (Finsupp.linearCombination A (s.var ∘ ⇑(Function.Embedding.sectL relations₁.G g₂))) (relations₁.relation r₁) = 0
⊢ (Finsupp.linearCombination A
        (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }))
      (relations₁.relation r₁) =
    0

Tactic:
]

Goal state after:
A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
r₁ : relations₁.R
g₂ : relations₂.G
this : (Finsupp.linearCombination A (s.var ∘ ⇑(Function.Embedding.sectL relations₁.G g₂))) (relations₁.relation r₁) = 0
⊢ (Finsupp.linearCombination A
        (⇑(LinearMap.applyₗ (solution₂.var g₂)) ∘ fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ }))
      (relations₁.relation r₁) =
    0
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4.monomial
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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
⊢ (if v ∈ {a ∈ Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support | a.1 = i} then
      (aeval P.val) ((monomial v.2) a)
    else 0) =
    if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0

Tactic:
]

Goal state after:
case a.convert_4.monomial
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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
⊢ (if v ∈ {a ∈ Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support | a.1 = i} then
      (aeval P.val) ((monomial v.2) a)
    else 0) =
    if v.1 = i then (aeval P.val) ((monomial v.2) a) else 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
A✝ : Type u_1
inst✝¹⁰ : CommRing A✝
inst✝⁹ : Algebra S A✝
inst✝⁸ : Algebra P✝.Ring A✝
inst✝⁷ : IsScalarTower P✝.Ring S A✝
P : Type u_2
A : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : CommRing A
inst✝⁴ : Algebra P S
inst✝³ : Algebra P A
inst✝² : Algebra R P
inst✝¹ : Algebra S A
inst✝ : IsScalarTower P S A
⊢ RingHom.ker (algebraMap P S) ≤ RingHom.ker ((algebraMap S A).comp (algebraMap P S))

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P✝ : Extension R S
A✝ : Type u_1
inst✝¹⁰ : CommRing A✝
inst✝⁹ : Algebra S A✝
inst✝⁸ : Algebra P✝.Ring A✝
inst✝⁷ : IsScalarTower P✝.Ring S A✝
P : Type u_2
A : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : CommRing A
inst✝⁴ : Algebra P S
inst✝³ : Algebra P A
inst✝² : Algebra R P
inst✝¹ : Algebra S A
inst✝ : IsScalarTower P S A
⊢ RingHom.ker (algebraMap P S) ≤ RingHom.ker ((algebraMap S A).comp (algebraMap P S))
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
A✝ : Type u_1
inst✝¹⁰ : CommRing A✝
inst✝⁹ : Algebra S A✝
inst✝⁸ : Algebra P✝.Ring A✝
inst✝⁷ : IsScalarTower P✝.Ring S A✝
P : Type u_2
A : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : CommRing A
inst✝⁴ : Algebra P S
inst✝³ : Algebra P A
inst✝² : Algebra R P
inst✝¹ : Algebra S A
inst✝ : IsScalarTower P S A
a : A
b : ↥(RingHom.ker (algebraMap P S))
⊢ ↑b ∈ RingHom.ker ((algebraMap S A).comp (algebraMap P S))

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P✝ : Extension R S
A✝ : Type u_1
inst✝¹⁰ : CommRing A✝
inst✝⁹ : Algebra S A✝
inst✝⁸ : Algebra P✝.Ring A✝
inst✝⁷ : IsScalarTower P✝.Ring S A✝
P : Type u_2
A : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : CommRing A
inst✝⁴ : Algebra P S
inst✝³ : Algebra P A
inst✝² : Algebra R P
inst✝¹ : Algebra S A
inst✝ : IsScalarTower P S A
a : A
b : ↥(RingHom.ker (algebraMap P S))
⊢ ↑b ∈ RingHom.ker ((algebraMap S A).comp (algebraMap P S))
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
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ (⇑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ ⇑(LinearMap.baseChange A P.cotangentComplex)) ∘
      ⇑((LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv).symm ≪≫ₗ
            AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm =
    ⇑(cotangentComplexBaseChange R S P.Ring A)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Extension R S
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ (⇑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ ⇑(LinearMap.baseChange A P.cotangentComplex)) ∘
      ⇑((LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv).symm ≪≫ₗ
            AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm =
    ⇑(cotangentComplexBaseChange R S P.Ring 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
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'
f : P.Hom P'
x : S
y : P.Ring
⊢ (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

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'
f : P.Hom P'
x : S
y : P.Ring
⊢ (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) ((algebraMap P.Ring P'.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)
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
ι : Type u_4
inst✝¹ : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst✝ : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j, a i j • y j
e : Fin (Fintype.card κ) ≃ κ
ham : ∀ (a_1 : Fin (Fintype.card κ)), ∑ i, a i (e a_1) • m i = 0
⊢ ∀ (j : Fin (Fintype.card κ)), ∑ i, (fun x ↦ a x ∘ ⇑e) i j • m i = 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
ι : Type u_4
inst✝¹ : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst✝ : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j, a i j • y j
e : Fin (Fintype.card κ) ≃ κ
ham : ∀ (a_1 : Fin (Fintype.card κ)), ∑ i, a i (e a_1) • m i = 0
⊢ ∀ (j : Fin (Fintype.card κ)), ∑ i, (fun x ↦ a x ∘ ⇑e) i j • m i = 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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i, a i j • m i = 0
⊢ ∑ y_1, ∑ x, a x y_1 • m x ⊗ₜ[R] y y_1 = 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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i, a i j • m i = 0
⊢ ∑ y_1, ∑ x, a x y_1 • m x ⊗ₜ[R] y y_1 = 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'
f : P.Hom P'
x : S
y : Ω[P.Ring⁄R]
⊢ (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring) y =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring) y

Tactic:
]

Goal state after:
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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
⊢ span R (Set.range m) ≤ G.range

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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
⊢ span R (Set.range m) ≤ G.range
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'
f : P.Hom P'
x : ↥P.ker
⊢ 1 ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom ↑x) = 1 ⊗ₜ[P'.Ring] (D R' P'.Ring) ↑⟨f.toAlgHom ↑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
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'
f g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈
    P'.ker * P'.ker

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'
f g : P.Hom P'
x y : P.Ring
this : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
⊢ (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈
    P'.ker * P'.ker
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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
x : ↥G.ker × N
a✝ : x ∈ ma
h'x : ↑x.1 i = 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'
f g : P.Hom P'
this✝² : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S S'
this✝ : Algebra P.Ring P'.Ring := f.toAlgHom.toAlgebra
this : IsScalarTower P.Ring P'.Ring S'
x : R
⊢ (algebraMap R S') x = (algebraMap R S') x

Tactic:
]

Goal state after:
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.ker
⊢ ∑ a ∈ (↑x).coeff.support,
      (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ ((↑x).coeff a)) * (monomial (Finsupp.mapDomain Sum.inl a)) 1) =
    ∑ v ∈ support ↑x, (monomial v) (coeff v ↑x)

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.ker
⊢ ∑ a ∈ (↑x).coeff.support,
      (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ ((↑x).coeff a)) * (monomial (Finsupp.mapDomain Sum.inl a)) 1) =
    ∑ v ∈ support ↑x, (monomial v) (coeff v ↑x)
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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ ((↑x).coeff j))) * j.prod fun a b ↦ (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)

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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ ((↑x).coeff j))) * j.prod fun a b ↦ (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
⊢ span R (Set.range (Subtype.val ∘ m')) = span R (Set.range m)

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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
⊢ span R (Set.range (Subtype.val ∘ m')) = span R (Set.range m)
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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((aeval fun i ↦ (Q.ofComp P).toAlgHom ((X ∘ Sum.inr) i)) (P.σ ((↑x).coeff j)) *
      j.prod fun a b ↦ (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)

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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((aeval fun i ↦ (Q.ofComp P).toAlgHom ((X ∘ Sum.inr) i)) (P.σ ((↑x).coeff j)) *
      j.prod fun a b ↦ (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case e_a
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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (algebraMap S Q.Ring) ((↑x).coeff j) = (algebraMap S (MvPolynomial ι' S)) (coeff j ↑x)

Tactic:
]

Goal state after:
case e_a
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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (algebraMap S Q.Ring) ((↑x).coeff j) = (algebraMap S (MvPolynomial ι' S)) (coeff j ↑x)
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.Ring
⊢ (∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x) ↔ x ∈ Q.ker

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.Ring
⊢ (∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x) ↔ x ∈ Q.ker