mathlib-initiative/mathlib-tactics huggingface dataset:
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
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁶ : CommRing R'
inst✝¹⁵ : CommRing S'
inst✝¹⁴ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝¹⁰ : Algebra R R'
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R' S''
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra S' S''
inst✝⁵ : Algebra S S''
inst✝⁴ : Algebra R R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : P.Ring
⊢ (g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x)

Tactic:
by

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
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
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 ι
i : ι
⊢ (aeval (Q.comp P).val) (X (Sum.inr i)) = (algebraMap S T) (P.val i)

Tactic:
by

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 ι
⊢ (Q.toComp P).toAlgHom = rename Sum.inr

Tactic:
by

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
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
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 ι
i : ι' ⊕ ι
⊢ (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) i) = (algebraMap T T) ((Q.comp P).val i)

Tactic:
by

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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ (Q.ofComp P).toAlgHom ((monomial (v₁.sumElim v₂)) a) = (monomial v₁) ((aeval P.val) ((monomial v₂) a))

Tactic:
by

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 ι
j : ι →₀ ℕ
a : R
⊢ (Q.toComp P).toAlgHom ((monomial j) a) = (monomial (Finsupp.sumElim 0 j)) a

Tactic:
by

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 ι
p : P.Ring
⊢ (Q.ofComp P).toAlgHom.comp (rename Sum.inr) =
    (IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)

Tactic:
by

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 ι
⊢ Function.Surjective ⇑(Q.ofComp P).toAlgHom

Tactic:
by

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
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Generators R T ι
i : ι
⊢ (aeval (extendScalars S P).val) (X i) = (algebraMap T T) (P.val i)

