awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
inl_add_inr₁ :
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl r)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
inl_add_inr₂ :
  inl (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) s : R) r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl r)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
⊢ HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A)) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
have inl_add_inr₃ : inl (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) s : R) r) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      ((↑a : Unitization R A) : Unitization R A) =
  inl (HMul.hMul (β := R) r ((algebraMap S R : (a : S) → R) s : R)) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
Tactic: rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
x : Unitization R A
⊢ HMul.hMul (α := Unitization R A)
      ((RingHom.comp (inlRingHom R A) (algebraMap S R) : (a : S) → Unitization R A) s : Unitization R A) x =
    HMul.hMul (β := Unitization R A) x
      ((RingHom.comp (inlRingHom R A) (algebraMap S R) : (a : S) → Unitization R A) s : Unitization R A)
have inl_add_inr : ∀ (r : R) (a : A),
  HMul.hMul (α := Unitization R A)
      ((RingHom.comp (inlRingHom R A) (algebraMap S R) : (a : S) → Unitization R A) s : Unitization R A)
      (inl r + (↑a : Unitization R A)) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      ((RingHom.comp (inlRingHom R A) (algebraMap S R) : (a : S) → Unitization R A) s : Unitization R A)
Tactic: induction x with
    | inl_add_inr =>
      change inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
      rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A)
      ((RingHom.comp (inlRingHom R A) (algebraMap S R) : (a : S) → Unitization R A) s : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr : s • (inl r + (↑a : Unitization R A)) =
  HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
    (inl r + (↑a : Unitization R A))
Tactic: change _ = inl (algebraMap S R s) * _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr : s • (inl r + (↑a : Unitization R A)) =
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      ((↑a : Unitization R A) : Unitization R A)
Tactic: rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr₁ : HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      ((↑a : Unitization R A) : Unitization R A)
Tactic: rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₁ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr₂ : HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
  HMul.hMul (α := Unitization R A) (inl (HSMul.hSMul (β := R) s 1)) (inl r) +
    inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
Tactic: rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₁ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₂ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (inl (HSMul.hSMul (β := R) s 1)) (inl r) +
      inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr₃ : HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
  inl (HSMul.hSMul (β := R) s 1 * r) + inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
Tactic: rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₁ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₂ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (inl (HSMul.hSMul (β := R) s 1)) (inl r) +
      inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₃ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr₄ : HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
  inl (HSMul.hSMul (β := R) s 1 * r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
Tactic: rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₁ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₂ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (inl (HSMul.hSMul (β := R) s 1)) (inl r) +
      inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₃ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₄ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr₅ : HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
  inl (s • r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
Tactic: rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₁ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₂ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (inl (HSMul.hSMul (β := R) s 1)) (inl r) +
      inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₃ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₄ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
inl_add_inr₅ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (s • r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr₆ : HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
  HSMul.hSMul (β := Unitization R A) s (inl r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
Tactic: rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₁ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A)
inl_add_inr₂ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (inl (HSMul.hSMul (β := R) s 1)) (inl r) +
      inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₃ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₄ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
inl_add_inr₅ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (s • r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
inl_add_inr₆ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HSMul.hSMul (β := Unitization R A) s (inl r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
⊢ s • (inl r + (↑a : Unitization R A)) =
    HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A))
have inl_add_inr₇ : HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
  HSMul.hSMul (β := Unitization R A) s (inl r) +
    HSMul.hSMul (β := Unitization R A) (HSMul.hSMul (β := R) s 1) (↑a : Unitization R A)
Tactic: rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]