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

Goal state after:
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✝
Module: Mathlib.RingTheory.Extension.Generators

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

Tactic:
by
  simp [ker_eq_ker_aeval_val, SetLike.ext_iff, aeval_X_left]

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

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 ι
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✝)
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
x✝ : P
⊢ x✝ ∈ RingHom.ker (algebraMap P S) → x✝ ∈ 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
x✝ : P
⊢ x✝ ∈ RingHom.ker (algebraMap P S) → x✝ ∈ 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✝ : P.Ring
⊢ (((AlgebraTensorModule.curry (CotangentSpace.map (Hom.id P))) 1).compDer (D R P.Ring)) a✝ =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R 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✝ : P.Ring
⊢ (((AlgebraTensorModule.curry (CotangentSpace.map (Hom.id P))) 1).compDer (D R P.Ring)) a✝ =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R 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 : P.Cotangent
⊢ (CotangentSpace.map f ∘ₗ P.cotangentComplex) x = (↑S P'.cotangentComplex ∘ₗ Cotangent.map f) x

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : P.Cotangent
⊢ (CotangentSpace.map f ∘ₗ P.cotangentComplex) x = (↑S P'.cotangentComplex ∘ₗ Cotangent.map f) 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
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 ι
x : ↥Q.ker
⊢ ↥(Q.comp P).ker

Tactic:
by
  refine ⟨(AddMonoidAlgebra.coeff x.1).sum fun n r ↦ ?_, ?_⟩
  · -- The use of `refine` is intentional to control the elaboration order
    -- so that the term has type `(Q.comp P).Ring` and not `MvPolynomial (Q.ι ⊕ P.ι) R`
    refine rename ?_ (P.σ r) * monomial ?_ 1
    exacts [Sum.inr, n.mapDomain Sum.inl]
  · simp only [ker_eq_ker_aeval_val, RingHom.mem_ker]
    conv_rhs => rw [← aeval_val_eq_zero x.2, ← x.1.support_sum_monomial_coeff]
    simp only [Finsupp.sum, map_sum, map_mul, aeval_rename, Function.comp_def, comp_val,
      Sum.elim_inr, aeval_monomial, map_one, Finsupp.prod_mapDomain_index_inj Sum.inl_injective,
      Sum.elim_inl, one_mul]
    congr! with v i
    simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ,
      coeff]

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
x✝ : P.H1Cotangent
⊢ (↑((map (Hom.id P)) x✝)).val = (↑(LinearMap.id x✝)).val

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.H1Cotangent
⊢ (↑((map (Hom.id P)) x✝)).val = (↑(LinearMap.id x✝)).val
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'
g : P'.Hom P''
x✝ : P.H1Cotangent
⊢ (↑((map (g.comp f)) x✝)).val = (↑((↑S (map g) ∘ₗ map f) x✝)).val

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x✝ : P.H1Cotangent
⊢ (↑((map (g.comp f)) x✝)).val = (↑((↑S (map g) ∘ₗ map f) x✝)).val
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
P₁ : Extension R S
P₂ : Extension R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₁.H1Cotangent
⊢ (↑S (map f₂) ∘ₗ map f₁) x = (map f₂ ∘ₗ map f₁) x

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
P₁ : Extension R S
P₂ : Extension R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₁.H1Cotangent
⊢ (↑S (map f₂) ∘ₗ map f₁) x = (map f₂ ∘ₗ map f₁) x
Module: Mathlib.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 : Extension R S
⊢ (IsScalarTower.toAlgHom R P.Ring S).comp (aeval P.σ) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R (Generators.self R S).Ring S)

Tactic:
;

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom R P.Ring S).comp (aeval P.σ) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R (Generators.self R S).Ring S)
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 : Extension R S
i✝ : S
⊢ ((IsScalarTower.toAlgHom R P.Ring S).comp (aeval P.σ)) (X i✝) =
    ((IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R (Generators.self R S).Ring S)) (X i✝)

Tactic:
;

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
i✝ : S
⊢ ((IsScalarTower.toAlgHom R P.Ring S).comp (aeval P.σ)) (X i✝) =
    ((IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R (Generators.self R S).Ring S)) (X i✝)
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
P₁ : Extension R S
P₂ : Extension R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₂.H1Cotangent
⊢ (↑S (map f₁) ∘ₗ map f₂) x = (map f₁ ∘ₗ map f₂) x

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
P₁ : Extension R S
P₂ : Extension R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₂.H1Cotangent
⊢ (↑S (map f₁) ∘ₗ map f₂) x = (map f₁ ∘ₗ map f₂) x
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
ι : Type u_2
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : ι → Ideal R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)))) 1) x✝ =
    ((AlgebraTensorModule.curry
          (↑(piLeft R M fun i ↦ R ⧸ I i).symm ∘ₗ
            (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1) ∘ₗ ↑(TensorProduct.lid R M)))
        1)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
ι : Type u_2
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : ι → Ideal R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)))) 1) x✝ =
    ((AlgebraTensorModule.curry
          (↑(piLeft R M fun i ↦ R ⧸ I i).symm ∘ₗ
            (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1) ∘ₗ ↑(TensorProduct.lid R M)))
        1)
      x✝
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R (Presentation.ofFinitePresentation R S).Ring

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R (Presentation.ofFinitePresentation R S).Ring
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : x' f' = 0
k : ℕ
a' : (Fin l →₀ R) →ₗ[R] Fin k →₀ R
y' : (Fin k →₀ R) →ₗ[R] M
ha'y' : x' = y' ∘ₗ a'
ha' : a' f' = 0
j : Fin k
⊢ ∑ i, f i * (fun i ↦ ⇑(a' (Finsupp.single i 1))) i j = 0

Tactic:
simp_rw [← smul_eq_mul, ← Finsupp.smul_apply, ← map_smul, ← finsetSum_apply, ← map_sum,
        smul_single, smul_eq_mul, mul_one,
        ← (fun _ ↦ equivFunOnFinite_symm_apply_apply _ _ : ∀ x, f' x = f x), univ_sum_single]

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : x' f' = 0
k : ℕ
a' : (Fin l →₀ R) →ₗ[R] Fin k →₀ R
y' : (Fin k →₀ R) →ₗ[R] M
ha'y' : x' = y' ∘ₗ a'
ha' : a' f' = 0
j : Fin k
⊢ (a' (equivFunOnFinite.symm f)) j = 0
Module: Mathlib.RingTheory.QuotSMulTop

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x✝ : M
⊢ ((map r) f ∘ₗ (r • ⊤).mkQ) x✝ = ((r • ⊤).mkQ ∘ₗ f) x✝

Tactic:
;

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x✝ : M
⊢ ((map r) f ∘ₗ (r • ⊤).mkQ) x✝ = ((r • ⊤).mkQ ∘ₗ f) x✝
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R (Presentation.ofFinitePresentation R S).Ring

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
⊢ FiniteType R (Presentation.ofFinitePresentation R S).Ring