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
x : S →₀ S
this :
  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))
rw :
  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])) ⋯))
        ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x) :
      Ω[S⁄R])
    ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x : Ω[S⁄R])
⊢ 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])

Tactic:
rw [this]
-- 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) : (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))
⊢ 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])) ⋯))
        ((Submodule.mkQ (kerTotal R S) : (a : S →₀ S) → (S →₀ S) ⧸ kerTotal R S) x) :
      Ω[S⁄R])
    ((linearCombination S (⇑(D R S) : (a : S) → Ω[S⁄R]) : (a : S →₀ S) → Ω[S⁄R]) x : Ω[S⁄R])

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
⊢ Eq (α := Derivation R S (HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)))
    (((LinearMap.compDer (Derivation.liftKaehlerDifferential (derivationQuotKerTotal R S)) :
            Derivation R S Ω[S⁄R] →ₗ[S]
              Derivation R S (HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))) :
          (a : Derivation R S Ω[S⁄R]) → Derivation R S ((S →₀ S) ⧸ kerTotal R S))
        (D R S) :
      Derivation R S (HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)))
    (derivationQuotKerTotal R S :
      Derivation R S (HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)))

Tactic:
(KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential_comp

Premises used: KaehlerDifferential.derivationQuotKerTotal, Derivation.liftKaehlerDifferential_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
⊢ Eq (α := Derivation R S (HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)))
    (((LinearMap.compDer (↑(LinearEquiv.symm (quotKerTotalEquiv R S)) : Ω[S⁄R] →ₗ[S] (S →₀ S) ⧸ kerTotal R S) :
            Derivation R S Ω[S⁄R] →ₗ[S]
              Derivation R S (HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S))) :
          (a : Derivation R S Ω[S⁄R]) → Derivation R S ((S →₀ S) ⧸ kerTotal R S))
        (D R S) :
      Derivation R S (HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)))
    (derivationQuotKerTotal R S :
      Derivation R S (HasQuotient.Quotient (S →₀ S) (B := Submodule S (S →₀ S)) (kerTotal R S)))

Tactic:
convert! (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential_comp

Premises used: KaehlerDifferential.derivationQuotKerTotal, Derivation.liftKaehlerDifferential_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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
        (Set.image.{u_2, u_3} (α := A →₀ A)
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
            (a : A →₀ A) → B →₀ B)
          (((Set.range fun (x : A × A) ↦ HAdd.hAdd (α := A →₀ A) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∪
              Set.range fun (x : A × A) ↦
                HAdd.hAdd (α := A →₀ A) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∪
            Set.range fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
    (Submodule.span A
      (((Set.range fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∪
          Set.range fun (x : B × B) ↦
            HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∪
        Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
⊢ Eq (α := Submodule A (B →₀ B))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (kerTotal R A) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
    (Submodule.restrictScalars A (kerTotal S B))

Tactic:
rw [KaehlerDifferential.kerTotal, Submodule.map_span, KaehlerDifferential.kerTotal,
    Submodule.restrictScalars_span _ _ h]

Premises used: Submodule.map_span, KaehlerDifferential.kerTotal, Submodule.restrictScalars_span
-- 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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h₁ :
  Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
        (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
    (Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
⊢ Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
        (Set.range fun (x : A × A) ↦
          HAdd.hAdd (α := B →₀ B) (β := B →₀ B) (single ((algebraMap A B : (a : A) → B) x.1) 1 : B →₀ B)
              (single ((algebraMap A B : (a : A) → B) x.2) 1 : B →₀ B) -
            single
              (HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) x.1 : B)
                ((algebraMap A B : (a : A) → B) x.2 : B))
              1) ⊔
      (Submodule.span A
          (Set.range fun (x : A × A) ↦
            HAdd.hAdd (α := B →₀ B) (β := B →₀ B)
                (single ((algebraMap A B : (a : A) → B) x.2) ((algebraMap A B : (a : A) → B) x.1) : B →₀ B)
                (single ((algebraMap A B : (a : A) → B) x.1) ((algebraMap A B : (a : A) → B) x.2) : B →₀ B) -
              single
                (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x.1 : B)
                  ((algebraMap A B : (a : A) → B) x.2 : B))
                1) ⊔
        (Submodule.span A
            (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1) ⊔
          Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))))
    (Submodule.span A
        (Set.range.{u_3, u_2 + 1} (ι := A × A)
          ((fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.1 1) (single x.2 1) - single (x.1 + x.2) 1) ∘
            Prod.map (⇑(algebraMap A B) : (a : A) → B) (⇑(algebraMap A B) : (a : A) → B))) ⊔
      (Submodule.span A
          (Set.range.{u_3, u_2 + 1} (ι := A × A)
            ((fun (x : B × B) ↦ HAdd.hAdd (α := B →₀ B) (single x.2 x.1) (single x.1 x.2) - single (x.1 * x.2) 1) ∘
              Prod.map (⇑(algebraMap A B) : (a : A) → B) (⇑(algebraMap A B) : (a : A) → B))) ⊔
        Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)))

Tactic:
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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h₁ :
  LE.le.{u_3} (α := Submodule A (B →₀ B))
    (Submodule.span A
      (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1))
    (Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
⊢ Eq.{u_3 + 1} (α := Submodule A (B →₀ B))
    (Submodule.span A
        (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1) ⊔
      Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))
    (Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))

Tactic:
rw [sup_eq_right]

Premises used: sup_eq_right
-- 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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h₁ :
  Subset.{u_3} (α := Set (B →₀ B))
    (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1)
    (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)
⊢ LE.le.{u_3} (α := Submodule A (B →₀ B))
    (Submodule.span A
      (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1))
    (Submodule.span A (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1))

Tactic:
apply Submodule.span_mono

Premises used: Submodule.span_mono
-- 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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h₁ :
  Subset.{u_3} (α := Set (B →₀ B))
    (Set.range fun (x : R) ↦ single ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) x : S)) 1)
    (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)
