awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₂ : Eq (α := R ⊗[R] S)
  (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
  (1 ⊗ₜ[R] s)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₃ : Eq (α := R ⊗[R] S)
  (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
  (1 ⊗ₜ[R] s)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₆ : Eq (α := R ⊗[R] S) (HMul.hMul (α := R) (β := R) ((g : (a : S) → R) s : R) (1 : R) ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₆ : Eq (α := R ⊗[R] S) (HMul.hMul (α := R) (β := R) ((g : (a : S) → R) s : R) (1 : R) ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₇ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₆ : Eq (α := R ⊗[R] S) (HMul.hMul (α := R) (β := R) ((g : (a : S) → R) s : R) (1 : R) ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₇ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₈ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₆ : Eq (α := R ⊗[R] S) (HMul.hMul (α := R) (β := R) ((g : (a : S) → R) s : R) (1 : R) ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₇ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₈ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₉ : Eq (α := R ⊗[R] S)
  (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (s ⊗ₜ[R] 1) : R ⊗[R] S)
  (1 ⊗ₜ[R] s : R ⊗[R] S)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₆ : Eq (α := R ⊗[R] S) (HMul.hMul (α := R) (β := R) ((g : (a : S) → R) s : R) (1 : R) ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₇ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₈ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₉ :
  Eq (α := R ⊗[R] S)
    (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (s ⊗ₜ[R] 1) :
      R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₁₀ : Eq (α := R ⊗[R] S)
  (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (1 ⊗ₜ[R] s) : R ⊗[R] S)
  (1 ⊗ₜ[R] s : R ⊗[R] S)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₆ : Eq (α := R ⊗[R] S) (HMul.hMul (α := R) (β := R) ((g : (a : S) → R) s : R) (1 : R) ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₇ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₈ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₉ :
  Eq (α := R ⊗[R] S)
    (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (s ⊗ₜ[R] 1) :
      R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₁₀ :
  Eq (α := R ⊗[R] S)
    (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (1 ⊗ₜ[R] s) :
      R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₁₁ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) 1 ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) s : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
g : S →ₐ[R] R
s : S
hs : Eq (α := S ⊗[R] S) ((TensorProduct.includeLeftSubRight R S : (a : S) → S ⊗[R] S) s : S ⊗[R] S) (0 : S ⊗[R] S)
h :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
h₁ :
  Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₂ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₃ :
  Eq (α := R ⊗[R] S)
    (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((g : (a : S) → R) s : R) : S) (1 : S))
    (1 ⊗ₜ[R] s)
h₄ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((g : (a : S) → R) s : R) 1) (1 ⊗ₜ[R] s)
h₅ : Eq (α := R ⊗[R] S) (HSMul.hSMul (α := R) (β := R) ((g : (a : S) → R) s : R) 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₆ : Eq (α := R ⊗[R] S) (HMul.hMul (α := R) (β := R) ((g : (a : S) → R) s : R) (1 : R) ⊗ₜ[R] 1) (1 ⊗ₜ[R] s)
h₇ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₈ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) s ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) 1 : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
h₉ :
  Eq (α := R ⊗[R] S)
    (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (s ⊗ₜ[R] 1) :
      R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₁₀ :
  Eq (α := R ⊗[R] S)
    (((TensorProduct.map g (AlgHom.id R S) : S ⊗[R] S →ₐ[R] R ⊗[R] S) : (a : S ⊗[R] S) → R ⊗[R] S) (1 ⊗ₜ[R] s) :
      R ⊗[R] S)
    (1 ⊗ₜ[R] s : R ⊗[R] S)
h₁₁ : Eq (α := R ⊗[R] S) ((g : (a : S) → R) 1 ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) s : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
⊢ Eq (α := R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S)
        ((Algebra.linearMap R S : (a : R) → S) ((g : (a : S) → R) s : R)) :
      R ⊗[R] S)
    ((AlgEquiv.symm (TensorProduct.lid R S) : (a : S) → R ⊗[R] S) s : R ⊗[R] S)
have h₁₂ : Eq (α := R ⊗[R] S) (1 ⊗ₜ[R] (AlgHom.id R S : (a : S) → S) s : R ⊗[R] S) (1 ⊗ₜ[R] s : R ⊗[R] S)
Tactic: rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]