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

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
r : σ
⊢ pres.relation r ∈ pres.ker

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
r : σ
a✝ : ι
⊢ (pres.cotangentSpaceBasis.repr (1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r))) a✝ =
    (pres.cotangentSpaceBasis.repr
        ((Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
          (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
            ((mvPolynomialBasis R ι).repr ((D R (MvPolynomial ι R)) (pres.relation r))))))
      a✝

Tactic:
simp

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

Goal state before:
pp: case add
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
ex : ∃ a, (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x
ey : ∃ a, (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = y
⊢ ∃ a, (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x + y

Tactic:
obtain ⟨a, ha⟩ := ex

Goal state after:
case add
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T✝ : Type ?u.18
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
x y : T ⊗[R] S
ey : ∃ a, (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = y
a : MvPolynomial ι T
ha : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x
⊢ ∃ a, (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) a = x + y
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁷ : Ring A
ι : Type w
inst✝⁶ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝⁵ : (i : ι) → AddCommGroup (M i)
inst✝⁴ : (i : ι) → Module A (M i)
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
solution : (i : ι) → (relations i).Solution (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N✝ : Type w'
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (Relations.directSum relations).Solution N✝
i : ι
g : (relations i).G
⊢ ((directSum solution).postcomp (toModule A ι N✝ fun i ↦ ⋯.desc (directSumEquiv s i))).var ⟨i, g⟩ = s.var ⟨i, g⟩

Tactic:
simp

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 ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
⊢ (aeval P.val) ((rename ⇑e) ((⇑(rename ⇑e.symm) ∘ P.σ) s)) = (aeval P.val) (P.σ s)

Tactic:
simp

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 R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((fun f ↦ { val := fun i ↦ ↑f (X i), aeval_val := ⋯ }) ((fun f ↦ ⟨f.toAlgHom, ⋯⟩) f)).val x✝) =
    coeff m✝ (f.val x✝)

Tactic:
simp

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 R' S'
inst✝ : IsScalarTower R S S'
f : { f // ∀ (x : P.Ring), (aeval P'.val) (f x) = (algebraMap S S') ((aeval P.val) x) }
i✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (↑((fun f ↦ ⟨f.toAlgHom, ⋯⟩) ((fun f ↦ { val := fun i ↦ ↑f (X i), aeval_val := ⋯ }) f)) (X i✝)) =
    coeff m✝ (↑f (X i✝))

Tactic:
simp

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''
x : ι
⊢ (aeval P'.val) ((P'.σ ∘ ⇑(algebraMap S S') ∘ P.val) x) = (algebraMap S S') (P.val x)

Tactic:
simp

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''
⊢ ∀ (i : ι), (aeval P.val) (X i) = (algebraMap S S) (P.val i)

Tactic:
simp

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 ι
i✝ : ι
⊢ (Hom.id P).toAlgHom (X i✝) = (AlgHom.id R P.Ring) (X i✝)

Tactic:
simp

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' ι'
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'
x✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ ((f.comp (Hom.id P)).val x✝) = coeff m✝ (f.val x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.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.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension 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 R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
⊢ (LinearMap.liftBaseChange S Cotangent.mk) (1 ⊗ₜ[P.Ring] x) = Cotangent.mk x

Tactic:
simp

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:
simp

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

Goal state before:
pp: case inl
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 ι
val✝ : ι'
⊢ (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inl val✝)) = (algebraMap T T) ((Q.comp P).val (Sum.inl val✝))

Tactic:
simp

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

Goal state before:
pp: case inr
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 ι
val✝ : ι
⊢ (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inr val✝)) = (algebraMap T T) ((Q.comp P).val (Sum.inr val✝))

Tactic:
simp

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:
rw [Hom.toAlgHom_monomial, monomial_eq]

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 ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 ↦ (Q.ofComp P).val x1 ^ x2) =
    C ((aeval P.val) ((monomial v₂) a)) * v₁.prod fun n e ↦ X n ^ e
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case zero
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
v : presM.R →₀ B
⊢ 0 ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
simp

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
i✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((Q.ofComp P).toAlgHom.comp (rename Sum.inr)) (X i✝)) =
    coeff m✝ (((IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) (X i✝))

Tactic:
simp

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

Goal state before:
pp: case h
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 ι
a : S
⊢ ((IsScalarTower.toAlgHom R S (MvPolynomial ι' S)).comp (aeval P.val)) (P.σ a) =
    (IsScalarTower.toAlgHom R S (MvPolynomial ι' S)) a

Tactic:
simp

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

Goal state before:
pp: case h
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 q : (Q.comp P).Ring
⊢ (Q.ofComp P).toAlgHom (p + q) = (Q.ofComp P).toAlgHom p + (Q.ofComp P).toAlgHom q

Tactic:
simp

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

Goal state before:
pp: case single_add
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
v : presM.R →₀ B
r : presM.R
b : B
w : presM.R →₀ B
a✝¹ : r ∉ w.support
a✝ : b ≠ 0
⊢ w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
    Finsupp.single r b + w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
hw

Goal state after:
case single_add
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
v : presM.R →₀ B
r : presM.R
b : B
w : presM.R →₀ B
a✝¹ : r ∉ w.support
a✝ : b ≠ 0
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
⊢ Finsupp.single r b + w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
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:
simp

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:
simp

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:
simp

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.toExtension.Ring
⊢ (Hom.id P).toExtensionHom.toRingHom x✝ = (Extension.Hom.id P.toExtension).toRingHom x✝

Tactic:
simp

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'
x✝ : P.toExtension.Ring
⊢ (f.comp g).toExtensionHom.toRingHom x✝ = (f.toExtensionHom.comp g.toExtensionHom).toRingHom x✝

Tactic:
simp

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

Goal state before:
pp: case single_add.zero
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
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝¹ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝ : presB.π β ≠ 0
⊢ Finsupp.single r (presB.π 0) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
simp

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:
simp

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

Goal state before:
pp: case add
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
m₁✝ m₂✝ : M
⊢ (Finsupp.linearCombination A ⇑f) ((tautologicalRelations A M).relation (tautological.R.add m₁✝ m₂✝)) = 0

Tactic:
simp

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

Goal state before:
pp: case smul
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
a✝ : A
m✝ : M
⊢ (Finsupp.linearCombination A ⇑f) ((tautologicalRelations A M).relation (tautological.R.smul a✝ m✝)) = 0

Tactic:
simp

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
i✝ : ι
⊢ ((Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom) (X i✝) = (IsScalarTower.toAlgHom R P.Ring Q.Ring) (X i✝)

Tactic:
simp

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

Goal state before:
pp: case single_add.single_add
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
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝³ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝² : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝¹ : g ∉ f.support
a✝ : a ≠ 0
⊢ Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
    Finsupp.single r (presB.π (Finsupp.single g a + f)) ∈
      Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
hf

Goal state after:
case single_add.single_add
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
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝³ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝² : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝¹ : g ∉ f.support
a✝ : a ≠ 0
hf : Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
⊢ Finsupp.single r (presB.π (Finsupp.single g a + f)) ∈
    Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)