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
r s : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) 0 =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0 +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0
⊢ (r + s) • x = r • x + s • x
have tmul : ∀ (x : S) (y : Ω[A⁄R]),
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y) +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
Tactic: induction 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
r s : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) 0 =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0 +
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0
tmul :
  ∀ (x : S) (y : Ω[A⁄R]),
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (r + s) (x ⊗ₜ[R] y) =
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y) +
        HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
⊢ (r + s) • x = r • x + s • x
have add : ∀ (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
  (r + s) • x = r • x + s • x → (r + s) • y = r • y + s • y → (r + s) • (x + y) = r • (x + y) + s • (x + y)
Tactic: induction 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
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ HSMul.hSMul (α := A) 0 x = 0
have zero : HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 0 = 0
Tactic: induction 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
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero : HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 0 = 0
⊢ HSMul.hSMul (α := A) 0 x = 0
have tmul : ∀ (x : S) (y : Ω[A⁄R]), HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 (x ⊗ₜ[R] y) = 0
Tactic: induction 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
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero : HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 0 = 0
tmul : ∀ (x : S) (y : Ω[A⁄R]), HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 (x ⊗ₜ[R] y) = 0
⊢ HSMul.hSMul (α := A) 0 x = 0
have add : ∀ (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
  HSMul.hSMul (α := A) 0 x = 0 → HSMul.hSMul (α := A) 0 y = 0 → HSMul.hSMul (α := A) 0 (x + y) = 0
Tactic: induction 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
⊢ IsScalarTower R A (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
have h : ∀ (r : R) (x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
  HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
Tactic: apply IsScalarTower.of_algebraMap_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
r : R
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
have h : HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A) 0 =
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0
Tactic: induction 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
r : R
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
h :
  HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A) 0 =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0
⊢ HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
have h₁ : ∀ (x : S) (y : Ω[A⁄R]),
  HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A)
      (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
Tactic: induction 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
r : R
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
h :
  HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A) 0 =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r 0
h₁ :
  ∀ (x : S) (y : Ω[A⁄R]),
    HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A)
        (x ⊗ₜ[R] y) =
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
⊢ HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
have h₂ : ∀ (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
  HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x →
    HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y = r • y →
      HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x + y) = r • (x + y)
Tactic: induction 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
r : R
x : S
y : Ω[A⁄R]
⊢ HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A)
      (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
have h : x ⊗ₜ[R] HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
Tactic: rw [mulActionBaseChange_smul_tmul, algebraMap_smul, tmul_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
r : R
x : S
y : Ω[A⁄R]
h :
  x ⊗ₜ[R] HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
⊢ HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A)
      (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
have h₁ : x ⊗ₜ[R] (r • y) = HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
Tactic: rw [mulActionBaseChange_smul_tmul, algebraMap_smul, tmul_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
r : R
x : S
y : Ω[A⁄R]
h :
  x ⊗ₜ[R] HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
h₁ : x ⊗ₜ[R] (r • y) = HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
⊢ HSMul.hSMul (α := A) (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((algebraMap R A : (a : R) → A) r : A)
      (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
have h₂ : HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y) =
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) r (x ⊗ₜ[R] y)
Tactic: rw [mulActionBaseChange_smul_tmul, algebraMap_smul, tmul_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
s : S
a : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ s • a • x = a • s • x
have zero : s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 =
  a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0
Tactic: induction 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
s : S
a : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero :
  s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0
⊢ s • a • x = a • s • x
have tmul : ∀ (x : S) (y : Ω[A⁄R]),
  s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (x ⊗ₜ[R] y) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
Tactic: induction 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
s : S
a : A
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero :
  s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a 0 =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s 0
tmul :
  ∀ (x : S) (y : Ω[A⁄R]),
    s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (x ⊗ₜ[R] y) =
      a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
⊢ s • a • x = a • s • x
have add : ∀ (x y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
  s • a • x = a • s • x → s • a • y = a • s • y → s • a • (x + y) = a • s • (x + y)
Tactic: induction 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
s : S
a : A
x : S
y : Ω[A⁄R]
⊢ s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (x ⊗ₜ[R] y) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
have tmul : HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] (a • y)) =
  a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
Tactic: rw [mulActionBaseChange_smul_tmul, smul_tmul', smul_tmul', mulActionBaseChange_smul_tmul]
-- 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
s : S
a : A
x : S
y : Ω[A⁄R]
tmul :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] (a • y)) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
⊢ s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (x ⊗ₜ[R] y) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
have tmul₁ : (s • x) ⊗ₜ[R] (a • y) = a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
Tactic: rw [mulActionBaseChange_smul_tmul, smul_tmul', smul_tmul', mulActionBaseChange_smul_tmul]
-- 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
s : S
a : A
x : S
y : Ω[A⁄R]
tmul :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] (a • y)) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
tmul₁ : (s • x) ⊗ₜ[R] (a • y) = a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
⊢ s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (x ⊗ₜ[R] y) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
have tmul₂ : (s • x) ⊗ₜ[R] (a • y) = HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a ((s • x) ⊗ₜ[R] y)
Tactic: rw [mulActionBaseChange_smul_tmul, smul_tmul', smul_tmul', mulActionBaseChange_smul_tmul]
-- 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
s : S
a : A
x : S
y : Ω[A⁄R]
tmul :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] (a • y)) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
tmul₁ : (s • x) ⊗ₜ[R] (a • y) = a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
tmul₂ : (s • x) ⊗ₜ[R] (a • y) = HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a ((s • x) ⊗ₜ[R] y)
⊢ s • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) a (x ⊗ₜ[R] y) =
    a • HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) s (x ⊗ₜ[R] y)
have tmul₃ : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) ((s • x) ⊗ₜ[R] (a • y)) ((s • x) ⊗ₜ[R] (a • y))
Tactic: rw [mulActionBaseChange_smul_tmul, smul_tmul', smul_tmul', mulActionBaseChange_smul_tmul]
-- 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
s : A
a : S
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
⊢ s • a • x = a • s • x
have rw : a • s • x = a • s • x
Tactic: rw [← smul_comm]
-- 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
⊢ IsScalarTower A B (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
have h : ∀ (r : A) (x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
  HSMul.hSMul (α := B) ((algebraMap A B : (a : A) → B) r : B) x = r • x
Tactic: apply IsScalarTower.of_algebraMap_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
inst_11 : Algebra.IsPushout R S A B
⊢ IsScalarTower S B (TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
have h : ∀ (r : S) (x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]),
  HSMul.hSMul (α := B) ((algebraMap S B : (a : S) → B) r : B) x = r • x
Tactic: apply IsScalarTower.of_algebraMap_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
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    ((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])
      1)
    0
have rw : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
  ((IsBaseChange.lift (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)) sorry
        ((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) 1))
  0
Tactic: rw [← (algebraMap A B).map_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
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    ((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) 1))
    0
have refine : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
  (((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])
    1)
  0
Tactic: refine (h.out.lift_eq _ _).trans ?_
-- 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
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    (1 ⊗ₜ[R] (D R A : (a : A) → Ω[A⁄R]) 1 : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    (0 : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
have rw : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (1 ⊗ₜ[R] 0) 0
Tactic: rw [Derivation.map_one_eq_zero, TensorProduct.tmul_zero]
-- 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
rw : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (1 ⊗ₜ[R] 0) 0
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    (1 ⊗ₜ[R] (D R A : (a : A) → Ω[A⁄R]) 1 : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    (0 : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
have rw₁ : Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) 0 0
Tactic: rw [Derivation.map_one_eq_zero, TensorProduct.tmul_zero]