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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
Rᵣₛ : Type u_3 := Localization rs
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Tactic:
have hsu : IsUnit (algebraMap R Rᵣₛ s) := isUnit_of_dvd_unit
      (hu := IsLocalization.map_units (M := rs) Rᵣₛ ⟨_, Submonoid.mem_powers _⟩)
      (map_dvd (algebraMap R Rᵣₛ) ⟨r, mul_comm _ _⟩)

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
Rᵣₛ : Type u_3 := Localization rs
hsu : IsUnit ((algebraMap R Rᵣₛ) ↑s)
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (x y : R[X]),
    (AEval.of R M a) (d ((aeval a) (x + y))) = (AEval.of R M a) (d ((aeval a) x)) + (AEval.of R M a) (d ((aeval a) y))

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (m : R) (x : R[X]), (AEval.of R M a) (d ((aeval a) (m • x))) = (RingHom.id R) m • (AEval.of R M a) (d ((aeval a) x))

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ { toFun := fun f ↦ (AEval.of R M a) (d ((aeval a) f)), map_add' := ⋯, map_smul' := ⋯ } 1 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: case single.e_a.C
R : Type u
inst✝ : CommRing R
σ : Type u_1
b : MvPolynomial σ R
a✝ : R
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1) (MvPolynomial.C a✝)) =
    (D R (MvPolynomial σ R)) (MvPolynomial.C a✝)

Tactic:
simp only [MvPolynomial.derivation_C, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R[X]
⊢ derivative'.liftKaehlerDifferential.toFun (((lsmul R R Ω[R[X]⁄R]).toLinearMap.flip ((D R R[X]) X)) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
y : M'
⊢ (y, 1).2 • y = LinearMap.id (y, 1).1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m✝ : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m✝ → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
φ : M →ₗ[R] N
s : S
m : Fin n → R
⊢ ((AlgebraTensorModule.curry ((baseChangeHom R S (Fin n → R) N ∘ₗ lcomp R N f) φ)) s) m =
    ((AlgebraTensorModule.curry ((↑R (lcomp S (S ⊗[R] N) (baseChange S f)) ∘ₗ baseChangeHom R S M N) φ)) s) m

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : FinitePresentation R M
n m✝ : ℕ
f : (Fin n → R) →ₗ[R] M
g : (Fin m✝ → R) →ₗ[R] Fin n → R
hf : Function.Surjective ⇑f
hfg : Function.Exact ⇑g ⇑f
φ : (Fin n → R) →ₗ[R] N
s : S
m : Fin m✝ → R
⊢ ((AlgebraTensorModule.curry ((baseChangeHom R S (Fin m✝ → R) N ∘ₗ lcomp R N g) φ)) s) m =
    ((AlgebraTensorModule.curry ((↑R (lcomp S (S ⊗[R] N) (baseChange S g)) ∘ₗ baseChangeHom R S (Fin n → R) N) φ)) s) m

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x✝ : MvPolynomial σ R
⊢ ↑(algebraTensorAlgEquiv R S) (1 ⊗ₜ[R] x✝) =
    (IsScalarTower.toAlgHom R (MvPolynomial σ R) (MvPolynomial σ S)).toLinearMap x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ∀ (x y : MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1}), (auxHom S r) (x * y) = (auxHom S r) x * (auxHom S r) y

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ∀ (x y : MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1}), (auxHom S r) (x + y) = (auxHom S r) x + (auxHom S r) y

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ∀ (r_1 : R),
    (auxHom S r) ((algebraMap R (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})) r_1) = (algebraMap R S) r_1

Tactic:
by 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
M : Submonoid S
S' : Type u_1
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : IsLocalization M S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R S S'
P : Extension R S
s : S'
⊢ P.σ ↑(IsLocalization.sec M s).2 ∈ Submonoid.comap (algebraMap P.Ring S) M

Tactic:
by 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 R''
inst✝² : Algebra S S'
inst✝¹ : Algebra S' S''
inst✝ : Algebra S S''
⊢ ∀ (x : R), (RingHom.id P.Ring) ((algebraMap R P.Ring) x) = (algebraMap R P.Ring) ((algebraMap R R) x)

Tactic:
by 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 R''
inst✝² : Algebra S S'
inst✝¹ : Algebra S' S''
inst✝ : Algebra S S''
⊢ ∀ (x : P.Ring), (algebraMap P.Ring S) ((RingHom.id P.Ring) x) = (algebraMap S S) ((algebraMap P.Ring S) x)

Tactic:
by 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''
r s : S
x : P.Cotangent
⊢ P.σ (r * s) - P.σ r * P.σ s ∈ P.ker

Tactic:
by 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''
x : P.Cotangent
⊢ P.σ 1 - 1 ∈ P.ker

Tactic:
by 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''
r s : S
x : P.Cotangent
⊢ P.σ (r + s) - (P.σ r + P.σ s) ∈ P.ker

Tactic:
by 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''
x : P.Cotangent
⊢ P.σ 0 ∈ P.ker

Tactic:
by 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 : P.Ring
x : P.Cotangent
⊢ P.σ ((algebraMap P.Ring S) r) - r ∈ P.ker

Tactic:
by 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''
x y : P.Cotangent
⊢ (x + y).val = x.val + y.val

Tactic:
by 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''
x : P.Ring
y : P.Cotangent
⊢ (x • y).val = (RingHom.id P.Ring) x • y.val

Tactic:
by 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''
x y : ↥P.ker
⊢ of (P.ker.toCotangent (x + y)) = of (P.ker.toCotangent x) + of (P.ker.toCotangent y)

Tactic:
by 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''
x : P.Ring
y : ↥P.ker
⊢ (of (P.ker.toCotangent (x • y))).val = ((RingHom.id P.Ring) x • of (P.ker.toCotangent y)).val

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
i : ι'
a : MvPolynomial (ι' ⊕ ι) R
⊢ (Q.aux P) (a * X (Sum.inl i)) = (Q.aux P) a * X i

Tactic:
by 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'
f : P.Hom P'
x : ↥P.ker
⊢ f.toAlgHom ↑x ∈ P'.ker

Tactic:
by simpa [-map_aeval] using RingHom.congr_arg (algebraMap S S') x.2

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

Tactic:
by 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 : S), (algebraMap P.Ring S) (P.σ x) = x

Tactic:
by 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 : σ
⊢ (algebraMap pres.Ring S) 0 = 0

Tactic:
by 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 : σ
⊢ pres.relation r ∈ pres.toExtension.ker

Tactic:
by 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 ι σ
⊢ ∀ (x y : σ →₀ S), (hom₁ pres) (x + y) = (hom₁ pres) x + (hom₁ pres) y

Tactic:
by 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 ι σ
⊢ ∀ (m : pres.Ring) (x : σ →₀ S), (hom₁ pres) (m • x) = (RingHom.id pres.Ring) m • (hom₁ pres) x

Tactic:
by 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 ι σ
φ : (σ →₀ 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:
by simp

Goal state after:
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✝
f✝ f'✝ : (⨁ (i : ι), M i) →ₗ[A] N✝
h' : (directSum solution).postcomp f✝ = (directSum solution).postcomp f'✝
⊢ f✝ = f'✝

Tactic:
by
    ext i : 1
    apply (h i).postcomp_injective
    ext g
    exact Solution.congr_var h' ⟨i, g⟩

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:
by 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:
by 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:
by 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:
by 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
P : Generators R T ι
i : ι
⊢ (aeval (extendScalars S P).val) (X i) = (algebraMap T T) (P.val i)

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

Goal state after: