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 :
  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)
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)
⊢ 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) s (↑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
x : Unitization R A
⊢ s • x =
    HMul.hMul (α := Unitization R A)
      ((RingHom.comp (inlRingHom R A) (algebraMap S R) : (a : S) → Unitization R A) s : Unitization R A) x
have inl_add_inr : ∀ (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))
Tactic: induction x with
    | inl_add_inr =>
      change _ = inl (algebraMap S R s) * _
      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]
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 : 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
F : Type u_6
inst_11 : FunLike F (Unitization R A) B
inst_12 : AlgHomClass F S (Unitization R A) B
φ ψ : F
h :
  ∀ (a : A),
    Eq.{u_4 + 1} (α := B) ((φ : (a : Unitization R A) → B) (↑a : Unitization R A) : B)
      ((ψ : (a : Unitization R A) → B) (↑a : Unitization R A) : B)
h' :
  ∀ (r : R),
    Eq.{u_4 + 1} (α := B)
      ((φ : (a : Unitization R A) → B)
          ((algebraMap R (Unitization R A) : (a : R) → Unitization R A) r : Unitization R A) :
        B)
      ((ψ : (a : Unitization R A) → B)
          ((algebraMap R (Unitization R A) : (a : R) → Unitization R A) r : Unitization R A) :
        B)
⊢ φ = ψ
have refine : ∀ (x : Unitization R A),
  Eq.{u_4 + 1} (α := B) ((φ : (a : Unitization R A) → B) x : B) ((ψ : (a : Unitization R A) → B) x : B)
Tactic: refine DFunLike.ext φ ψ (fun 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 : 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
F : Type u_6
inst_11 : FunLike F (Unitization R A) B
inst_12 : AlgHomClass F S (Unitization R A) B
φ ψ : F
h :
  ∀ (a : A),
    Eq.{u_4 + 1} (α := B) ((φ : (a : Unitization R A) → B) (↑a : Unitization R A) : B)
      ((ψ : (a : Unitization R A) → B) (↑a : Unitization R A) : B)
h' :
  ∀ (r : R),
    Eq.{u_4 + 1} (α := B)
      ((φ : (a : Unitization R A) → B)
          ((algebraMap R (Unitization R A) : (a : R) → Unitization R A) r : Unitization R A) :
        B)
      ((ψ : (a : Unitization R A) → B)
          ((algebraMap R (Unitization R A) : (a : R) → Unitization R A) r : Unitization R A) :
        B)
x : Unitization R A
⊢ Eq.{u_4 + 1} (α := B) ((φ : (a : Unitization R A) → B) x : B) ((ψ : (a : Unitization R A) → B) x : B)
have inl_add_inr : ∀ (r : R) (a : A),
  Eq.{u_4 + 1} (α := B) ((φ : (a : Unitization R A) → B) (inl r + (↑a : Unitization R A)) : B)
    ((ψ : (a : Unitization R A) → B) (inl r + (↑a : Unitization R A)) : B)
Tactic: induction x
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 : 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
⊢ 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)
have 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)
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 φ]
-- 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 : 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)) =
    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)
have 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))
Tactic: rw [add_mul, mul_add, mul_add]
-- 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 : 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) ((φ : (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))
have 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))
Tactic: rw [← Algebra.commutes _ (φ x_a)]
-- 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 : 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
⊢ 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)
have 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)
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]
Cleared hypotheses: y
-- 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 : 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
⊢ 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)
have 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)
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]
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 : 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
⊢ 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)
have 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)
Tactic: simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr,
          zero_add, φ.map_add]
-- 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 : 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
⊢ 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)
have 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)
Tactic: rw [add_add_add_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 : 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
⊢ 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)
have 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)
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]
Cleared hypotheses: y
-- 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 : 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
⊢ 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)
have 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)
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]
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 : 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
⊢ (fun (φ : Unitization R A →ₐ[R] C) ↦ (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A)) φ.toAlgHom = φ
have 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)
Tactic: ext