mathlib-initiative/mathlib-tactics huggingface dataset:
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
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
this : f.toRingHom ↑x ∈ P'.ker ^ 2
⊢ mk x ∈ Submodule.restrictScalars P.Ring (map f).ker

Tactic:
by

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 ι σ
⊢ pres.toExtension.cotangentComplex ∘ₗ hom₁ pres =
    ↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map

Tactic:
by

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.differentialsRelations.R
⊢ (Finsupp.linearCombination S fun g ↦ (D R S) (pres.val g)) (pres.differentialsRelations.relation r) = 0

Tactic:
by

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 ι σ
⊢ pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm = LinearMap.id ∘ₗ pres.differentialsSolution.π

Tactic:
by

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 ι σ
⊢ pres.differentialsSolution.IsPresentation

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 ι
ι' : 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 ι
⊢ Generators T (T ⊗[R] S) ι

Tactic:
by

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
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun g ↦ s.var ⟨i, g⟩) ((relations i).relation r) = 0

Tactic:
by

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
t : (i : ι) → (relations i).Solution N
x✝ : (directSum relations).R
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun x ↦
        match x with
        | ⟨i, g⟩ => (t i).var g)
      ((directSum relations).relation ⟨i, r⟩) =
    0

Tactic:
by

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✝
s : (Relations.directSum relations).Solution N✝
⊢ (directSum solution).postcomp (toModule A ι N✝ fun i ↦ ⋯.desc (directSumEquiv s i)) = 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
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
⊢ (IsScalarTower.toAlgHom T (baseChange T P).toExtension.Ring (T ⊗[R] S)).comp ↑(algebraTensorAlgEquiv R T) =
    (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S)).comp
      (IsScalarTower.toAlgHom T P.toExtension.baseChange.Ring (T ⊗[R] S))

Tactic:
by

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

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
⊢ (IsScalarTower.toAlgHom T P.toExtension.baseChange.Ring (T ⊗[R] S)).comp ↑(algebraTensorAlgEquiv R T).symm =
    (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S)).comp
      (IsScalarTower.toAlgHom T (baseChange T P).toExtension.Ring (T ⊗[R] 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
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
b : ι' → S
s : S
⊢ ∃ a, (aeval (Sum.elim P.val b)) a = 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
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 ∘ ⇑e)) ((⇑(rename ⇑e.symm) ∘ P.σ) s) = s

Tactic:
conv_rhs => rw [← P.aeval_val_σ s]
    rw [← MvPolynomial.aeval_rename]
    simp

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

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (pres.finsupp ι).var ⟨i, g⟩ = Finsupp.single i (pres.var g)

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

Tactic:
by

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
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ ↑x - y ∈ P.ker ^ 2

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
pres : Presentation A M
inst✝¹ : Finite pres.G
inst✝ : Finite pres.R
⊢ pres.π.ker.FG

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
⊢ Function.Surjective ⇑(Finsupp.linearCombination A var)

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = (Finsupp.linearCombination A var).ker
r : R
⊢ (Finsupp.linearCombination A var) (relation r) = 0

Tactic:
by

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
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ ↑x - y + y = ↑x

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = (Finsupp.linearCombination A var).ker
⊢ { var := var, linearCombination_var_relation := ⋯ }.IsPresentation

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ FinitePresentation A M ↔ ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
by

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
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
⊢ Submodule.restrictScalars P.Ring (map f).ker =
    Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ 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
P : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : MvPolynomial σ R ⧸ I
⊢ (aeval fun i ↦ (Ideal.Quotient.mk I) (X i)) (s x) = 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 ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
⊢ algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I) = ↑(aeval fun i ↦ (Ideal.Quotient.mk I) (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
h : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(aeval fun i ↦ f (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
⊢ FiniteType R S ↔ ∃ n, Nonempty (Generators R S (Fin n))

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' ι'
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 : P.Ring
⊢ (aeval P'.val) (f.toAlgHom x) = (algebraMap S S') ((aeval P.val) 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' ι'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
v : ι →₀ ℕ
r : R
⊢ f.toAlgHom ((monomial v) r) = r • v.prod fun x1 x2 ↦ f.val x1 ^ x2

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 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 : ι
⊢ (aeval P'.val) (↑f (X i)) = (algebraMap S S') (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''
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
⊢ (fun f ↦ { val := fun i ↦ ↑f (X i), aeval_val := ⋯ }) ((fun f ↦ ⟨f.toAlgHom, ⋯⟩) f) = f

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝³ : Ring A
relations : Relations A
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsEmpty relations.R
r : relations.R
⊢ (Finsupp.linearCombination A fun g ↦ Finsupp.single g 1) (relations.relation r) = 0

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝³ : Ring A
relations : Relations A
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsEmpty relations.R
⊢ ∀ {N : Type w} [inst : AddCommGroup N] [inst_1 : Module A N] (s : relations.Solution N),
    relations.solutionFinsupp.postcomp (Finsupp.linearCombination A s.var) = 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
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) }
⊢ (fun f ↦ ⟨f.toAlgHom, ⋯⟩) ((fun f ↦ { val := fun i ↦ ↑f (X i), aeval_val := ⋯ }) f) = f

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

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : Ring A
relations : Relations A
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module A M
inst✝² : IsEmpty relations.R
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : (relations.G →₀ A) →ₗ[A] N✝
h : relations.solutionFinsupp.postcomp f✝ = relations.solutionFinsupp.postcomp f'✝
⊢ f✝ = f'✝

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type w₀
⊢ PEmpty.{w₁ + 1} → G →₀ 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
P : Generators R S ι
⊢ (Hom.id P).toAlgHom = AlgHom.id R P.Ring

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type w₀
⊢ { G := G, R := PEmpty.{w₁ + 1}, relation := fun r ↦ PEmpty.casesOn (fun x ↦ G →₀ A) r }.solutionFinsupp.IsPresentation

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type v
e : M ≃ₗ[A] G →₀ A
⊢ IsEmpty ((presentationFinsupp A G).ofLinearEquiv e.symm).R

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Free A M ↔ ∃ p, IsEmpty p.R

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✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
x : ι
⊢ (aeval P''.val) ((aeval f.val) (g.val x)) = (algebraMap S S'') (P.val 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' ι'
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'
⊢ f.comp (Hom.id P) = f

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' ι'
inst✝ : Algebra S S'
f : P.Hom P'
⊢ (Hom.id P').comp f = f

Tactic:
by

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

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''
⊢ S ⊗[P.Ring] ↥P.ker ≃ₗ[S] P.Cotangent

Tactic:
by

Goal state after: