awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
h :
  ∀ (x : Ω[S⁄R])
    (h : Membership.mem (γ := Set Ω[S⁄R]) (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R])) x),
    Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
h₁ : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) 0 : M) ((f' : (a : Ω[S⁄R]) → M) 0 : M)
h₂ :
  ∀ (x y : Ω[S⁄R])
    (hx :
      Membership.mem (γ := Submodule S Ω[S⁄R])
        (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x)
    (hy :
      Membership.mem (γ := Submodule S Ω[S⁄R])
        (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) y),
    Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M) →
      Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) y : M) ((f' : (a : Ω[S⁄R]) → M) y : M) →
        Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) (x + y) : M) ((f' : (a : Ω[S⁄R]) → M) (x + y) : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
have h₃ : ∀ (a : S) (x : Ω[S⁄R])
  (hx :
    Membership.mem (γ := Submodule S Ω[S⁄R])
      (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x),
  Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M) →
    Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) (a • x) : M) ((f' : (a : Ω[S⁄R]) → M) (a • x) : M)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) 0 : M) ((f' : (a : Ω[S⁄R]) → M) 0 : M)
have h : Eq.{u_1 + 1} (α := M) (0 : M) ((f' : (a : Ω[S⁄R]) → M) 0 : M)
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
h : Eq.{u_1 + 1} (α := M) (0 : M) ((f' : (a : Ω[S⁄R]) → M) 0 : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) 0 : M) ((f' : (a : Ω[S⁄R]) → M) 0 : M)
have h₁ : Eq.{u_1 + 1} (α := M) 0 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x_1 : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x_1
x y : Ω[S⁄R]
hx_1 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
hy_1 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) y
hx : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
hy : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) y : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) (x + y) : M) ((f' : (a : Ω[S⁄R]) → M) (x + y) : M)
have h : HAdd.hAdd (α := M) (β := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
  (f' : (a : Ω[S⁄R]) → M) (x + y)
Tactic: rw [map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x_1 : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x_1
x y : Ω[S⁄R]
hx_1 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
hy_1 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) y
hx : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
hy : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) y : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
h :
  HAdd.hAdd (α := M) (β := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
    (f' : (a : Ω[S⁄R]) → M) (x + y)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) (x + y) : M) ((f' : (a : Ω[S⁄R]) → M) (x + y) : M)
have h₁ : HAdd.hAdd (α := M) (β := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
  HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
Tactic: rw [map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x_1 : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x_1
x y : Ω[S⁄R]
hx_1 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
hy_1 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) y
hx : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
hy : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) y : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
h :
  HAdd.hAdd (α := M) (β := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
    (f' : (a : Ω[S⁄R]) → M) (x + y)
h₁ :
  HAdd.hAdd (α := M) (β := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
    HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) (x + y) : M) ((f' : (a : Ω[S⁄R]) → M) (x + y) : M)
have h₂ : HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
  HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
Tactic: rw [map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf :
  Eq (α := Derivation R S M)
    (((f.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
    (((f'.compDer : Derivation R S Ω[S⁄R] →ₗ[S] Derivation R S M) : (a : Derivation R S Ω[S⁄R]) → Derivation R S M)
        (KaehlerDifferential.D R S) :
      Derivation R S M)
x_1 : Ω[S⁄R]
this :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x_1
x y : Ω[S⁄R]
hx_1 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
hy_1 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) y
hx : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) x : M)
hy : Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) y : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
h :
  HAdd.hAdd (α := M) (β := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
    (f' : (a : Ω[S⁄R]) → M) (x + y)
h₁ :
  HAdd.hAdd (α := M) (β := M) ((f : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
    HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
h₂ :
  HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f : (a : Ω[S⁄R]) → M) y : M) =
    HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) (x + y) : M) ((f' : (a : Ω[S⁄R]) → M) (x + y) : M)
have h₃ : HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) y : M) =
  HAdd.hAdd (α := M) (β := M) ((f' : (a : Ω[S⁄R]) → M) x : M) ((f' : (a : Ω[S⁄R]) → M) y : M)
Tactic: rw [map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : ↥(ideal R S)
⊢ Eq (α := Ω[S⁄R]) ((Derivation.tensorProductTo (D R S) : (a : S ⊗[R] S) → Ω[S⁄R]) (↑x : S ⊗[R] S) : Ω[S⁄R])
    ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent) x :
      Ideal.Cotangent (R := S ⊗[R] S) (ideal R S))
have rw : Eq (α := Ω[S⁄R])
  ((LinearMap.id : (a : Ω[S⁄R]) → Ω[S⁄R])
      ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent) x) :
    Ω[S⁄R])
  ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent) x :
    Ideal.Cotangent (R := S ⊗[R] S) (ideal R S))
Tactic: rw [← Derivation.liftKaehlerDifferential_apply, Derivation.liftKaehlerDifferential_D]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : Ω[S⁄R]
⊢ ∃ (a : S ⊗[R] S), (Derivation.tensorProductTo (D R S) : (a : S ⊗[R] S) → Ω[S⁄R]) a = x
have obtain : ∀ (x : ↥(ideal R S)),
  ∃ (a : S ⊗[R] S),
    Eq (α := Ω[S⁄R]) ((Derivation.tensorProductTo (D R S) : (a : S ⊗[R] S) → Ω[S⁄R]) a : Ω[S⁄R])
      ((Ideal.toCotangent (ideal R S) : (a : ↥(ideal R S)) → (ideal R S).Cotangent) x :
        Ideal.Cotangent (R := S ⊗[R] S) (ideal R S))
Tactic: obtain ⟨x, rfl⟩ := (KaehlerDifferential.ideal R S).toCotangent_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
x : S
⊢ ((↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S) : (a : S ⊗[R] S) → S)
      ((TensorProduct.includeLeft : (a : S) → S ⊗[R] S) x : S ⊗[R] S) =
    x
have rw : (AlgHom.id R S : (a : S) → S) x = x
Tactic: rw [AlgHom.coe_toRingHom, ← AlgHom.comp_apply, TensorProduct.lmul'_comp_includeLeft]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
⊢ HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
      Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
      (Ideal.cotangentIdeal (ideal R S)) ≃+*
    S
have this : Function.RightInverse (α := S ⊗[R] S) (β := S) (⇑TensorProduct.includeLeft : (a : S) → S ⊗[R] S)
  (⇑(↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S) : (a : S ⊗[R] S) → S)
Tactic: have : Function.RightInverse (TensorProduct.includeLeft (R := R) (S := R) (A := S) (B := S))
      (↑(TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S) : S ⊗[R] S →+* S) := by
    intro x; rw [AlgHom.coe_toRingHom, ← AlgHom.comp_apply, TensorProduct.lmul'_comp_includeLeft]
    rfl
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
this :
  Function.RightInverse (α := S ⊗[R] S) (β := S) (⇑TensorProduct.includeLeft : (a : S) → S ⊗[R] S)
    (⇑(↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S) : (a : S ⊗[R] S) → S)
⊢ HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
      Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
      (Ideal.cotangentIdeal (ideal R S)) ≃+*
    S
have refine : HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (ideal R S) ≃+* S
Tactic: refine (Ideal.quotCotangent _).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
this :
  Function.RightInverse (α := S ⊗[R] S) (β := S) (⇑TensorProduct.includeLeft : (a : S) → S ⊗[R] S)
    (⇑(↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S) : (a : S ⊗[R] S) → S)
⊢ HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (ideal R S) ≃+* S
have refine : ideal R S = RingHom.ker (F := S ⊗[R] S →+* S) (↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S)
Tactic: refine (Ideal.quotEquivOfEq ?_).trans (RingHom.quotientKerEquivOfRightInverse this)
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
this :
  Function.RightInverse (α := S ⊗[R] S) (β := S) (⇑TensorProduct.includeLeft : (a : S) → S ⊗[R] S)
    (⇑(↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S) : (a : S ⊗[R] S) → S)
⊢ ideal R S = RingHom.ker (F := S ⊗[R] S →+* S) (↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S)
have h : ∀ (x : S ⊗[R] S),
  Membership.mem (γ := Ideal (S ⊗[R] S)) (ideal R S) x ↔
    Membership.mem (γ := Ideal (S ⊗[R] S))
      (RingHom.ker (F := S ⊗[R] S →+* S) (↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [AlgHom.ext_iff, AlgHom.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
x : S
⊢ Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x :
          S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
      S)
    ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
        ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
              (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
            ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x) :
          HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
            Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
            (Ideal.cotangentIdeal (ideal R S))) :
      S)
have generalize : ∀ (y : S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2),
  Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        y :
      S)
    ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
        ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
              (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
            y :
          HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
            Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
            (Ideal.cotangentIdeal (ideal R S))) :
      S)
Tactic: generalize f x = y
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
x : S
y : S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
⊢ Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        y :
      S)
    ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
        ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
              (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
            y :
          HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
            Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
            (Ideal.cotangentIdeal (ideal R S))) :
      S)
have obtain : ∀ (y : S ⊗[R] S),
  Eq (α := S)
    ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
          (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
        ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
              (a : S ⊗[R] S) → S ⊗[R] S ⧸ ideal R S ^ 2)
            y :
          S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
      S)
    ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
        ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
              (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
            ((Ideal.Quotient.mk (HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
                (a : S ⊗[R] S) → S ⊗[R] S ⧸ ideal R S ^ 2)
              y) :
          HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
            Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
            (Ideal.cotangentIdeal (ideal R S))) :
      S)
Tactic: obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2
x : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e₁ : Eq (α := S)
  ((AlgHom.kerSquareLift (TensorProduct.lmul' R) :
        (a : S ⊗[R] S ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) → S)
      ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x :
        S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) :
    S)
  ((quotientCotangentIdealRingEquiv R S : (a : (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) → S)
      ((Ideal.Quotient.mk (Ideal.cotangentIdeal (ideal R S)) :
            (a : S ⊗[R] S ⧸ ideal R S ^ 2) → (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)
          ((f : (a : S) → S ⊗[R] S ⧸ ideal R S ^ 2) x) :
        HasQuotient.Quotient (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2) (B :=
          Ideal (S ⊗[R] S ⧸ HPow.hPow (α := Ideal (S ⊗[R] S)) (β := ℕ) (ideal R S) 2))
          (Ideal.cotangentIdeal (ideal R S))) :
    S)
Tactic: have e₁ : (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift (f x) =
      KaehlerDifferential.quotientCotangentIdealRingEquiv R S
        (Ideal.Quotient.mk (KaehlerDifferential.ideal R S).cotangentIdeal <| f x) := by
    generalize f x = y; obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y; rfl