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
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
⊢ 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])
have 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])
Tactic: simp only [← mul_smul, ← @algebraMap_smul S _ B, ← @algebraMap_smul A _ B]
-- 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 ⊗[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])
have tmul : (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) 0 ⊗ₜ[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) 0 ⊗ₜ[A] y) : Ω[B⁄S])
Tactic: induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *, add_tmul]
  | tmul x z =>
  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]
  simp only [← mul_smul, ← @algebraMap_smul S _ B, ← @algebraMap_smul A _ B]
  ring_nf
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)
x : B ⊗[A] Ω[A⁄R]
a : A
b : S
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) x) =
    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 : Ω[B⁄S])
have tmul : (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)
      0) =
  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]) 0)
Tactic: induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *]
  | tmul x y =>
  obtain ⟨x, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective x
  induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *, add_tmul]
  | tmul x z =>
  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]
  simp only [← mul_smul, ← @algebraMap_smul S _ B, ← @algebraMap_smul A _ B]
  ring_nf
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)
x : B ⊗[A] Ω[A⁄R]
m : A ⊗[R] S
⊢ (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])
have zero : (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
    (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 : B) x) =
  HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 : B)
    ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x : Ω[B⁄S])
Tactic: induction m with
  | zero => simp
  | add x y _ _ => simp only [add_smul, map_add, *]
  | tmul a b =>
  induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *]
  | tmul x y =>
  obtain ⟨x, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective x
  induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *, add_tmul]
  | tmul x z =>
  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]
  simp only [← mul_smul, ← @algebraMap_smul S _ B, ← @algebraMap_smul A _ B]
  ring_nf
Cleared hypotheses: m
-- 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
inst_11 : Algebra.IsPushout R S A B
b : B
a : A
⊢ (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])
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
inst_11 : Algebra.IsPushout R S A B
b : B
a : A
this : Algebra.IsPushout R A S B
⊢ (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])
have 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])
Tactic: obtain ⟨b, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective b
Cleared hypotheses: b
-- 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
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) =
    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])
have 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])
Tactic: trans s • a' • D S B (algebraMap A B a)
-- 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
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])
⊢ (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])
have 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])
Tactic: trans s • a' • D S B (algebraMap A B a)
-- 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
a : A
this : Algebra.IsPushout R A S B
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])
have zero : (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: induction b with
  | zero => simp
  | add x y _ _ => simp only [map_add, *, add_tmul, add_smul]
  | tmul a' s =>
  trans s • a' • D S B (algebraMap A B a)
  · simp [tensorKaehlerEquiv]
  · simp [Algebra.IsPushout.equiv_tmul, mul_smul, smul_comm]
Cleared hypotheses: b
-- 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
a : A
this : Algebra.IsPushout R A S B
b : A ⊗[R] S
zero :
  (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])
⊢ (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])
have add : ∀ (x y : 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) 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]) →
    (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: induction b with
  | zero => simp
  | add x y _ _ => simp only [map_add, *, add_tmul, add_smul]
  | tmul a' s =>
  trans s • a' • D S B (algebraMap A B a)
  · simp [tensorKaehlerEquiv]
  · simp [Algebra.IsPushout.equiv_tmul, mul_smul, smul_comm]
Cleared hypotheses: b
-- 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
a : A
this : Algebra.IsPushout R A S B
b : A ⊗[R] S
zero :
  (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])
add :
  ∀ (x y : 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) 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]) →
      (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])
⊢ (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])
have tmul : ∀ (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) =
    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: induction b with
  | zero => simp
  | add x y _ _ => simp only [map_add, *, add_tmul, add_smul]
  | tmul a' s =>
  trans s • a' • D S B (algebraMap A B a)
  · simp [tensorKaehlerEquiv]
  · simp [Algebra.IsPushout.equiv_tmul, mul_smul, smul_comm]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
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 ⊗[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])
have 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])
Tactic: apply (tensorKaehlerEquiv R S A _).symm_apply_eq.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
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]) ((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])
have 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])
Tactic: simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    tensorKaehlerEquiv_tmul_D]
-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (goal)
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
⊢ (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])
have 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])
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]