awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
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])
⊢ (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])

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]
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
tmul :
  HSMul.hSMul (β := Ω[B⁄S])
      (HMul.hMul (α := B) ((algebraMap S B : (a : S) → B) b : B)
        (HMul.hMul (α := B) ((algebraMap S B : (a : S) → B) z : B)
          (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) x : B))))
      (((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]) =
    HSMul.hSMul (β := Ω[B⁄S])
      (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap S B : (a : S) → B) b : B) *
        HMul.hMul (α := B) (β := B) ((algebraMap S B : (a : S) → B) z : B) ((algebraMap A B : (a : A) → B) x : B))
      (((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])
⊢ 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:
simp only [← mul_smul, ← @algebraMap_smul S _ B, ← @algebraMap_smul A _ B]

Premises used: algebraMap_smul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
⊢ HSMul.hSMul (β := Ω[B⁄S])
      (HMul.hMul (α := B) ((algebraMap S B : (a : S) → B) b : B)
        (HMul.hMul (α := B) ((algebraMap S B : (a : S) → B) z : B)
          (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) x : B))))
      (((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]) =
    HSMul.hSMul (β := Ω[B⁄S])
      (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap S B : (a : S) → B) b : B) *
        HMul.hMul (α := B) (β := B) ((algebraMap S B : (a : S) → B) z : B) ((algebraMap A B : (a : A) → B) x : B))
      (((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:
ring_nf
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
b : B
a : A
⊢ Algebra.IsPushout R A S B

Tactic:
have : Algebra.IsPushout R A S B := .symm inferInstance
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
b : B
a : A
this : Algebra.IsPushout R A S B
obtain :
  ∀ (b : A ⊗[R] S),
    (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) b ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) b : B)
        ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])
⊢ (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) (b ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    HSMul.hSMul (β := Ω[B⁄S]) b ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])

Tactic:
obtain ⟨b, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective b

Premises used: Algebra.IsPushout.equiv, AlgEquiv.surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
a : A
this : Algebra.IsPushout R A S B
⊢ (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
a : A
this : Algebra.IsPushout R A S B
x y : A ⊗[R] S
h :
  (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])
h_1 :
  (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) y ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) y : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])
⊢ (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x + y) ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x + y) : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])

Tactic:
simp only [map_add, *, add_tmul, add_smul]

Premises used: map_add, add_smul, TensorProduct.add_tmul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
a : A
this : Algebra.IsPushout R A S B
a' : A
s : S
trans :
  (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a' ⊗ₜ[R] s) ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    s • HSMul.hSMul (β := Ω[B⁄S]) a' ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])
trans₁ :
  s • HSMul.hSMul (β := Ω[B⁄S]) a' ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S]) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a' ⊗ₜ[R] s) : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])
⊢ (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a' ⊗ₜ[R] s) ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a' ⊗ₜ[R] s) : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])

Tactic:
trans s • a' • D S B (algebraMap A B a)

Premises used: Algebra.algebraMap, KaehlerDifferential.D, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
a : A
this : Algebra.IsPushout R A S B
a' : A
s : S
⊢ (tensorKaehlerEquiv R S A B : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a' ⊗ₜ[R] s) ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) =
    s • HSMul.hSMul (β := Ω[B⁄S]) a' ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])

Tactic:
simp [tensorKaehlerEquiv]

Premises used: KaehlerDifferential.tensorKaehlerEquiv
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
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
a : A
this : Algebra.IsPushout R A S B
a' : A
s : S
⊢ s • HSMul.hSMul (β := Ω[B⁄S]) a' ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S]) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a' ⊗ₜ[R] s) : B)
      ((D S B : (a : B) → Ω[B⁄S]) ((algebraMap A B : (a : A) → B) a : B) : Ω[B⁄S])

Tactic:
simp [Algebra.IsPushout.equiv_tmul, mul_smul, smul_comm]

Premises used: Algebra.IsPushout.equiv_tmul, SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
apply :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((tensorKaehlerEquiv R S A (S ⊗[R] A) : (a : S ⊗[R] A ⊗[A] Ω[A⁄R]) → Ω[S ⊗[R] A⁄S])
        ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) :
      Ω[S ⊗[R] A⁄S])
⊢ Eq (α := S ⊗[R] A ⊗[A] Ω[A⁄R])
    ((LinearEquiv.symm (tensorKaehlerEquiv R S A (S ⊗[R] A)) : (a : Ω[S ⊗[R] A⁄S]) → S ⊗[R] A ⊗[A] Ω[A⁄R])
        ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a)) :
      S ⊗[R] A ⊗[A] Ω[A⁄R])
    ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a : S ⊗[R] A ⊗[A] Ω[A⁄R])

Tactic:
apply (tensorKaehlerEquiv R S A _).symm_apply_eq.mpr ?_

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, KaehlerDifferential.tensorKaehlerEquiv
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
simp :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] 1)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
⊢ Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((tensorKaehlerEquiv R S A (S ⊗[R] A) : (a : S ⊗[R] A ⊗[A] Ω[A⁄R]) → Ω[S ⊗[R] A⁄S])
        ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) :
      Ω[S ⊗[R] A⁄S])

Tactic:
simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    tensorKaehlerEquiv_tmul_D]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, KaehlerDifferential.tensorKaehlerEquiv_tmul_D
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
⊢ Eq (α := S ⊗[R] A) (s ⊗ₜ[R] 1) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s)

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
rw :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])
rw₁ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) ((algebraMap S (S ⊗[R] A) : (a : S) → S ⊗[R] A) s : S ⊗[R] A)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₂ :
  (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (β := Ω[S ⊗[R] A⁄S]) s ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₃ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S ⊗[R] A) s (1 ⊗ₜ[R] a)) : Ω[S ⊗[R] A⁄S])
rw₄ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (HSMul.hSMul (β := S) s 1 ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₅ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((s * 1) ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
rw₆ rw₇ :
  Eq (α := Ω[S ⊗[R] A⁄S]) ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
    ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) : Ω[S ⊗[R] A⁄S])
⊢ (D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] a) =
    HSMul.hSMul (α := S ⊗[R] A) (β := Ω[S ⊗[R] A⁄S]) (s ⊗ₜ[R] 1)
      ((D S (S ⊗[R] A) : (a : S ⊗[R] A) → Ω[S ⊗[R] A⁄S]) ((algebraMap A (S ⊗[R] A) : (a : A) → S ⊗[R] A) a) :
        Ω[S ⊗[R] A⁄S])

Tactic:
rw [show s ⊗ₜ 1 = algebraMap S (S ⊗ A) s by simp, Algebra.TensorProduct.right_algebraMap_apply,
    algebraMap_smul, ← Derivation.map_smul, smul_tmul', smul_eq_mul, mul_one]

Premises used: Algebra.TensorProduct.right_algebraMap_apply, algebraMap_smul, TensorProduct.smul_tmul', Derivation.map_smul, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
apply :
  Eq (α := Ω[A ⊗[R] S⁄S]) ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) : Ω[A ⊗[R] S⁄S])
    ((tensorKaehlerEquiv R S A (A ⊗[R] S) : (a : A ⊗[R] S ⊗[A] Ω[A⁄R]) → Ω[A ⊗[R] S⁄S])
        ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) :
      Ω[A ⊗[R] S⁄S])
⊢ Eq (α := A ⊗[R] S ⊗[A] Ω[A⁄R])
    ((LinearEquiv.symm (tensorKaehlerEquiv R S A (A ⊗[R] S)) : (a : Ω[A ⊗[R] S⁄S]) → A ⊗[R] S ⊗[A] Ω[A⁄R])
        ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s)) :
      A ⊗[R] S ⊗[A] Ω[A⁄R])
    ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a : A ⊗[R] S ⊗[A] Ω[A⁄R])

Tactic:
apply (tensorKaehlerEquiv R S A _).symm_apply_eq.mpr ?_

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, KaehlerDifferential.tensorKaehlerEquiv
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
simp :
  (D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) =
    HSMul.hSMul (α := A ⊗[R] S) (β := Ω[A ⊗[R] S⁄S]) ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s : A ⊗[R] S)
      ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] 1) : Ω[A ⊗[R] S⁄S])
⊢ Eq (α := Ω[A ⊗[R] S⁄S]) ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) : Ω[A ⊗[R] S⁄S])
    ((tensorKaehlerEquiv R S A (A ⊗[R] S) : (a : A ⊗[R] S ⊗[A] Ω[A⁄R]) → Ω[A ⊗[R] S⁄S])
        ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s ⊗ₜ[A] (D R A : (a : A) → Ω[A⁄R]) a) :
      Ω[A ⊗[R] S⁄S])

Tactic:
simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    tensorKaehlerEquiv_tmul_D]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, KaehlerDifferential.tensorKaehlerEquiv_tmul_D
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
rw :
  Eq (α := Ω[A ⊗[R] S⁄S]) ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) : Ω[A ⊗[R] S⁄S])
    ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (HMul.hMul (α := A ⊗[R] S) (1 ⊗ₜ[R] s) (a ⊗ₜ[R] 1)) :
      Ω[A ⊗[R] S⁄S])
⊢ (D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) =
    HSMul.hSMul (α := A ⊗[R] S) (β := Ω[A ⊗[R] S⁄S]) ((algebraMap S (A ⊗[R] S) : (a : S) → A ⊗[R] S) s : A ⊗[R] S)
      ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] 1) : Ω[A ⊗[R] S⁄S])

Tactic:
rw [algebraMap_smul, ← Derivation.map_smul, Algebra.smul_def,
    Algebra.TensorProduct.right_algebraMap_apply]

Premises used: Algebra.TensorProduct.right_algebraMap_apply, algebraMap_smul, Derivation.map_smul, Algebra.smul_def
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : Algebra R A
s : S
a : A
⊢ Eq (α := Ω[A ⊗[R] S⁄S]) ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (a ⊗ₜ[R] s) : Ω[A ⊗[R] S⁄S])
    ((D S (A ⊗[R] S) : (a : A ⊗[R] S) → Ω[A ⊗[R] S⁄S]) (HMul.hMul (α := A ⊗[R] S) (1 ⊗ₜ[R] s) (a ⊗ₜ[R] 1)) :
      Ω[A ⊗[R] S⁄S])

Tactic:
simp only [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_one]

Premises used: Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
⊢ KrullDimLE n R ↔ ringKrullDim R ≤ (↑n : WithBot ℕ∞)

Tactic:
Order.krullDimLE_iff n (PrimeSpectrum R)

Premises used: PrimeSpectrum, ringKrullDim, Order.krullDimLE_iff
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Subsingleton R
⊢ ringKrullDim R = ⊥

Tactic:
krullDim_eq_bot

Premises used: Order.krullDim_eq_bot, ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ 0 ≤ ringKrullDim R

Tactic:
krullDim_nonneg

Premises used: ringKrullDim, Order.krullDim_nonneg
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x x_1 : PrimeSpectrum S
h :
  Eq (α := PrimeSpectrum R) { asIdeal := Ideal.comap f x.asIdeal, isPrime := ⋯ }
    { asIdeal := Ideal.comap f x_1.asIdeal, isPrime := ⋯ }
⊢ Eq (α := Ideal R) (Ideal.comap f x.asIdeal) (Ideal.comap f x_1.asIdeal)

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.KrullDimension.Basic
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
⊢ ringKrullDim.{u_3} (R ⧸ I) ≤ ringKrullDim R

Tactic:
ringKrullDim_le_of_surjective _ Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective, ringKrullDim_le_of_surjective