mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * 0) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) 0

pp: case tmul
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝ ⊗ₜ[R] y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ ⊗ₜ[R] y✝)

pp: case add
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S ⊗[R] S
a✝¹ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) x✝
a✝ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) y✝
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * (x✝ + y✝)) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ + y✝)

Tactic:
·

Goal state after:
case zero
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * 0) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) 0
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝ ⊗ₜ[R] y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ ⊗ₜ[R] y✝)

pp: case add
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S ⊗[R] S
a✝¹ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) x✝
a✝ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) y✝
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * (x✝ + y✝)) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ + y✝)

Tactic:
·

Goal state after:
case tmul
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝ ⊗ₜ[R] y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ ⊗ₜ[R] y✝)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2✝ : ↥Q.toExtension.ker = ↥Q.ker
⊢ ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom).toAlgHom x =
    ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) x

pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2✝ : ↥Q.toExtension.ker = ↥Q.ker
⊢ ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) x = ↑0

Tactic:
·

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2✝ : ↥Q.toExtension.ker = ↥Q.ker
⊢ ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom).toAlgHom x =
    ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) x
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S ⊗[R] S
a✝¹ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) x✝
a✝ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) y✝
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * (x✝ + y✝)) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ + y✝)

Tactic:
·

Goal state after:
case add
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S ⊗[R] S
a✝¹ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) x✝
a✝ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) y✝
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * (x✝ + y✝)) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ + y✝)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2✝ : ↥Q.toExtension.ker = ↥Q.ker
⊢ ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) x = ↑0

Tactic:
·

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2✝ : ↥Q.toExtension.ker = ↥Q.ker
⊢ ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) x = ↑0
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case e'_1
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ i, mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔ ∃ l, ↑P (mapBaseChange R P A) ∘ₗ l = LinearMap.id

pp: case e'_2
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective ⇑(↑P (mapBaseChange R P A)) ∧ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

Tactic:
·

Goal state after:
case e'_1
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ i, mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔ ∃ l, ↑P (mapBaseChange R P A) ∘ₗ l = LinearMap.id
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ ∀ (x : (Q.comp P).toExtension.Cotangent),
    (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0 →
      x ∈ (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
·

Goal state after:
case h2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ ∀ (x : (Q.comp P).toExtension.Cotangent),
    (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0 →
      x ∈ (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case e'_2
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective ⇑(↑P (mapBaseChange R P A)) ∧ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

Tactic:
·

Goal state after:
case e'_2
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective ⇑(↑P (mapBaseChange R P A)) ∧ ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (_root_.TensorProduct.lift (↑R (↑R (lsmul S S M).toLinearMap.flip).flip))
      ((TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip x)) (elem R S)) =
    (TensorProduct.lmul' R) (elem R S) • x

pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (TensorProduct.lmul' R) (elem R S) • x = x

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (_root_.TensorProduct.lift (↑R (↑R (lsmul S S M).toLinearMap.flip).flip))
      ((TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip x)) (elem R S)) =
    (TensorProduct.lmul' R) (elem R S) • x
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) → ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

pp: case mpr
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id) → ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id

Tactic:
·

Goal state after:
case mp
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) → ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (TensorProduct.lmul' R) (elem R S) • x = x

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (TensorProduct.lmul' R) (elem R S) • x = x
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case mpr
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id) → ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id

Tactic:
·

Goal state after:
case mpr
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id) → ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2.refine_1
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Q.toComp P).toAlgHom w ∈ (Q.comp P).toExtension.ker

pp: case h2.refine_2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Extension.Cotangent.map (Q.toComp P).toExtensionHom) (Extension.Cotangent.mk ⟨w, hw⟩) =
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩

Tactic:
·

Goal state after:
case h2.refine_1
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Q.toComp P).toAlgHom w ∈ (Q.comp P).toExtension.ker
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2.refine_2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Extension.Cotangent.map (Q.toComp P).toExtensionHom) (Extension.Cotangent.mk ⟨w, hw⟩) =
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩

Tactic:
·

Goal state after:
case h2.refine_2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Extension.Cotangent.map (Q.toComp P).toExtensionHom) (Extension.Cotangent.mk ⟨w, hw⟩) =
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case mp
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
⊢ (∃ g, (ofId R A).kerSquareLift.comp g = AlgHom.id R A) → IsIdempotentElem (RingHom.ker (algebraMap R A))

pp: case mpr
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
⊢ IsIdempotentElem (RingHom.ker (algebraMap R A)) → ∃ g, (ofId R A).kerSquareLift.comp g = AlgHom.id R A

Tactic:
·

Goal state after:
case mp
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
⊢ (∃ g, (ofId R A).kerSquareLift.comp g = AlgHom.id R A) → IsIdempotentElem (RingHom.ker (algebraMap R A))
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P) =
    Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom

Tactic:
apply (Q.comp P).cotangentSpaceBasis.ext
  intro i
  apply Q.cotangentSpaceBasis.repr.injective
  ext j
  simp only [compEquiv, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ofComp_val,
    LinearEquiv.trans_apply, Basis.repr_self, LinearMap.fst_apply, repr_CotangentSpaceMap]
  obtain (i | i) := i <;>
    simp only [Basis.repr_symm_apply, Finsupp.linearCombination_single, Basis.prod_apply,
      LinearMap.coe_inl, LinearMap.coe_inr, Sum.elim_inl, Function.comp_apply, one_smul,
      Basis.repr_self, Finsupp.single_apply, pderiv_X, Pi.single_apply,
      Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
      MonoidWithZeroHom.map_ite_one_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case mpr
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
⊢ IsIdempotentElem (RingHom.ker (algebraMap R A)) → ∃ g, (ofId R A).kerSquareLift.comp g = AlgHom.id R A

Tactic:
·

Goal state after:
case mpr
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
⊢ IsIdempotentElem (RingHom.ker (algebraMap R A)) → ∃ g, (ofId R A).kerSquareLift.comp g = AlgHom.id R A