awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.Basic
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 : S
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) ((KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) : M)
    ((f' : (a : Ω[S⁄R]) → M) ((KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) : M)

Tactic:
congr_arg (fun D : Derivation R S M => D x) hf

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.Basic
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 : S
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) ((KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) : M)
    ((f' : (a : Ω[S⁄R]) → M) ((KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) x : Ω[S⁄R]) : M)

Tactic:
exact congr_arg (fun D : Derivation R S M => D x) hf

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
h₁ h₂ : Eq.{u_1 + 1} (α := M) 0 0
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : Ω[S⁄R]) → M) 0 : M) ((f' : (a : Ω[S⁄R]) → M) 0 : M)

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Kaehler.Basic
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]
h :
  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)
⊢ ∀
    (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)

Tactic:
_
-- Module: Mathlib.RingTheory.Kaehler.Basic
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 :
  Membership.mem (γ := Submodule S Ω[S⁄R])
    (Submodule.span S (Set.range (ι := S) (⇑(KaehlerDifferential.D R S) : (a : S) → Ω[S⁄R]))) x
h :
  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)
⊢ ∀
    (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)

Tactic:
_
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
h₃ 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)

Tactic:
rw [map_add, map_add, hx, hy]

Premises used: map_add
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
a : S
x : Ω[S⁄R]
h :
  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)
⊢ ∀
    (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:
_
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
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
e : 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:
simp [e]
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Eq (α := Ω[S⁄R] →ₗ[S] Ω[S⁄R]) (liftKaehlerDifferential (KaehlerDifferential.D R S)) LinearMap.id

Tactic:
Derivation.liftKaehlerDifferential_unique _ _
    (KaehlerDifferential.D R S).liftKaehlerDifferential_comp

Premises used: Derivation.liftKaehlerDifferential_comp, Derivation.liftKaehlerDifferential_unique, KaehlerDifferential.D
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : ↥(ideal R S)
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))
⊢ 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))

Tactic:
rw [← Derivation.liftKaehlerDifferential_apply, Derivation.liftKaehlerDifferential_D]

Premises used: Derivation.liftKaehlerDifferential_D, Derivation.liftKaehlerDifferential_apply
-- Module: Mathlib.RingTheory.Kaehler.Basic
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])
    ((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:
rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : Ω[S⁄R]
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))
⊢ ∃ (a : S ⊗[R] S), (Derivation.tensorProductTo (D R S) : (a : S ⊗[R] S) → Ω[S⁄R]) a = x

Tactic:
obtain ⟨x, rfl⟩ := (KaehlerDifferential.ideal R S).toCotangent_surjective x

Premises used: KaehlerDifferential.ideal, Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
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:
⟨x, KaehlerDifferential.D_tensorProductTo x⟩

Premises used: KaehlerDifferential.D_tensorProductTo, Exists.intro, Subtype.val
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
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:
exact ⟨x, KaehlerDifferential.D_tensorProductTo x⟩
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
rw : (AlgHom.id R S : (a : S) → S) x = x
⊢ ((↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S) : (a : S ⊗[R] S) → S)
      ((TensorProduct.includeLeft : (a : S) → S ⊗[R] S) x : S ⊗[R] S) =
    x

Tactic:
rw [AlgHom.coe_toRingHom, ← AlgHom.comp_apply, TensorProduct.lmul'_comp_includeLeft]

Premises used: AlgHom.coe_toRingHom, AlgHom.comp_apply, Algebra.TensorProduct.lmul'_comp_includeLeft
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
⊢ (AlgHom.id R S : (a : S) → S) x = x

Tactic:
rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
⊢ 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
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
refine : HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (ideal 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

Tactic:
refine (Ideal.quotCotangent _).trans ?_

Premises used: Ideal.quotCotangent, RingEquiv.trans
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
refine : ideal R S = RingHom.ker (F := S ⊗[R] S →+* S) (↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S)
⊢ HasQuotient.Quotient (S ⊗[R] S) (B := Ideal (S ⊗[R] S)) (ideal R S) ≃+* S

Tactic:
refine (Ideal.quotEquivOfEq ?_).trans (RingHom.quotientKerEquivOfRightInverse this)

Premises used: Ideal.quotEquivOfEq, RingHom.quotientKerEquivOfRightInverse, RingEquiv.trans
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
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
⊢ ideal R S = RingHom.ker (F := S ⊗[R] S →+* S) (↑(TensorProduct.lmul' R) : S ⊗[R] S →+* S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Kaehler.Basic
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)
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:
rfl
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [AlgHom.ext_iff, AlgHom.ext_iff]

Premises used: AlgHom.ext_iff
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.Kaehler.Basic
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
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)
⊢ 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:
generalize f x = y

Premises used: DFunLike.coe