Tactic:
by

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
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁸ : CommRing R'
inst✝¹⁷ : CommRing S'
inst✝¹⁶ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹⁵ : CommRing R''
inst✝¹⁴ : CommRing S''
inst✝¹³ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝¹² : Algebra R R'
inst✝¹¹ : Algebra R' R''
inst✝¹⁰ : Algebra R' S''
inst✝⁹ : Algebra S S'
inst✝⁸ : Algebra S' S''
inst✝⁷ : Algebra S S''
T : Type u_7
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x : R
⊢ f.toAlgHom.toRingHom ((algebraMap R P.toExtension.Ring) x) = (algebraMap R' P'.toExtension.Ring) ((algebraMap R R') x)

Tactic:
by

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
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁸ : CommRing R'
inst✝¹⁷ : CommRing S'
inst✝¹⁶ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹⁵ : CommRing R''
inst✝¹⁴ : CommRing S''
inst✝¹³ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝¹² : Algebra R R'
inst✝¹¹ : Algebra R' R''
inst✝¹⁰ : Algebra R' S''
inst✝⁹ : Algebra S S'
inst✝⁸ : Algebra S' S''
inst✝⁷ : Algebra S S''
T : Type u_7
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x : P.toExtension.Ring
⊢ (algebraMap P'.toExtension.Ring S') (f.toAlgHom.toRingHom x) = (algebraMap S S') ((algebraMap P.toExtension.Ring S) x)

Tactic:
by

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
P : Generators R S ι
⊢ (Hom.id P).toExtensionHom = Extension.Hom.id P.toExtension

Tactic:
by

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
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝²² : CommRing R'
inst✝²¹ : CommRing S'
inst✝²⁰ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹⁹ : CommRing R''
inst✝¹⁸ : CommRing S''
inst✝¹⁷ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra R' R''
inst✝¹⁴ : Algebra R' S''
inst✝¹³ : Algebra S S'
inst✝¹² : Algebra S' S''
inst✝¹¹ : Algebra S S''
inst✝¹⁰ : Algebra R S'
inst✝⁹ : IsScalarTower R S S'
inst✝⁸ : Algebra R R''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : IsScalarTower R S S''
inst✝⁴ : IsScalarTower R' R'' S''
inst✝³ : IsScalarTower R' S' S''
inst✝² : IsScalarTower S S' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower R R' S'
f : P'.Hom P''
g : P.Hom P'
⊢ (f.comp g).toExtensionHom = f.toExtensionHom.comp g.toExtensionHom

Tactic:
by

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
P : Generators R S ι
⊢ P.ker = RingHom.ker (aeval P.val)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
m₁ m₂ : M
⊢ s.var (m₁ + m₂) = s.var m₁ + s.var m₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
⊢ (mvPolynomial R ι).ker = ⊥

Tactic:
by

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
P : Generators R S ι
x : P.Ring
hx : x ∈ P.ker
⊢ (aeval P.val) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
a : A
m : M
⊢ s.var (a • m) = (RingHom.id A) a • s.var m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
⊢ ∀ (r : (tautologicalRelations A M).R), (Finsupp.linearCombination A ⇑f) ((tautologicalRelations A M).relation r) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective ⇑f
⊢ ∀ (r : R), (algebraMap (ofAlgHom f h).toExtension.Ring S) (C r) = f.toRingHom (C r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : M →ₗ[A] N✝
h : (tautologicalSolution A M).postcomp f✝ = (tautologicalSolution A M).postcomp f'✝
⊢ f✝ = f'✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective ⇑f
⊢ ∀ (i : I), (algebraMap (ofAlgHom f h).toExtension.Ring S) (X i) = f.toRingHom (X i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Type u_8
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective ⇑f
⊢ (ofAlgHom f h).ker = RingHom.ker f.toRingHom

Tactic:
by

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
P : Generators R S ι
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
⊢ (P.ofAlgEquiv e).ker = P.ker

Tactic:
by

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 ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : P.Ring
hx : (algebraMap P.Ring S) x = 0
⊢ (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R P.Ring Q.Ring

Tactic:
by

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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
this :
  ∑ v ∈ Finset.map (↑e).toEmbedding (support x), (monomial (e.symm v)) (coeff (e.symm v) x) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
⊢ x ∈ Ideal.map (Q.toComp P).toAlgHom P.ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
⊢ Submodule.span A
      (Set.range fun x ↦
        match x with
        | (g, g') => presB.var g • Finsupp.single g' 1) =
    ⊤

Tactic:
by

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 ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x✝ : (Q.comp P).Ring
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
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))

Tactic:
by

Goal state after:
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₂
⊢ ∀ (r : (relations₁.tensor relations₂).R),
    (Finsupp.linearCombination A fun x ↦
          match x with
          | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂)
        ((relations₁.tensor relations₂).relation r) =
      0

Tactic:
by

Goal state after:
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 fun g₂ ↦ s.var (g₁, g₂)) (relations₂.relation r₂) = 0

Tactic:
by

Goal state after:
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
⊢ solution₂.postcomp
      ((Finsupp.linearCombination A fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ })
        (relations₁.relation r₁)) =
    solution₂.postcomp 0

Tactic:
by

Goal state after:
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✝
x✝ : (relations₁.tensor relations₂).Solution N✝
⊢ (solution₁.tensor solution₂).postcomp
      ((uncurry (RingHom.id A) M₁ M₂ N✝)
        (h₁.desc
          { var := fun g₁ ↦ h₂.desc { var := fun g₂ ↦ x✝.var (g₁, g₂), linearCombination_var_relation := ⋯ },
            linearCombination_var_relation := ⋯ })) =
    x✝

Tactic:
by

Goal state after:
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✝
f✝ f'✝ : M₁ ⊗[A] M₂ →ₗ[A] N✝
h : (solution₁.tensor solution₂).postcomp f✝ = (solution₁.tensor solution₂).postcomp f'✝
⊢ solution₁.postcomp (curry f✝) = solution₁.postcomp (curry f'✝)

Tactic:
by

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 u_1
G : Generators R S σ
r : R
hr : C r ∈ G.ker
⊢ mk ⟨C r, hr⟩ ∈ G.toExtension.cotangentComplex.ker

Tactic:
by

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
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 P A)

Tactic:
by

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
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 P A)

Tactic:
by

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
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ cotangentComplexBaseChange R S P.Ring A =
    ↑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ₗ
      LinearMap.baseChange A P.cotangentComplex ∘ₗ
        ↑((AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
            LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv)

Tactic:
by

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
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ LinearMap.baseChange A P.cotangentComplex =
    ↑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]).symm ∘ₗ
      cotangentComplexBaseChange R S P.Ring A ∘ₗ
        ↑((AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
              LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv).symm

Tactic:
by

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''
f : P.Hom P'
⊢ P.CotangentSpace →ₗ[S] P'.CotangentSpace

Tactic:
by

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 : P.Hom P'
x : S
y : P.Ring
⊢ (CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (D R' P'.Ring) (f.toAlgHom y)

Tactic:
by

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
κ : Type u_5
inst✝ : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j, a i j • y j
ham : ∀ (j : κ), ∑ i, a i j • m i = 0
e : Fin (Fintype.card κ) ≃ κ
⊢ ∀ (i : ι), n i = ∑ j, (fun x ↦ a x ∘ ⇑e) i j • (y ∘ ⇑e) j

Tactic:
by

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
κ : Type u_5
inst✝ : Fintype κ
a : ι → κ → R
y : κ → N
hay : ∀ (i : ι), n i = ∑ j, a i j • y j
ham : ∀ (j : κ), ∑ i, a i j • m i = 0
e : Fin (Fintype.card κ) ≃ κ
⊢ ∀ (j : Fin (Fintype.card κ)), ∑ i, (fun x ↦ a x ∘ ⇑e) i j • m i = 0

Tactic:
by

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
κ : Type u_5
inst✝ : Fintype κ
e : κ ≃ ι
⊢ VanishesTrivially R (m ∘ ⇑e) (n ∘ ⇑e) ↔ VanishesTrivially R m n

Tactic:
by

Goal state after: