awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this_8 : Nontrivial.{u_2} (S ⧸ mR)
this : IsLocalRing.{u_2} (S ⧸ mR)
rw : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.jacobson ⊥) ⊥
rw₁ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical ⊥) ⊥
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥
have rw₂ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical 0) 0
Tactic: rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this_8 : Nontrivial.{u_2} (S ⧸ mR)
this : IsLocalRing.{u_2} (S ⧸ mR)
rw : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.jacobson ⊥) ⊥
rw₁ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical ⊥) ⊥
rw₂ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical 0) 0
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥
have rw₃ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (nilradical (S ⧸ mR)) 0
Tactic: rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this_8 : Nontrivial.{u_2} (S ⧸ mR)
this : IsLocalRing.{u_2} (S ⧸ mR)
rw : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.jacobson ⊥) ⊥
rw₁ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical ⊥) ⊥
rw₂ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (Ideal.radical 0) 0
rw₃ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (nilradical (S ⧸ mR)) 0
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥
have rw₄ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) 0 0
Tactic: rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this_8 : Nontrivial.{u_2} (S ⧸ mR)
this : IsLocalRing.{u_2} (S ⧸ mR)
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have this₁ : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥
Tactic: have : maximalIdeal (S ⧸ mR) = ⊥ := by
    rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical,
      ← Ideal.zero_eq_bot, ← nilradical, nilradical_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
mR : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this_1 : Algebra.{u_1, u_2} (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun (x1 : R) (x2 : S) ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯,
    commutes' := ⋯, smul_def' := ⋯ }
this_2 : IsScalarTower.{u_1, u_1, u_2} R (ResidueField R) (S ⧸ mR)
this_3 : FormallyUnramified.{u_2, u_1} (ResidueField R) (S ⧸ mR)
this_4 : EssFiniteType.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_5 : Module.Finite.{u_1, u_2} (ResidueField R) (S ⧸ mR)
this_6 : IsReduced.{u_2} (S ⧸ mR)
this_7 : IsArtinianRing.{u_2} (S ⧸ mR)
this_8 : Nontrivial.{u_2} (S ⧸ mR)
this_9 : IsLocalRing.{u_2} (S ⧸ mR)
this : Eq.{u_2 + 1} (α := Ideal (S ⧸ mR)) (maximalIdeal (S ⧸ mR)) ⊥
⊢ IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
have rwa : ∀ (this : IsField.{u_2} (S ⧸ mR)),
  IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
Tactic: rwa [← isField_iff_maximalIdeal_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
⊢ Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
have hI : Ideal.IsMaximal.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))
Tactic: apply eq_maximalIdeal
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : FormallyUnramified R S
⊢ Ideal.IsMaximal.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))
have hI : IsField.{u_2} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
Tactic: rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
⊢ FormallyUnramified R S
have subsingleton_kaehlerDifferential : Subsingleton.{u_2 + 1} Ω[S⁄R]
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]
have this : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
Tactic: have : FormallyUnramified (ResidueField R) (ResidueField S) := .of_isSeparable _ _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]
have this₁ : FormallyUnramified.{u_2, u_1} R (ResidueField S)
Tactic: have : FormallyUnramified R (ResidueField S) := .comp _ (ResidueField R) _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]
have subsingleton_kaehlerDifferential : Subsingleton.{u_2 + 1} (TensorProduct S (ResidueField S) Ω[S⁄R])
Tactic: rw [← subsingleton_tensorProduct (R := S)]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
⊢ Subsingleton.{u_2 + 1} (TensorProduct S (ResidueField S) Ω[S⁄R])
have subsingleton_kaehlerDifferential : ∀ (x : TensorProduct S (ResidueField S) Ω[S⁄R]), x = 0
Tactic: refine subsingleton_of_forall_eq 0 fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : TensorProduct S (ResidueField S) Ω[S⁄R]
⊢ x = 0
have subsingleton_kaehlerDifferential : ∀ (x : Ideal.Cotangent (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S)))),
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    ((KaehlerDifferential.kerCotangentToTensor R S (ResidueField S) :
          (a : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent) → TensorProduct S (ResidueField S) Ω[S⁄R])
        x :
      TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
Tactic: obtain ⟨x, rfl⟩ := (KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange R S
    (ResidueField S) Ideal.Quotient.mk_surjective x).mp (Subsingleton.elim _ _)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : Ideal.Cotangent (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S)))
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    ((KaehlerDifferential.kerCotangentToTensor R S (ResidueField S) :
          (a : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent) → TensorProduct S (ResidueField S) Ω[S⁄R])
        x :
      TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
have subsingleton_kaehlerDifferential : ∀ (x : S)
  (hx : Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x),
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    ((KaehlerDifferential.kerCotangentToTensor R S (ResidueField S) :
          (a : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent) → TensorProduct S (ResidueField S) Ω[S⁄R])
        ((Ideal.toCotangent (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) :
            (a : ↥(RingHom.ker (algebraMap S (ResidueField S)))) →
              (RingHom.ker (algebraMap S (ResidueField S))).Cotangent)
          (Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x) x
            hx)) :
      TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
Tactic: obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : S
hx : Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    ((KaehlerDifferential.kerCotangentToTensor R S (ResidueField S) :
          (a : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent) → TensorProduct S (ResidueField S) Ω[S⁄R])
        ((Ideal.toCotangent (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) :
            (a : ↥(RingHom.ker (algebraMap S (ResidueField S)))) →
              (RingHom.ker (algebraMap S (ResidueField S))).Cotangent)
          (Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x) x
            hx)) :
      TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
have subsingleton_kaehlerDifferential : Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
  (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
  (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
Tactic: simp only [KaehlerDifferential.kerCotangentToTensor_toCotangent]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x : S
hx : Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* ResidueField S) (algebraMap S (ResidueField S))) x
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
have hx₁ : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) x
Tactic: replace hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R) := by simpa [H] using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 x : S
h : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R)) x
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
have subsingleton_kaehlerDifferential : ∀ (x : R) (hx : x ∈ (↑(maximalIdeal R) : Set R)),
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) ((algebraMap R S : (a : R) → S) x) :
      TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
Tactic: obtain ⟨x, hx, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 a x : S
hx :
  Membership.mem (γ := Submodule S S)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) x
h :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) x : ResidueField S) (0 : ResidueField S)
have rwa : Membership.mem (γ := Ideal S) (maximalIdeal S) x
Tactic: rwa [residue_eq_zero_iff, ← H]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 a x : S
hx :
  Membership.mem (γ := Submodule S S)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) x
h :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
rwa : Membership.mem (γ := Ideal S) (maximalIdeal S) x
⊢ Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) x : ResidueField S) (0 : ResidueField S)
have rwa₁ : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) x
Tactic: rwa [residue_eq_zero_iff, ← H]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : IsLocalRing S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_6 : EssFiniteType R S
inst_7 : Algebra.IsSeparable.{u_1, u_2} (ResidueField R) (ResidueField S)
H : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) (maximalIdeal S)
this_1 : FormallyUnramified.{u_2, u_1} (ResidueField R) (ResidueField S)
this : FormallyUnramified.{u_2, u_1} R (ResidueField S)
x_1 a x : S
hx :
  Membership.mem (γ := Submodule S S)
    (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑(maximalIdeal R) : Set R))) x
h :
  Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
⊢ Eq (α := TensorProduct S (ResidueField S) Ω[S⁄R])
    (1 ⊗ₜ[S] (KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) (a • x) : TensorProduct S (ResidueField S) Ω[S⁄R])
    (0 : TensorProduct S (ResidueField S) Ω[S⁄R])
have this₁ : Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) x : ResidueField S) (0 : ResidueField S)
Tactic: have : residue S x = 0 := by rwa [residue_eq_zero_iff, ← H]