⊢ Subset.{u_3} (α := Set (B →₀ B))
    (Set.range fun (x : R) ↦ single ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) x : A)) 1)
    (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)

Tactic:
simp_rw [← IsScalarTower.algebraMap_apply R A B, IsScalarTower.algebraMap_apply R S B]

Premises used: IsScalarTower.algebraMap_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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Subset.{u_3} (α := Set (B →₀ B))
    (Set.range fun (x : R) ↦ single ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) x : S)) 1)
    (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)

Tactic:
Set.range_comp_subset_range (algebraMap R S)
    fun x => Finsupp.single (algebraMap S B x) (1 : B)

Premises used: Set.range_comp_subset_range, Algebra.algebraMap, OfNat.ofNat, DFunLike.coe, Finsupp.single
-- 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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Subset.{u_3} (α := Set (B →₀ B))
    (Set.range fun (x : R) ↦ single ((algebraMap S B : (a : S) → B) ((algebraMap R S : (a : R) → S) x : S)) 1)
    (Set.range fun (x : S) ↦ single ((algebraMap S B : (a : S) → B) x) 1)

Tactic:
exact Set.range_comp_subset_range (algebraMap R S)
    fun x => Finsupp.single (algebraMap S B x) (1 : B)

Premises used: Set.range_comp_subset_range, Algebra.algebraMap, OfNat.ofNat, DFunLike.coe, Finsupp.single
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq (α := Submodule A (B →₀ B))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (kerTotal R A) ⊔
      Submodule.span A
        (Set.range.{u_3, u + 1} (ι := R)
          (Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
              (a : A →₀ A) → B →₀ B)
            fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (kerTotal R A) ⊔
      Submodule.span A (Set.range fun (x : R) ↦ single ((algebraMap R B : (a : R) → B) x) 1))
⊢ Eq (α := Submodule A (B →₀ B))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
      (kerTotal R A ⊔ Submodule.span A (Set.range fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
    (Submodule.restrictScalars A (kerTotal R B))

Tactic:
rw [Submodule.map_sup, ← kerTotal_map R R A B h, Submodule.map_span, ← Set.range_comp]

Premises used: Set.range_comp, Submodule.map_sup, KaehlerDifferential.kerTotal_map, Submodule.map_span
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
e_a :
  Eq (α := R → B →₀ B)
    (Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
      (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
        (a : A →₀ A) → B →₀ B)
      fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)
    fun (x : R) ↦ single ((algebraMap R B : (a : R) → B) x) 1
⊢ Eq (α := Submodule A (B →₀ B))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (kerTotal R A) ⊔
      Submodule.span A
        (Set.range.{u_3, u + 1} (ι := R)
          (Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
              (a : A →₀ A) → B →₀ B)
            fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)))
    (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (kerTotal R A) ⊔
      Submodule.span A (Set.range fun (x : R) ↦ single ((algebraMap R B : (a : R) → B) x) 1))

