mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x y : P
⊢ x + y - (g (f x) + g (f y)) = x - g (f x) + (y - g (f y))

Tactic:
;

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
x y : P
⊢ x + y - (g (f x) + g (f y)) = x - g (f x) + (y - g (f y))
Module: Mathlib.RingTheory.Unramified.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Ideal R
inst✝⁴ : P.IsPrime
Q' : Ideal (P.Fiber A)
inst✝³ : Q'.IsPrime
inst✝² : (Ideal.comap TensorProduct.includeRight.toRingHom Q').IsPrime
inst✝¹ : (Ideal.comap TensorProduct.includeRight.toRingHom Q').LiesOver P
inst✝ : IsUnramifiedAt R (Ideal.comap TensorProduct.includeRight.toRingHom Q')
f₀ : Localization.AtPrime (Ideal.comap TensorProduct.includeRight.toRingHom Q') →ₐ[R] Localization.AtPrime Q' :=
  Localization.localAlgHom (Ideal.comap TensorProduct.includeRight.toRingHom Q') Q' TensorProduct.includeRight ⋯
⊢ Function.Surjective ⇑f₀

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Ideal R
inst✝⁴ : P.IsPrime
Q' : Ideal (P.Fiber A)
inst✝³ : Q'.IsPrime
inst✝² : (Ideal.comap TensorProduct.includeRight.toRingHom Q').IsPrime
inst✝¹ : (Ideal.comap TensorProduct.includeRight.toRingHom Q').LiesOver P
inst✝ : IsUnramifiedAt R (Ideal.comap TensorProduct.includeRight.toRingHom Q')
f₀ : Localization.AtPrime (Ideal.comap TensorProduct.includeRight.toRingHom Q') →ₐ[R] Localization.AtPrime Q' :=
  Localization.localAlgHom (Ideal.comap TensorProduct.includeRight.toRingHom Q') Q' TensorProduct.includeRight ⋯
⊢ Function.Surjective ⇑f₀
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
x : ↥(RingHom.ker (algebraMap P S))
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S) x) = ↑(LinearMap.id x)

Tactic:
;

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
x : ↥(RingHom.ker (algebraMap P S))
⊢ ↑((retractionOfSectionOfKerSqZero g hf' hg ∘ₗ kerToTensor R P S) x) = ↑(LinearMap.id x)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(l x) * ↑(l y) ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)

Tactic:
;

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(l x) * ↑(l y) ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
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.Cotangent
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ
            LinearMap.baseChange T P.toExtension.cotangentComplex))
        1)
      x =
    ((AlgebraTensorModule.curry
          ((Q.comp P).toExtension.cotangentComplex ∘ₗ
            LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)))
        1)
      x

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.Cotangent
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ
            LinearMap.baseChange T P.toExtension.cotangentComplex))
        1)
      x =
    ((AlgebraTensorModule.curry
          ((Q.comp P).toExtension.cotangentComplex ∘ₗ
            LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)))
        1)
      x
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₃
σ : Type w₂
σ' : Type w₄
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
W : Generators R T τ
x✝ : (Q.comp P).toExtension.Cotangent
⊢ (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom ∘ₗ (Q.comp P).toExtension.cotangentComplex) x✝ =
    (Q.toExtension.cotangentComplex ∘ₗ Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x✝

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₃
σ : Type w₂
σ' : Type w₄
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
W : Generators R T τ
x✝ : (Q.comp P).toExtension.Cotangent
⊢ (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom ∘ₗ (Q.comp P).toExtension.cotangentComplex) x✝ =
    (Q.toExtension.cotangentComplex ∘ₗ Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x✝
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case e_f
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A := ⋯
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A := ⋯
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := ⋯
⊢ ∀ (x : A) (y : A ⧸ IsLocalRing.maximalIdeal A),
    (↑K ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap)) (x ⊗ₜ[K] y) =
      (↑K
          (TensorProduct.AlgebraTensorModule.lift
            (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip))
        (x ⊗ₜ[K] y)

Tactic:
intro r

Goal state after:
case e_f
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
r : A
⊢ ∀ (y : A ⧸ IsLocalRing.maximalIdeal A),
    (↑K ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap)) (r ⊗ₜ[K] y) =
      (↑K
          (TensorProduct.AlgebraTensorModule.lift
            (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip))
        (r ⊗ₜ[K] 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 σ
i : σ
| (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i))

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 σ
i : σ
| (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i))
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
l : { l // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(↑l x) * ↑(↑l y) ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)

Tactic:
;

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
l : { l // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(↑l x) * ↑(↑l y) ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
g : { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
s : S
⊢ ↑((fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩)
          ((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩) g))
      s =
    ↑g s

Tactic:
;

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
g : { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
s : S
⊢ ↑((fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩)
          ((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩) g))
      s =
    ↑g s
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
g : { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
s : P
⊢ ↑((fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩)
          ((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩) g))
      ((algebraMap P S) s) =
    ↑g ((algebraMap P S) s)

Tactic:
;

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
g : { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
s : P
⊢ ↑((fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩)
          ((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩) g))
      ((algebraMap P S) s) =
    ↑g ((algebraMap P S) s)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x✝ : P
hx✝ : x✝ ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
x y : P
hx : 1 ⊗ₜ[P] (D R P) x = 0
hy : 1 ⊗ₜ[P] (D R P) y = 0
⊢ 1 ⊗ₜ[P] (D R P) (x + y) = 0

Tactic:
;

Goal state after:
case refine_1.refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x✝ : P
hx✝ : x✝ ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
x y : P
hx : 1 ⊗ₜ[P] (D R P) x = 0
hy : 1 ⊗ₜ[P] (D R P) y = 0
⊢ 1 ⊗ₜ[P] (D R P) (x + y) = 0
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
⊢ 1 ⊗ₜ[P] (D R P) 1 = 0

Tactic:
;

Goal state after:
case refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
⊢ 1 ⊗ₜ[P] (D R P) 1 = 0
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hz.snd
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.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := ⋯
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace := ⋯
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).2 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2

pp: case hz.fst
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.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := ⋯
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace := ⋯
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).1 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).1

Tactic:
;

Goal state after:
case hz.snd
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.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := ⋯
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace := ⋯
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).2 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2

case hz.fst
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.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := ⋯
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace := ⋯
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).1 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).1
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x✝ : A
hx : IsNilpotent x✝
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
x : A
⊢ f x = (LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap) x

Tactic:
;

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x✝ : A
hx : IsNilpotent x✝
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
x : A
⊢ f x = (LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap) x
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hF
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.H1Cotangent
⊢ ((Extension.Cotangent.map (Q.ofComp P).toExtensionHom ∘ₗ Extension.h1Cotangentι) x).val =
    ((Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) x).val

Tactic:
;

Goal state after:
case hF
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.H1Cotangent
⊢ ((Extension.Cotangent.map (Q.ofComp P).toExtensionHom ∘ₗ Extension.h1Cotangentι) x).val =
    ((Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) x).val
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring Q.Ring T
this : FormallyEtale P.Ring Q.Ring
x✝ : Q.CotangentSpace
a✝ : Q.Ring
x : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]
hx : (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring) x = (D R Q.Ring) a✝
a : P.Ring
⊢ 1 ⊗ₜ[Q.Ring] (D R Q.Ring) (f.toRingHom a) = 1 ⊗ₜ[Q.Ring] (D R Q.Ring) ((algebraMap P.Ring Q.Ring) a)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring Q.Ring T
this : FormallyEtale P.Ring Q.Ring
x✝ : Q.CotangentSpace
a✝ : Q.Ring
x : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]
hx : (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring) x = (D R Q.Ring) a✝
a : P.Ring
⊢ 1 ⊗ₜ[Q.Ring] (D R Q.Ring) (f.toRingHom a) = 1 ⊗ₜ[Q.Ring] (D R Q.Ring) ((algebraMap P.Ring Q.Ring) a)
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ⋯
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker := ⋯
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent := ⋯
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
⊢ (↑b • Cotangent.mk d).val = Cotangent.val 0

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ⋯
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker := ⋯
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent := ⋯
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
⊢ (↑b • Cotangent.mk d).val = Cotangent.val 0