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
x : R
y : S
⊢ Membership.mem (γ := Submodule S (S →₀ S)) (kerTotal R S)
    (HSMul.hSMul (β := S →₀ S) y (single ((algebraMap R S : (a : R) → S) x) 1 : S →₀ S))

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inr <| ⟨_, 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
rw :
  Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (x𝖣(algebraMap R S : (a : R) → S) 1 : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (0 : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
rw₁ rw₂ : Eq.{v + 1} (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) 0 0
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (x𝖣1 : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (0 : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
rw [← (algebraMap R S).map_one, KaehlerDifferential.kerTotal_mkQ_single_algebraMap]

Premises used: Algebra.algebraMap, RingHom.map_one, KaehlerDifferential.kerTotal_mkQ_single_algebraMap
-- 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
a b : S
simp_rw :
  HAdd.hAdd (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (β :=
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
          (HSMul.hSMul (β := S →₀ S) (1 * a) (single b 1)) :
        HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
          (HSMul.hSMul (β := S →₀ S) (1 * b) (single a 1)) :
        HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) =
    HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) a
        (({ toFun := fun (x : S) ↦ 1𝖣x, map_add' := ⋯, map_smul' := ⋯ :
                S →ₗ[R] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S) } :
              (a : S) → (S →₀ S) ⧸ kerTotal R S)
            b :
          HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) +
      HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
        (({ toFun := fun (x : S) ↦ 1𝖣x, map_add' := ⋯, map_smul' := ⋯ :
                S →ₗ[R] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S) } :
              (a : S) → (S →₀ S) ⧸ kerTotal R S)
            a :
          HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
⊢ HAdd.hAdd (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (β :=
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((1 * a)𝖣b : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((1 * b)𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) =
    HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) a
        (({ toFun := fun (x : S) ↦ 1𝖣x, map_add' := ⋯, map_smul' := ⋯ :
                S →ₗ[R] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S) } :
              (a : S) → (S →₀ S) ⧸ kerTotal R S)
            b :
          HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) +
      HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
        (({ toFun := fun (x : S) ↦ 1𝖣x, map_add' := ⋯, map_smul' := ⋯ :
                S →ₗ[R] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S) } :
              (a : S) → (S →₀ S) ⧸ kerTotal R S)
            a :
          HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
simp_rw [← Finsupp.smul_single_one _ (1 * _ : S)]

Premises used: HMul.hMul, OfNat.ofNat, Finsupp.smul_single_one
-- 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
a b : S
⊢ HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (1 * a)
        (Submodule.Quotient.mk (single b 1)) +
      HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (1 * b)
        (Submodule.Quotient.mk (single a 1)) =
    HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) a
        (Submodule.Quotient.mk (single b 1)) +
      HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
        (Submodule.Quotient.mk (single a 1))

Tactic:
simp
-- 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
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((derivationQuotKerTotal R S : (a : S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (1𝖣x : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
rfl

Premises used: Submodule.Quotient.mk, 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
h :
  ∀ (a b : S),
    Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
              linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
            (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
          (single a b) :
        HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (b𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
⊢ Eq (α := (S →₀ S) →ₗ[S] HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
      linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))
    (Submodule.mkQ (kerTotal R S))

Tactic:
apply Finsupp.lhom_ext

Premises used: Finsupp.lhom_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
a b : S
rw :
  HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
    (1𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
| b𝖣a

Tactic:
rw [← Finsupp.smul_single_one a b, map_smul]

Premises used: Finsupp.smul_single_one, map_smul
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a b : S
h :
  (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
          linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
        (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
      (single a b) =
    HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
      (1𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
            linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
          (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
        (single a b) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    (b𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
conv_rhs => rw [← Finsupp.smul_single_one a b, map_smul]

Premises used: Finsupp.smul_single_one, map_smul
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a b : S
⊢ (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
          linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
        (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
      (single a b) =
    HSMul.hSMul (β := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) b
      (1𝖣a : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
simp [KaehlerDifferential.derivationQuotKerTotal_apply]

Premises used: KaehlerDifferential.derivationQuotKerTotal_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
a :
  LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (kerTotal R S)
a₁ :
  LE.le (α := Submodule S (S →₀ S)) (kerTotal R S)
    (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
⊢ Eq (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (kerTotal R S)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw :
  (LinearMap.ker (R₂ := S) (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (τ₁₂ :=
      RingHom.id S) (Submodule.mkQ (kerTotal R S)) :
    Submodule S (S →₀ S))
| kerTotal R S

Tactic:
rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]

Premises used: Submodule.ker_mkQ, KaehlerDifferential.kerTotal
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a :
  LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (LinearMap.ker (R₂ := S) (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (τ₁₂ :=
      RingHom.id S) (Submodule.mkQ (kerTotal R S)))
⊢ LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (kerTotal R S)

Tactic:
conv_rhs => rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]

Premises used: Submodule.ker_mkQ, KaehlerDifferential.kerTotal
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a :
  LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (LinearMap.ker (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
        linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
⊢ LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (LinearMap.ker (R₂ := S) (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)) (τ₁₂ :=
      RingHom.id S) (Submodule.mkQ (kerTotal R S)))

Tactic:
rw [← KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination]

Premises used: KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (LinearMap.ker (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
        linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))

Tactic:
LinearMap.ker_le_ker_comp _ _

Premises used: Set.Mem, LinearMap.ker_le_ker_comp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ LE.le (α := Submodule S (S →₀ S)) (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))
    (LinearMap.ker (M₂ := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
        linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))

Tactic:
exact LinearMap.ker_le_ker_comp _ _

Premises used: LinearMap.ker_le_ker_comp
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a :
  (((Set.range fun (x : S × S) ↦ HAdd.hAdd (α := S →₀ S) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∪
        Set.range fun (x : S × S) ↦ HAdd.hAdd (α := S →₀ S) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∪
      Set.range fun (x : R) ↦ single ((algebraMap R S : (a : R) → S) x) 1) ⊆
    (↑(LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) : Set (S →₀ S))
⊢ LE.le (α := Submodule S (S →₀ S)) (kerTotal R S)
    (LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])))

Tactic:
rw [KaehlerDifferential.kerTotal, Submodule.span_le]

Premises used: Submodule.span_le, KaehlerDifferential.kerTotal
-- 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 y : S
⊢ (fun (x : S × S) ↦ HAdd.hAdd (α := S →₀ S) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) (x, y) ∈
    (↑(LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) : Set (S →₀ S))

Tactic:
simp [LinearMap.mem_ker]

Premises used: LinearMap.mem_ker
-- 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 y : S
⊢ (fun (x : S × S) ↦ HAdd.hAdd (α := S →₀ S) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) (x, y) ∈
    (↑(LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) : Set (S →₀ S))

Tactic:
simp [LinearMap.mem_ker]

Premises used: LinearMap.mem_ker
-- 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 : R
⊢ (fun (x : R) ↦ (single ((algebraMap R S : (a : R) → S) x) 1 : S →₀ S)) x ∈
    (↑(LinearMap.ker (M₂ := Ω[S⁄R]) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) : Set (S →₀ S))

Tactic:
simp [LinearMap.mem_ker]

Premises used: LinearMap.mem_ker
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Eq (α := Submodule S Ω[S⁄R]) (LinearMap.range (M := S →₀ S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤
rw₁ : Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))) ⊤
rw₂ rw₃ : Eq.{v + 1} (α := Submodule S Ω[S⁄R]) ⊤ ⊤
⊢ Function.Surjective (α := S →₀ S) (β := Ω[S⁄R])
    (⇑(linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) : (a : S →₀ S) → Ω[S⁄R])

Tactic:
rw [← LinearMap.range_eq_top, range_linearCombination, span_range_derivation]

Premises used: KaehlerDifferential.span_range_derivation, LinearMap.range_eq_top, Finsupp.range_linearCombination
-- 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 : HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)
obtain :
  ∀ (x : S →₀ S),
    Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
          (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
            (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
              (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
            ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x)) :
        HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
        HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
⊢ (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
      (AddHom.toFun
        (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
          (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
        x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x

Premises used: Submodule.mkQ_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
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 →₀ S
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
        (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
          (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
            (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
          ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x)) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
LinearMap.congr_fun
          (KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination R S :) x

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, Finsupp.sum, LinearMap.congr_fun, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Finset.sum
-- 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 →₀ S
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
        (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
          (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
            (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
          ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x)) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
exact
        LinearMap.congr_fun
          (KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination R S :) x

Premises used: LinearMap.congr_fun, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination
-- 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⁄R]
obtain :
  ∀ (x : S →₀ S),
    Eq (α := Ω[S⁄R])
      (AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
          (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
            (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
          ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
            ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x)) :
        Ω[S⁄R])
      ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x : Ω[S⁄R])
⊢ AddHom.toFun (M := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
      (LinearMap.toAddHom (S := S) (σ := RingHom.id S)
        (Submodule.liftQ (kerTotal R S) (linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R])) ⋯))
      ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S) x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := KaehlerDifferential.linearCombination_surjective R S x

Premises used: rfl, KaehlerDifferential.linearCombination_surjective
-- 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 →₀ S
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
            linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
          (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
        x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
have := LinearMap.congr_fun
        (KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination R S) 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 →₀ S
this :
  Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) ∘ₗ
            linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) :
          (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S)
        x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
⊢ Eq (α := HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S) : (a : Ω[S⁄R]) → (S →₀ S) ⧸ kerTotal R S)
        ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x) :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))
    ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x :
      HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))

Tactic:
rw [LinearMap.comp_apply] at this

Premises used: LinearMap.comp_apply