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

Goal state before:
pp: case refine_3.exac
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
⊢ Function.Exact ⇑(baseChange S g) ⇑(baseChange S f)

pp: case surj
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
⊢ Function.Surjective ⇑(baseChange S f)

Tactic:
· exact lTensor_exact S hfg hf

Goal state after:
case surj
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
⊢ Function.Surjective ⇑(baseChange S f)
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
g : R →+* MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1} := (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C
⊢ IsUnit ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r))

Tactic:
isUnit_iff_exists_inv

Goal state after:
σ : 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
g : R →+* MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1} := (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C
⊢ ∃ b, (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (C r) * b = 1
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ((auxHom S r).comp (auxInv S r)).comp (algebraMap R S) = (RingHom.id S).comp (algebraMap R S)

Tactic:
ext x

Goal state after:
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : R
⊢ (((auxHom S r).comp (auxInv S r)).comp (algebraMap R S)) x = ((RingHom.id S).comp (algebraMap R S)) x
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ((auxInv S r).comp (auxHom S r).toRingHom).comp (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) =
    (RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
      (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))

Tactic:
ext x

Goal state after:
case hC
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : R
⊢ ((((auxInv S r).comp (auxHom S r).toRingHom).comp (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))).comp C) x =
    (((RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
            (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))).comp
        C)
      x

case hX
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : Unit
⊢ (((auxInv S r).comp (auxHom S r).toRingHom).comp (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))) (X x) =
    ((RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp
        (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})))
      (X x)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ aeval (Generators.localizationAway S r).val =
    (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))

Tactic:
ext x

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : Unit
⊢ (aeval (Generators.localizationAway S r).val) (X x) =
    ((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (X x)
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 ι σ
⊢ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P) = Set.range Q.relation

Tactic:
ext x

Goal state after:
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 ι σ
x : MvPolynomial ι' S
⊢ x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P) ↔ x ∈ Set.range Q.relation
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
⊢ map (Hom.id P) = LinearMap.id

Tactic:
ext x

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.Cotangent
⊢ ((map (Hom.id P)) x).val = (LinearMap.id x).val
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_1
S' : Type u_2
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type u_4
S'' : Type u_5
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''
f : P.Hom P'
g : P'.Hom P''
⊢ map (g.comp f) = ↑S (map g) ∘ₗ map f

Tactic:
ext x

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_1
S' : Type u_2
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type u_4
S'' : Type u_5
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''
f : P.Hom P'
g : P'.Hom P''
x : P.Cotangent
⊢ ((map (g.comp f)) x).val = ((↑S (map g) ∘ₗ map f) x).val
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 ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span (Set.range (Q.compRelationAux P)) ⊔ Ideal.span (Set.range fun rp ↦ (rename Sum.inr) (P.relation rp)) =
    Ideal.span (Set.range (Q.compRelationAux P)) ⊔ RingHom.ker (Q.aux P)

Tactic:
Q.aux_ker,

Goal state after:
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 ι σ
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ Ideal.span (Set.range (Q.compRelationAux P)) ⊔ Ideal.span (Set.range fun rp ↦ (rename Sum.inr) (P.relation rp)) =
    Ideal.span (Set.range (Q.compRelationAux P)) ⊔ Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case mul_X
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 ι
a : T
b : S
X : P.Ring := P.σ b
p : MvPolynomial ι R
i : ι
hp : (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) p = 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) p
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] P.val x) (p * MvPolynomial.X i) = 1 ⊗ₜ[R] (aeval fun x ↦ P.val x) (p * MvPolynomial.X i)

Tactic:
simp [hp]

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:
ext x

Goal state after:
case hC
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 : R
⊢ ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)).comp C) x =
    ((↑(aeval fun i ↦ (Ideal.Quotient.mk I) (X i))).comp C) x

case hX
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 : σ
⊢ (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I)) (X x) = ↑(aeval fun i ↦ (Ideal.Quotient.mk I) (X i)) (X 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
P : Extension R S
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ cotangentComplexBaseChange R S P.Ring A =
    ↑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ₗ
      LinearMap.baseChange A P.cotangentComplex ∘ₗ
        ↑((AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
            LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv)

Tactic:
ext x

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
x : ↥(RingHom.ker (algebraMap P.Ring S))
⊢ ((AlgebraTensorModule.curry (cotangentComplexBaseChange R S P.Ring A)) 1) x =
    ((AlgebraTensorModule.curry
          (↑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ₗ
            LinearMap.baseChange A P.cotangentComplex ∘ₗ
              ↑((AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ
                  LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv)))
        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
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''
⊢ CotangentSpace.map (g.comp f) = ↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f

Tactic:
ext x

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.CotangentSpace
⊢ (CotangentSpace.map (g.comp f)) x = (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) x
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: case tmul.tmul
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 : S
x✝ y✝ : P.Ring
⊢ (CotangentSpace.map (g.comp f)) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝)) =
    (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ ⊗ₜ[R] y✝))

Tactic:
simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', map_tmul,
        Hom.toAlgHom_apply, Hom.comp_toRingHom, RingHom.coe_comp, Function.comp_apply,
        LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        ← IsScalarTower.algebraMap_apply S S' S'']

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
⊢ CotangentSpace.map f ∘ₗ P.cotangentComplex = ↑S P'.cotangentComplex ∘ₗ Cotangent.map f

Tactic:
ext x

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.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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
⊢ CotangentSpace.map f - CotangentSpace.map g = ↑S P'.cotangentComplex ∘ₗ f.sub g

Tactic:
ext x

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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : P.CotangentSpace
⊢ (CotangentSpace.map f - CotangentSpace.map g) x = (↑S P'.cotangentComplex ∘ₗ f.sub g) 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
ι' : 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 ι
⊢ Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker = Q.ker

Tactic:
ext x

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 ι
x : Q.Ring
⊢ x ∈ Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker ↔ x ∈ Q.ker
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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
⊢ map f - map g = f.sub g ∘ₗ P.cotangentComplex

Tactic:
ext x

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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : P.Cotangent
⊢ ((map f - map g) x).val = ((f.sub g ∘ₗ P.cotangentComplex) 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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
⊢ map f = map g

Tactic:
ext x

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'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : P.H1Cotangent
⊢ (↑((map f) x)).val = (↑((map g) x)).val
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ p ∉ support R M ↔ ∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0

Tactic:
by
  simp only [notMem_support_iff, Ideal.primeCompl, LocalizedModule.subsingleton_iff,
    Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff, SetLike.mem_coe]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₂ : span 𝓀 s = ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
⊢ ⇑((mk R 𝓀 ↥N) 1) '' t = s

Tactic:
← Set.image_comp,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₂ : span 𝓀 s = ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
⊢ ⇑((mk R 𝓀 ↥N) 1) ∘ Function.surjInv ⋯ '' s = s
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
⊢ ⊤ ≤ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))

Tactic:
by rw [hsp]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis κ R ↥M
n : Basis ι R ↥N
H : Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ ↑(i0 ≪≫ₗ i1.symm)
⊢ i = Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
ext x

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis κ R ↥M
n : Basis ι R ↥N
H : Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := ⋯
i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := ⋯
i : (κ × ι →₀ R) →ₗ[R] S := ⋯
x : κ × ι
⊢ (i ∘ₗ Finsupp.lsingle x) 1 = ((Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2)) ∘ₗ Finsupp.lsingle x) 1