awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z m : A
⊢ (IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
          ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
        (a : B) → S ⊗[R] Ω[A⁄R])
      ((algebraMap A B : (a : A) → B) (z * m)) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) z
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            ((algebraMap A B : (a : A) → B) m) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) m
        ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) ⋯
                ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R])) :
              (a : B) → S ⊗[R] Ω[A⁄R])
            ((algebraMap A B : (a : A) → B) z) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
have tmul : ((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R]) : (a : A) → S ⊗[R] Ω[A⁄R])
    (z * m) =
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) z
      (((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R]) :
            (a : A) → S ⊗[R] Ω[A⁄R])
          m :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) +
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) m
      (((mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 ∘ₗ (↑(D R A) : A →ₗ[R] Ω[A⁄R]) :
            (a : A) → S ⊗[R] Ω[A⁄R])
          z :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
Tactic: rw [← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq,
          ← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq,
          ← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : Algebra.IsPushout R S A B
x : S
x_1 y : A
⊢ x •
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x_1
        (1 ⊗ₜ[R] (D R A : (a : A) → Ω[A⁄R]) y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    x ⊗ₜ[R] HSMul.hSMul (β := Ω[A⁄R]) x_1 ((D R A : (a : A) → Ω[A⁄R]) y : Ω[A⁄R])
have H : HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x_1
    (x ⊗ₜ[R] (D R A : (a : A) → Ω[A⁄R]) y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
  x ⊗ₜ[R] HSMul.hSMul (β := Ω[A⁄R]) x_1 ((D R A : (a : A) → Ω[A⁄R]) y : Ω[A⁄R])
Tactic: rw [smul_comm, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x : Ω[B⁄S]
⊢ AddHom.toFun (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      (LinearMap.toAddHom
        (LinearMap.liftBaseChange S
          ((↑R :
              {S M : Type u_3} →
                {M₂ : Type u_4} →
                  [inst : Semiring R] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module R M] →
                            [inst_15 : Module R M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (map R S A B))))
      (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
              (derivationTensorProduct R S A B) :
            Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
          (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
        x) =
    x
have obtain : ∀ (x : B ⊗[S] B),
  Eq (α := Ω[B⁄S])
    (AddHom.toFun (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      (LinearMap.toAddHom
        (LinearMap.liftBaseChange S
          ((↑R :
              {S M : Type u_3} →
                {M₂ : Type u_4} →
                  [inst : Semiring R] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module R M] →
                            [inst_15 : Module R M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (map R S A B))))
      (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
              (derivationTensorProduct R S A B) :
            Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
          (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
        ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) x)))
    ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) x)
Tactic: obtain ⟨x, rfl⟩ := tensorProductTo_surjective _ _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x y : B
⊢ Eq.{u_4 + 1} (α := Ω[B⁄S])
    ((LinearMap.liftBaseChange S
            ((↑R :
                {S M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (map R S A B)) :
          (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
        (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                (derivationTensorProduct R S A B) :
              Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
            (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
          ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) (x ⊗ₜ[S] y))) :
      Ω[B⁄S])
    ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) (x ⊗ₜ[S] y) : Ω[B⁄S])
have tmul : HSMul.hSMul (β := Ω[B⁄S]) x
    ((LinearMap.liftBaseChange S
            ((↑R :
                {S M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (map R S A B)) :
          (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
        ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) y) :
      Ω[B⁄S]) =
  HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) y : Ω[B⁄S])
Tactic: simp only [Derivation.tensorProductTo_tmul, LinearMap.map_smul,
        Derivation.liftKaehlerDifferential_comp_D, map_liftBaseChange_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x y : B
⊢ HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
              ((↑R :
                  {S M : Type u_3} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (map R S A B)) :
            (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
          ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) y) :
        Ω[B⁄S]) =
    HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) y : Ω[B⁄S])
have tmul : HSMul.hSMul (β := Ω[B⁄S]) x
    ((LinearMap.liftBaseChange S
          ((↑R :
              {S M : Type u_3} →
                {M₂ : Type u_4} →
                  [inst : Semiring R] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module R M] →
                            [inst_15 : Module R M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (map R S A B)) :
        (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
      ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) 0)) =
  HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) 0 : Ω[B⁄S])
Tactic: induction y using h.1.inductionOn
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ IsBaseChange (M := Ω[A⁄R]) (N := Ω[B⁄S]) S
    ((↑R :
        {S M : Type u_3} →
          {M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_11 : Semiring S] →
                [inst_12 : AddCommMonoid M] →
                  [inst_13 : AddCommMonoid M₂] →
                    [inst_14 : Module R M] →
                      [inst_15 : Module R M₂] →
                        [inst_16 : Module S M] →
                          [inst_17 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (map R S A B))
have h₁ : Eq (α := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) Ω[A⁄R] Ω[B⁄S])
  ((↑R :
      {S M : Type u_3} →
        {M₂ : Type u_4} →
          [inst : Semiring R] →
            [inst_11 : Semiring S] →
              [inst_12 : AddCommMonoid M] →
                [inst_13 : AddCommMonoid M₂] →
                  [inst_14 : Module R M] →
                    [inst_15 : Module R M₂] →
                      [inst_16 : Module S M] →
                        [inst_17 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (map R S A B))
  ((↑R :
        {S : Type u_2} →
          {M : Type (max u_2 u_3)} →
            {M₂ : Type u_4} →
              [inst : Semiring R] →
                [inst_11 : Semiring S] →
                  [inst_12 : AddCommMonoid M] →
                    [inst_13 : AddCommMonoid M₂] →
                      [inst_14 : Module R M] →
                        [inst_15 : Module R M₂] →
                          [inst_16 : Module S M] →
                            [inst_17 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (↑(tensorKaehlerEquivBase R S A B) : S ⊗[R] Ω[A⁄R] →ₗ[S] Ω[B⁄S]) ∘ₗ
    (mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1)
Tactic: convert!
    (TensorProduct.isBaseChange R Ω[A⁄R] S).comp
      (IsBaseChange.ofEquiv (tensorKaehlerEquivBase R S A B))
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ B ⊗[A] Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]
have this : Algebra.IsPushout R A S B
Tactic: have : Algebra.IsPushout R A S B := .symm inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
⊢ B ⊗[A] Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]
have refine : ∀ (m : B) (x : B ⊗[A] Ω[A⁄R]),
  (↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun (m • x) =
    HSMul.hSMul (α := B) ((RingHom.id B : (a : B) → B) m : B) ((↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun x)
Tactic: refine { __ := e₂, map_smul' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
m : B
x : B ⊗[A] Ω[A⁄R]
⊢ (↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun (m • x) =
    HSMul.hSMul (α := B) ((RingHom.id B : (a : B) → B) m : B) ((↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun x)
have obtain : ∀ (m : A ⊗[R] S),
  (↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) x) =
    HSMul.hSMul (α := B)
      ((RingHom.id B : (a : B) → B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) : B)
      ((↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun x)
Tactic: obtain ⟨m, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
x : B ⊗[A] Ω[A⁄R]
m : A ⊗[R] S
⊢ (↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) x) =
    HSMul.hSMul (α := B)
      ((RingHom.id B : (a : B) → B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) : B)
      ((↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun x)
have dsimp : (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
    (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) x) =
  HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B)
    ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x : Ω[B⁄S])
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
x : B
y : Ω[A⁄R]
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) (x ⊗ₜ[A] y)) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) (x ⊗ₜ[A] y) : Ω[B⁄S])
have tmul : ∀ (x : A ⊗[R] S),
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x ⊗ₜ[A] y : B ⊗[A] Ω[A⁄R])) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x ⊗ₜ[A] y) : Ω[B⁄S])
Tactic: obtain ⟨x, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y : Ω[A⁄R]
x : A
z : S
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x ⊗ₜ[R] z) ⊗ₜ[A] y : B ⊗[A] Ω[A⁄R])) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
          ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x ⊗ₜ[R] z) ⊗ₜ[A] y) :
        Ω[B⁄S])
have tmul : b •
    z •
      a •
        HSMul.hSMul (β := Ω[B⁄S]) x
          (((map R S A B : LinearMap.{u_3, u_3, u_3, u_4} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S]) y :
            Ω[B⁄S]) =
  HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap S B : (a : S) → B) b : B) •
    z •
      HSMul.hSMul (β := Ω[B⁄S]) x
        (((map R S A B : LinearMap.{u_3, u_3, u_3, u_4} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S]) y :
          Ω[B⁄S])
Tactic: suffices b • z • a • x • KaehlerDifferential.map R S A B y =
      (algebraMap A B a * algebraMap S B b) • z • x • KaehlerDifferential.map R S A B y by
    simpa [e₂, e₁, smul_tmul', Algebra.IsPushout.equiv_tmul, ← mul_smul,
      Algebra.IsPushout.equiv_symm_algebraMap_left, Algebra.IsPushout.equiv_symm_algebraMap_right]