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

Goal state before:
pp: case e_a
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
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ (g ((algebraMap P S) p) - p) * ↑m ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)

Tactic:
]

Goal state after:
case e_a
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
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ (g ((algebraMap P S) p) - p) * ↑m ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
⊢ ∀ ⦃B : Type u_3⦄ [inst : CommRing B] [inst_1 : Algebra K B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
⊢ ∀ ⦃B : Type u_3⦄ [inst : CommRing B] [inst_1 : Algebra K B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp
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
s : S
t : P
this✝ : Algebra S P := g.toAlgebra
this : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
⊢ s • ↑((derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg) t) =
    g s * t - g s * g ((algebraMap P S) t)

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
s : S
t : P
this✝ : Algebra S P := g.toAlgebra
this : IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
⊢ s • ↑((derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg) t) =
    g s * t - g s * g ((algebraMap P S) t)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
⊢ I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp

Tactic:
hI

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ K I).comp
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
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - y = ↑(l (1 ⊗ₜ[P] (D R P) (x - 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
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - y = ↑(l (1 ⊗ₜ[P] (D R P) (x - y)))
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
this✝ : f₁ x - f₂ x ∈ I
this : f₁ x = f₂ x
⊢ f₁ x = f₂ x

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
this✝ : f₁ x - f₂ x ∈ I
this : f₁ x = f₂ x
⊢ f₁ x = f₂ x
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
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
⊢ IsNilpotent ⊥.jacobson

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
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
⊢ ⊥ ≠ ⊤

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
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
⊢ IsNilpotent ⊥.jacobson

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
⊢ ⊥ ≠ ⊤
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.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
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)
⊢ ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap) ∘ₗ
      sec K A (A ⧸ IsLocalRing.maximalIdeal A) =
    TensorProduct.AlgebraTensorModule.lift (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip ∘ₗ
      sec K A (A ⧸ IsLocalRing.maximalIdeal A)

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
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)
⊢ ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap) ∘ₗ
      sec K A (A ⧸ IsLocalRing.maximalIdeal A) =
    TensorProduct.AlgebraTensorModule.lift (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip ∘ₗ
      sec K A (A ⧸ IsLocalRing.maximalIdeal A)
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 σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))

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 σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((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.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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
⊢ (algebraMap A (A ⧸ IsLocalRing.maximalIdeal A)) (f 1) = 1

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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
⊢ (algebraMap A (A ⧸ IsLocalRing.maximalIdeal A)) (f 1) = 1
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
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(↑l x) * ↑(↑l y) = 0
⊢ s * ↑(↑l (1 ⊗ₜ[P] (D R P) p)) - ↑(↑l (1 ⊗ₜ[P] (D R P) s)) * ↑(↑l (1 ⊗ₜ[P] (D R P) p)) =
    ↑(↑l ((algebraMap P S) s ⊗ₜ[P] (D R P) p))

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
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(↑l x) * ↑(↑l y) = 0
⊢ s * ↑(↑l (1 ⊗ₜ[P] (D R P) p)) - ↑(↑l (1 ⊗ₜ[P] (D R P) s)) * ↑(↑l (1 ⊗ₜ[P] (D R P) p)) =
    ↑(↑l ((algebraMap P S) s ⊗ₜ[P] (D R P) p))
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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
⊢ 0 = 0

Tactic:
]

Goal state after:
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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
⊢ f 1 = f 1

Tactic:
]

Goal state after:
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
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing 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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
n : ℕ
hn : IsLocalRing.maximalIdeal A ^ n = 0
⊢ (1 - f 1) ^ n ∈ IsLocalRing.maximalIdeal A ^ n

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
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing 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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
n : ℕ
hn : IsLocalRing.maximalIdeal A ^ n = 0
⊢ (1 - f 1) ^ n ∈ IsLocalRing.maximalIdeal A ^ n
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 : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (LinearMap.baseChange T P.toExtension.toKaehler) z =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) ↑(Q.kerCompPreimage P x))).2

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 : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (LinearMap.baseChange T P.toExtension.toKaehler) z =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) ↑(Q.kerCompPreimage P x))).2
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)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
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
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝¹ : Module.Finite K A
this✝ : IsArtinianRing 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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
n : ℕ
hn : IsLocalRing.maximalIdeal A ^ n = 0
this : (1 - f 1) ^ n = 0
⊢ 0 = 0

Tactic:
]

Goal state after: