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
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₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Algebra R₁ S
inst✝² : Algebra R₂ S
inst✝¹ : Algebra R₁ R₂
inst✝ : IsScalarTower R₁ R₂ S
⊢ IsScalarTower R₁ R₂ P.Cotangent

Tactic:
constructor

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.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₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Algebra R₁ S
inst✝² : Algebra R₂ S
inst✝¹ : Algebra R₁ R₂
inst✝ : IsScalarTower R₁ R₂ S
⊢ ∀ (x : R₁) (y : R₂) (z : P.Cotangent), (x • y) • z = x • y • z
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'
r : S
x : P.Cotangent
⊢ of ((P.ker.mapCotangent P'.ker f.toAlgHom ⋯) (r • x).val) =
    (RingHom.id S) r • of ((P.ker.mapCotangent P'.ker f.toAlgHom ⋯) x.val)

Tactic:
ext

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.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'
r : S
x : P.Cotangent
⊢ (of ((P.ker.mapCotangent P'.ker f.toAlgHom ⋯) (r • x).val)).val =
    ((RingHom.id S) r • of ((P.ker.mapCotangent P'.ker f.toAlgHom ⋯) x.val)).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 ι σ
x : MvPolynomial ι' S
⊢ x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P) ↔ x ∈ Set.range Q.relation

Tactic:
constructor

Goal state after:
case mp
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

case mpr
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 ∈ Set.range Q.relation → x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case e_a
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
⊢ (Set.range fun rp ↦ (rename Sum.inr) (P.relation rp)) = ⇑(rename Sum.inr) '' Set.range P.relation

Tactic:
ext

Goal state after:
case e_a
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
x✝ : MvPolynomial (ι' ⊕ ι) R
⊢ (x✝ ∈ Set.range fun rp ↦ (rename Sum.inr) (P.relation rp)) ↔ x✝ ∈ ⇑(rename Sum.inr) '' Set.range P.relation
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S ι
I : Type u_1
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective ⇑f
⊢ aeval (⇑f ∘ X) = f

Tactic:
ext

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 ι
I : Type u_1
f : MvPolynomial I R →ₐ[R] S
h : Function.Surjective ⇑f
i✝ : I
⊢ (aeval (⇑f ∘ X)) (X i✝) = f (X i✝)
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 =
    Finsupp.linearCombination S fun g ↦ (D R S) (pres.val g)

Tactic:
ext

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
a✝ : ι
⊢ ((pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm) ∘ₗ Finsupp.lsingle a✝) 1 =
    ((Finsupp.linearCombination S fun g ↦ (D R S) (pres.val g)) ∘ₗ Finsupp.lsingle a✝) 1
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.cotangentSpaceBasis.repr (1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r)) =
    pres.cotangentSpaceBasis.repr
      ((Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
        (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
          ((mvPolynomialBasis R ι).repr ((D R (MvPolynomial ι R)) (pres.relation r)))))

Tactic:
ext

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
r : σ
a✝ : ι
⊢ (pres.cotangentSpaceBasis.repr (1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r))) a✝ =
    (pres.cotangentSpaceBasis.repr
        ((Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
          (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
            ((mvPolynomialBasis R ι).repr ((D R (MvPolynomial ι R)) (pres.relation r))))))
      a✝
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 ι σ
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤ ∧
    pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
constructor

Goal state after:
case left
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤

case right
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.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
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).Ring (T ⊗[R] S)).comp ↑(algebraTensorAlgEquiv R T) =
    (IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S)).comp (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S))

Tactic:
ext

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 ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
i✝ : ι
⊢ ((AlgHom.restrictScalars R
            ((IsScalarTower.toAlgHom T (baseChange T P).Ring (T ⊗[R] S)).comp ↑(algebraTensorAlgEquiv R T))).comp
        TensorProduct.includeRight)
      (X i✝) =
    ((AlgHom.restrictScalars R
            ((IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S)).comp
              (IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S)))).comp
        TensorProduct.includeRight)
      (X i✝)
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 (T ⊗[R] P.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).Ring (T ⊗[R] S))

Tactic:
ext

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 ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
i✝ : ι
⊢ ((IsScalarTower.toAlgHom T (T ⊗[R] P.Ring) (T ⊗[R] S)).comp ↑(algebraTensorAlgEquiv R T).symm) (X i✝) =
    ((IsScalarTower.toAlgHom T (T ⊗[R] S) (T ⊗[R] S)).comp (IsScalarTower.toAlgHom T (baseChange T P).Ring (T ⊗[R] S)))
      (X i✝)
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
⊢ (directSum fun x ↦ pres).var ⟨i, g⟩ = (finsuppLequivDFinsupp A) (Finsupp.single i (pres.var g))

Tactic:
rw [directSum_var, finsuppLequivDFinsupp_apply_apply, Finsupp.toDFinsupp_single]

Goal state after:
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
⊢ (lof A ι (fun x ↦ N) i) (pres.var g) = DFinsupp.single i (pres.var g)
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:
constructor

Goal state after:
case mp
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

case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ pres, Finite pres.G ∧ Finite pres.R) → FinitePresentation A M
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:
ext

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

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

Goal state after:
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'✝
a✝ : relations.G
⊢ (f✝ ∘ₗ Finsupp.lsingle a✝) 1 = (f'✝ ∘ₗ Finsupp.lsingle a✝) 1
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:
constructor

Goal state after:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Free A M → ∃ p, IsEmpty p.R

case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ p, IsEmpty p.R) → Free A M
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:
ext

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' ι'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ ((f.comp (Hom.id P)).val x✝) = coeff m✝ (f.val x✝)
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:
ext

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' ι'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : ι
m✝ : ι' →₀ ℕ
⊢ coeff m✝ (((Hom.id P').comp f).val x✝) = coeff m✝ (f.val 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 ι
p : P.Ring
⊢ (Q.ofComp P).toAlgHom.comp (rename Sum.inr) =
    (IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)

Tactic:
ext

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

Goal state before:
pp: case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
⊢ ∀ (a : presM.R) (b : B) (f : presM.R →₀ B),
    a ∉ f.support →
      b ≠ 0 →
        f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single a b + f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
intro r b w _ _ hw

Goal state after:
case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
b : B
w : presM.R →₀ B
a✝¹ : r ∉ w.support
a✝ : b ≠ 0
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
⊢ Finsupp.single r b + w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S ι
⊢ (Hom.id P).toExtensionHom = Extension.Hom.id P.toExtension

Tactic:
ext

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

Tactic:
ext

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.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
⊢ CotangentSpace.map (Hom.id P) = LinearMap.id

Tactic:
ext

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.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i, a i j • m i = 0
⊢ ∑ y_1, ∑ x, a x y_1 • m x ⊗ₜ[R] y y_1 = 0

Tactic:
simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]

Goal state after: