awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
C : Type u_5
inst_5 : Semiring C
inst_6 : Algebra R C
F : Type u_6
inst_7 : FunLike F (Unitization R A) C
inst_8 : AlgHomClass F R (Unitization R A) C
φ ψ : F
h :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := C) ((φ : (a : Unitization R A) → C) (↑a : Unitization R A) : C)
      ((ψ : (a : Unitization R A) → C) (↑a : Unitization R A) : C)
r : R
⊢ Eq.{u_5 + 1} (α := C)
    ((φ : (a : Unitization R A) → C)
        ((algebraMap R (Unitization R A) : (a : R) → Unitization R A) r : Unitization R A) :
      C)
    ((ψ : (a : Unitization R A) → C)
        ((algebraMap R (Unitization R A) : (a : R) → Unitization R A) r : Unitization R A) :
      C)

Tactic:
simp only [AlgHomClass.commutes]

Premises used: AlgHomClass.commutes
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
C : Type u_5
inst_5 : Semiring C
inst_6 : Algebra R C
φ ψ : Unitization R A →ₐ[R] C
h :
  (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A) =
    (↑ψ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A)
⊢ φ = ψ

Tactic:
algHom_ext'' (NonUnitalAlgHom.congr_fun h)

Premises used: NonUnitalAlgHom.congr_fun, Unitization.algHom_ext''
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
⊢ HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (toProd 1).1 : C) ((φ : (a : A) → C) (toProd 1).2 : C) = 1

Tactic:
simp only [fst_one, map_one, snd_one, φ.map_zero, add_zero]

Premises used: NonUnitalAlgHom.map_zero, Unitization.fst_one, map_one, Unitization.snd_one, add_zero
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
r : R
a : A
inl_add_inr :
  HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
      (HSMul.hSMul (β := C) x_r ((φ : (a : A) → C) a : C) + HSMul.hSMul (β := C) r ((φ : (a : A) → C) x_a : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C)) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((φ : (a : A) → C) x_a : C) *
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((φ : (a : A) → C) a : C)
⊢ HAdd.hAdd (α := C) (β := C)
      ((algebraMap R C : (a : R) → C)
          ((inl x_r + (↑x_a : Unitization R A)) * (inl r + (↑a : Unitization R A))).toProd.1 :
        C)
      ((φ : (a : A) → C) ((inl x_r + (↑x_a : Unitization R A)) * (inl r + (↑a : Unitization R A))).toProd.2 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl x_r + (↑x_a : Unitization R A)).toProd.1 : C)
        ((φ : (a : A) → C) (inl x_r + (↑x_a : Unitization R A)).toProd.2 : C) *
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A)).toProd.1 : C)
        ((φ : (a : A) → C) (inl r + (↑a : Unitization R A)).toProd.2 : C)

Tactic:
simp only [fst_mul, fst_add, fst_inl, fst_inr, snd_mul, snd_add, snd_inl, snd_inr, add_zero,
          map_mul, zero_add, map_add, map_smul φ]

Premises used: Unitization.fst_inr, Unitization.fst_inl, Unitization.snd_inr, Unitization.snd_mul, Unitization.fst_mul, map_add, Unitization.fst_add, zero_add, map_mul, Unitization.snd_add, add_zero, Unitization.snd_inl, map_smul
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
r : R
a : A
inl_add_inr :
  HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
      (HSMul.hSMul (β := C) x_r ((φ : (a : A) → C) a : C) + HSMul.hSMul (β := C) r ((φ : (a : A) → C) x_a : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C)) =
    HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
        HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((φ : (a : A) → C) a : C) +
      (HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((algebraMap R C : (a : R) → C) r : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C))
⊢ HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
      (HSMul.hSMul (β := C) x_r ((φ : (a : A) → C) a : C) + HSMul.hSMul (β := C) r ((φ : (a : A) → C) x_a : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C)) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((φ : (a : A) → C) x_a : C) *
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((φ : (a : A) → C) a : C)

Tactic:
rw [add_mul, mul_add, mul_add]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
r : R
a : A
inl_add_inr :
  HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
      (HSMul.hSMul (β := C) x_r ((φ : (a : A) → C) a : C) + HSMul.hSMul (β := C) r ((φ : (a : A) → C) x_a : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C)) =
    HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
        HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((φ : (a : A) → C) a : C) +
      (HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((φ : (a : A) → C) x_a : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C))
⊢ HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
      (HSMul.hSMul (β := C) x_r ((φ : (a : A) → C) a : C) + HSMul.hSMul (β := C) r ((φ : (a : A) → C) x_a : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C)) =
    HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
        HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((φ : (a : A) → C) a : C) +
      (HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((algebraMap R C : (a : R) → C) r : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C))

Tactic:
rw [← Algebra.commutes _ (φ x_a)]

Premises used: DFunLike.coe, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
r : R
a : A
⊢ HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
      (HSMul.hSMul (β := C) x_r ((φ : (a : A) → C) a : C) + HSMul.hSMul (β := C) r ((φ : (a : A) → C) x_a : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C)) =
    HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((algebraMap R C : (a : R) → C) r : C) +
        HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) x_r : C) ((φ : (a : A) → C) a : C) +
      (HMul.hMul (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((φ : (a : A) → C) x_a : C) +
        HMul.hMul (α := C) (β := C) ((φ : (a : A) → C) x_a : C) ((φ : (a : A) → C) a : C))

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]

Premises used: add_assoc, Algebra.algebraMap_eq_smul_one, smul_one_mul
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
y : Unitization R A
x_r : R
x_a : A
inl_add_inr :
  ∀ (r : R) (a : A),
    HAdd.hAdd (α := C) (β := C)
        ((algebraMap R C : (a : R) → C)
            ((inl x_r + (↑x_a : Unitization R A)) * (inl r + (↑a : Unitization R A))).toProd.1 :
          C)
        ((φ : (a : A) → C) ((inl x_r + (↑x_a : Unitization R A)) * (inl r + (↑a : Unitization R A))).toProd.2 : C) =
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl x_r + (↑x_a : Unitization R A)).toProd.1 : C)
          ((φ : (a : A) → C) (inl x_r + (↑x_a : Unitization R A)).toProd.2 : C) *
        HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A)).toProd.1 : C)
          ((φ : (a : A) → C) (inl r + (↑a : Unitization R A)).toProd.2 : C)
⊢ HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) ((inl x_r + (↑x_a : Unitization R A)) * y).toProd.1 : C)
      ((φ : (a : A) → C) ((inl x_r + (↑x_a : Unitization R A)) * y).toProd.2 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl x_r + (↑x_a : Unitization R A)).toProd.1 : C)
        ((φ : (a : A) → C) (inl x_r + (↑x_a : Unitization R A)).toProd.2 : C) *
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) y.toProd.1 : C) ((φ : (a : A) → C) y.toProd.2 : C)

Tactic:
induction y with
      | inl_add_inr =>
        simp only [fst_mul, fst_add, fst_inl, fst_inr, snd_mul, snd_add, snd_inl, snd_inr, add_zero,
          map_mul, zero_add, map_add, map_smul φ]
        rw [add_mul, mul_add, mul_add]
        rw [← Algebra.commutes _ (φ x_a)]
        simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]

Premises used: add_mul, Unitization.fst_inr, Unitization.fst_inl, Unitization.snd_inr, add_assoc, Unitization.snd_mul, Unitization.fst_mul, map_add, Unitization.fst_add, zero_add, Algebra.algebraMap_eq_smul_one, map_mul, smul_one_mul, mul_add, Unitization.snd_add, add_zero, Unitization.snd_inl, DFunLike.coe, Algebra.commutes, map_smul
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
x y : Unitization R A
inl_add_inr :
  ∀ (x_r : R) (x_a : A),
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) ((inl x_r + (↑x_a : Unitization R A)) * y).toProd.1 : C)
        ((φ : (a : A) → C) ((inl x_r + (↑x_a : Unitization R A)) * y).toProd.2 : C) =
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl x_r + (↑x_a : Unitization R A)).toProd.1 : C)
          ((φ : (a : A) → C) (inl x_r + (↑x_a : Unitization R A)).toProd.2 : C) *
        HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) y.toProd.1 : C) ((φ : (a : A) → C) y.toProd.2 : C)
⊢ HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (x * y).toProd.1 : C)
      ((φ : (a : A) → C) (x * y).toProd.2 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) x.toProd.1 : C) ((φ : (a : A) → C) x.toProd.2 : C) *
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) y.toProd.1 : C) ((φ : (a : A) → C) y.toProd.2 : C)

Tactic:
induction x with
    | inl_add_inr x_r x_a =>
      induction y with
      | inl_add_inr =>
        simp only [fst_mul, fst_add, fst_inl, fst_inr, snd_mul, snd_add, snd_inl, snd_inr, add_zero,
          map_mul, zero_add, map_add, map_smul φ]
        rw [add_mul, mul_add, mul_add]
        rw [← Algebra.commutes _ (φ x_a)]
        simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]

Premises used: add_mul, Unitization.fst_inr, Unitization.fst_inl, Unitization.snd_inr, add_assoc, Unitization.snd_mul, Unitization.fst_mul, map_add, Unitization.fst_add, zero_add, Algebra.algebraMap_eq_smul_one, map_mul, smul_one_mul, mul_add, Unitization.snd_add, add_zero, Unitization.snd_inl, map_smul
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
⊢ HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (toProd 0).1 : C) ((φ : (a : A) → C) (toProd 0).2 : C) = 0

Tactic:
simp only [fst_zero, map_zero, snd_zero, φ.map_zero, add_zero]

Premises used: Unitization.fst_zero, map_zero, NonUnitalAlgHom.map_zero, Unitization.snd_zero, add_zero
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
r : R
a : A
r_1 : R
a_1 : A
inl_add_inr :
  HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((algebraMap R C : (a : R) → C) r_1 : C) +
      HAdd.hAdd (α := C) (β := C) ((φ : (a : A) → C) a : C) ((φ : (a : A) → C) a_1 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((φ : (a : A) → C) a : C) +
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r_1 : C) ((φ : (a : A) → C) a_1 : C)
⊢ HAdd.hAdd (α := C) (β := C)
      ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A) + (inl r_1 + (↑a_1 : Unitization R A))).toProd.1 :
        C)
      ((φ : (a : A) → C) (inl r + (↑a : Unitization R A) + (inl r_1 + (↑a_1 : Unitization R A))).toProd.2 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A)).toProd.1 : C)
        ((φ : (a : A) → C) (inl r + (↑a : Unitization R A)).toProd.2 : C) +
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r_1 + (↑a_1 : Unitization R A)).toProd.1 : C)
        ((φ : (a : A) → C) (inl r_1 + (↑a_1 : Unitization R A)).toProd.2 : C)

Tactic:
simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr,
          zero_add, φ.map_add]

Premises used: Unitization.fst_inr, Unitization.fst_inl, Unitization.snd_inr, map_add, Unitization.fst_add, zero_add, NonUnitalAlgHom.map_add, Unitization.snd_add, add_zero, Unitization.snd_inl
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
r : R
a : A
r_1 : R
a_1 : A
inl_add_inr inl_add_inr₁ :
  HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((φ : (a : A) → C) a : C) +
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r_1 : C) ((φ : (a : A) → C) a_1 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((φ : (a : A) → C) a : C) +
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r_1 : C) ((φ : (a : A) → C) a_1 : C)
⊢ HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((algebraMap R C : (a : R) → C) r_1 : C) +
      HAdd.hAdd (α := C) (β := C) ((φ : (a : A) → C) a : C) ((φ : (a : A) → C) a_1 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r : C) ((φ : (a : A) → C) a : C) +
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) r_1 : C) ((φ : (a : A) → C) a_1 : C)

Tactic:
rw [add_add_add_comm]

Premises used: add_add_add_comm
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
y : Unitization R A
r : R
a : A
inl_add_inr :
  ∀ (r_1 : R) (a_1 : A),
    HAdd.hAdd (α := C) (β := C)
        ((algebraMap R C : (a : R) → C)
            (inl r + (↑a : Unitization R A) + (inl r_1 + (↑a_1 : Unitization R A))).toProd.1 :
          C)
        ((φ : (a : A) → C) (inl r + (↑a : Unitization R A) + (inl r_1 + (↑a_1 : Unitization R A))).toProd.2 : C) =
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A)).toProd.1 : C)
          ((φ : (a : A) → C) (inl r + (↑a : Unitization R A)).toProd.2 : C) +
        HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r_1 + (↑a_1 : Unitization R A)).toProd.1 : C)
          ((φ : (a : A) → C) (inl r_1 + (↑a_1 : Unitization R A)).toProd.2 : C)
⊢ HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A) + y).toProd.1 : C)
      ((φ : (a : A) → C) (inl r + (↑a : Unitization R A) + y).toProd.2 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A)).toProd.1 : C)
        ((φ : (a : A) → C) (inl r + (↑a : Unitization R A)).toProd.2 : C) +
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) y.toProd.1 : C) ((φ : (a : A) → C) y.toProd.2 : C)

Tactic:
induction y with
      | inl_add_inr =>
        simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr,
          zero_add, φ.map_add]
        rw [add_add_add_comm]

Premises used: Unitization.fst_inr, Unitization.fst_inl, Unitization.snd_inr, map_add, Unitization.fst_add, zero_add, NonUnitalAlgHom.map_add, Unitization.snd_add, add_add_add_comm, add_zero, Unitization.snd_inl
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
x y : Unitization R A
inl_add_inr :
  ∀ (r : R) (a : A),
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A) + y).toProd.1 : C)
        ((φ : (a : A) → C) (inl r + (↑a : Unitization R A) + y).toProd.2 : C) =
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (inl r + (↑a : Unitization R A)).toProd.1 : C)
          ((φ : (a : A) → C) (inl r + (↑a : Unitization R A)).toProd.2 : C) +
        HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) y.toProd.1 : C) ((φ : (a : A) → C) y.toProd.2 : C)
⊢ HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) (x + y).toProd.1 : C)
      ((φ : (a : A) → C) (x + y).toProd.2 : C) =
    HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) x.toProd.1 : C) ((φ : (a : A) → C) x.toProd.2 : C) +
      HAdd.hAdd (α := C) (β := C) ((algebraMap R C : (a : R) → C) y.toProd.1 : C) ((φ : (a : A) → C) y.toProd.2 : C)

Tactic:
induction x with
    | inl_add_inr =>
      induction y with
      | inl_add_inr =>
        simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr,
          zero_add, φ.map_add]
        rw [add_add_add_comm]

Premises used: Unitization.fst_inr, Unitization.fst_inl, Unitization.snd_inr, map_add, Unitization.fst_add, zero_add, NonUnitalAlgHom.map_add, Unitization.snd_add, add_add_add_comm, add_zero, Unitization.snd_inl
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
r : R
⊢ HAdd.hAdd (α := C) (β := C)
      ((algebraMap R C : (a : R) → C) (toProd ((algebraMap R (Unitization R A) : (a : R) → Unitization R A) r)).1 : C)
      ((φ : (a : A) → C) (toProd ((algebraMap R (Unitization R A) : (a : R) → Unitization R A) r)).2 : C) =
    (algebraMap R C : (a : R) → C) r

Tactic:
simp only [algebraMap_eq_inl, fst_inl, snd_inl, φ.map_zero, add_zero]

Premises used: Unitization.fst_inl, NonUnitalAlgHom.map_zero, Unitization.algebraMap_eq_inl, add_zero, Unitization.snd_inl
-- Module: Mathlib.Algebra.Algebra.Unitization
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 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : A →ₙₐ[R] C
h :
  ∀ (x : A),
    Eq.{u_5 + 1} (α := C)
      (((fun (φ : Unitization R A →ₐ[R] C) ↦ (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A)) φ.toAlgHom :
            (a : A) → C)
          x :
        C)
      ((φ : (a : A) → C) x : C)
⊢ (fun (φ : Unitization R A →ₐ[R] C) ↦ (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A)) φ.toAlgHom = φ

Tactic:
ext