Tactic:
congr
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
e_a :
  ∀ (x : R) (a : B),
    Eq (α := B)
      ((Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
              (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
                (a : A →₀ A) → B →₀ B)
              (fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1) x :
            (a : B) → B)
          a :
        B)
      (((single ((algebraMap R B : (a : R) → B) x) 1 : B →₀ B) : (a : B) → B) a : B)
⊢ Eq (α := R → B →₀ B)
    (Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
      (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
        (a : A →₀ A) → B →₀ B)
      fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1)
    fun (x : R) ↦ single ((algebraMap R B : (a : R) → B) x) 1

Tactic:
ext
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
x : R
a : B
⊢ Eq (α := B)
    ((Function.comp.{u + 1, u_2 + 1, u_3 + 1} (β := A →₀ A)
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B)) :
              (a : A →₀ A) → B →₀ B)
            (fun (x : R) ↦ single ((algebraMap R A : (a : R) → A) x) 1) x :
          (a : B) → B)
        a :
      B)
    (((single ((algebraMap R B : (a : R) → B) x) 1 : B →₀ B) : (a : B) → B) a : B)

Tactic:
simp [IsScalarTower.algebraMap_eq R A B]

Premises used: IsScalarTower.algebraMap_eq
-- 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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
⊢ Eq (α := Derivation.{u, u_2, u_3} R A Ω[B⁄S])
    (((LinearMap.compDer (map R S A B) : Derivation R A Ω[A⁄R] →ₗ[A] Derivation.{u, u_2, u_3} R A Ω[B⁄S]) :
          (a : Derivation R A Ω[A⁄R]) → Derivation R A Ω[B⁄S])
        (D R A) :
      Derivation.{u, u_2, u_3} R A Ω[B⁄S])
    (Derivation.compAlgebraMap A (Derivation.restrictScalars R (D S B)) : Derivation.{u, u_2, u_3} R A Ω[B⁄S])

Tactic:
Derivation.liftKaehlerDifferential_comp _

Premises used: Derivation.liftKaehlerDifferential_comp, KaehlerDifferential.map
-- 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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
x : A
⊢ Eq.{u_3 + 1} (α := Ω[B⁄S])
    (((map R S A B : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S])
        ((D R A : (a : A) → Ω[A⁄R]) x) :
      Ω[B⁄S])
    ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) x) : Ω[B⁄S])

Tactic:
Derivation.congr_fun (KaehlerDifferential.map_compDer R S A B) x

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Quotient.map₂, List.foldl, KaehlerDifferential.map_compDer, Derivation.congr_fun, FreeAddMonoid.sumAux
-- 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 : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
rw :
  Eq (α := Submodule A Ω[A⁄R])
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B))))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (Submodule.restrictScalars A (kerTotal S B))))
⊢ Eq (α := Submodule A Ω[A⁄R]) (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (Submodule.restrictScalars A (kerTotal S B))))

Tactic:
rw [← Submodule.map_comap_eq_of_surjective (linearCombination_surjective R A) (LinearMap.ker _)]

Premises used: LinearMap.ker, Submodule.map_comap_eq_of_surjective, 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
A : Type u_2
B : Type u_3
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra A B
inst_7 : Algebra S B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : SMulCommClass S A B
e_p :
  Eq (α := Submodule A (A →₀ A))
    (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B)))
    (Submodule.comap (M₂ := B →₀ B)
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
      (Submodule.restrictScalars A (kerTotal S B)))
⊢ Eq (α := Submodule A Ω[A⁄R])
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (Submodule.comap (M₂ := Ω[A⁄R]) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
        (LinearMap.ker (M₂ := Ω[B⁄S]) (map R S A B))))
    (Submodule.map (M := A →₀ A) (linearCombination A (⇑(D R A) : (a : A) → Ω[A⁄R]))
      (Submodule.comap (M₂ := B →₀ B)
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A (⇑(algebraMap A B) : (a : A) → B))
        (Submodule.restrictScalars A (kerTotal S B))))

Tactic:
congr 1