awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_5
A : Type u_6
inst : AddZeroClass R
inst_1 : AddZeroClass A
P : Unitization R A → Prop
inl_add_inr : ∀ (r : R) (a : A), P (inl r + (↑a : Unitization R A))
x : Unitization R A
⊢ P x

Tactic:
inl_fst_add_inr_snd_eq x ▸ inl_add_inr x.fst x.snd

Premises used: Eq.rec, Prod.fst, Unitization.toProd, Prod.snd, Unitization.inl_fst_add_inr_snd_eq
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
S : Type u_2
R : Type u_3
A : Type u_4
N : Type u_5
inst : CommSemiring S
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid N
inst_4 : Module S R
inst_5 : Module S A
inst_6 : Module S N
f g : Unitization R A →ₗ[S] N
hl :
  ∀ (r : R),
    Eq.{u_5 + 1} (α := N) ((f : (a : Unitization R A) → N) (inl r) : N) ((g : (a : Unitization R A) → N) (inl r) : N)
hr :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := N) ((f : (a : Unitization R A) → N) (↑a : Unitization R A) : N)
      ((g : (a : Unitization R A) → N) (↑a : Unitization R A) : N)
⊢ f = g

Tactic:
(linearEquiv S R A).arrowCongr (.refl ..) |>.injective <|
    LinearMap.prod_ext (LinearMap.ext hl) (LinearMap.ext hr)

Premises used: LinearMap.ext, LinearEquiv.arrowCongr, Unitization.linearEquiv, LinearEquiv.refl, LinearEquiv.injective, LinearMap.prod_ext
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
S : Type u_2
R : Type u_3
A : Type u_4
inst : Semiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Module S R
inst_4 : Module S A
⊢ Function.Injective (α := A) (β := Unitization R A) (⇑(inrHom S R A) : (a : A) → Unitization R A)

Tactic:
Unitization.inr_injective

Premises used: Unitization.inr, Unitization.inr_injective
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : One R
inst_1 : Zero A
⊢ Eq.{u_1 + 1} (α := R) (toProd 1).1 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : One R
inst_1 : Zero A
⊢ Eq.{u_2 + 1} (α := A) (toProd 1).2 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : Add A
inst_2 : Mul A
inst_3 : SMul R A
x₁ x₂ : Unitization R A
⊢ (x₁ * x₂).toProd.1 = x₁.toProd.1 * x₂.toProd.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : Add A
inst_2 : Mul A
inst_3 : SMul R A
x₁ x₂ : Unitization R A
⊢ (x₁ * x₂).toProd.2 = x₁.toProd.1 • x₂.toProd.2 + x₂.toProd.1 • x₁.toProd.2 + x₁.toProd.2 * x₂.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : One R
inst_1 : Zero A
⊢ Eq (α := Unitization R A) (inl 1) 1

Tactic:
rfl

Premises used: Unitization.inl, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : SMulZeroClass R A
r₁ r₂ : R
⊢ (toProd (inl (r₁ * r₂))).2 = (HMul.hMul (α := Unitization R A) (inl r₁) (inl r₂)).toProd.2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : SMulZeroClass R A
r₁ r₂ : R
⊢ HMul.hMul (α := Unitization R A) (inl r₁) (inl r₂) = inl (r₁ * r₂)

Tactic:
(inl_mul A r₁ r₂).symm

Premises used: Unitization.inl_mul, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : MulZeroClass R
inst_1 : AddZeroClass A
inst_2 : Mul A
inst_3 : SMulWithZero R A
a₁ a₂ : A
⊢ (toProd (↑(a₁ * a₂) : Unitization R A)).2 =
    (HMul.hMul (α := Unitization R A) (↑a₁ : Unitization R A) (↑a₂ : Unitization R A)).toProd.2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : MulZeroClass R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : SMulZeroClass R A
r : R
a : A
⊢ (inl r * (↑a : Unitization R A)).toProd.2 = (toProd (↑(r • a) : Unitization R A)).2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : MulZeroClass R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : SMulZeroClass R A
r : R
a : A
⊢ ((↑a : Unitization R A) * inl r).toProd.2 = (toProd (↑(r • a) : Unitization R A)).2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
x : Unitization R A
⊢ (1 * x).toProd.2 = x.toProd.2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
x : Unitization R A
⊢ (x * 1).toProd.2 = x.toProd.2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x x_1 x_2 : Unitization R A
simp :
  x.toProd.1 • x_1.toProd.2 + x.toProd.1 • x_2.toProd.2 + (x_1.toProd.1 • x.toProd.2 + x_2.toProd.1 • x.toProd.2) +
      (x.toProd.2 * x_1.toProd.2 + x.toProd.2 * x_2.toProd.2) =
    x.toProd.1 • x_1.toProd.2 + x_1.toProd.1 • x.toProd.2 + x.toProd.2 * x_1.toProd.2 +
      (x.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x.toProd.2 + x.toProd.2 * x_2.toProd.2)
⊢ (x * (x_1 + x_2)).toProd.2 = (x * x_1 + x * x_2).toProd.2

Tactic:
simp [smul_add, add_smul, mul_add]

Premises used: add_smul, mul_add, smul_add
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x x_1 x_2 : Unitization R A
⊢ x.toProd.1 • x_1.toProd.2 + x.toProd.1 • x_2.toProd.2 + (x_1.toProd.1 • x.toProd.2 + x_2.toProd.1 • x.toProd.2) +
      (x.toProd.2 * x_1.toProd.2 + x.toProd.2 * x_2.toProd.2) =
    x.toProd.1 • x_1.toProd.2 + x_1.toProd.1 • x.toProd.2 + x.toProd.2 * x_1.toProd.2 +
      (x.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x.toProd.2 + x.toProd.2 * x_2.toProd.2)

Tactic:
abel
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x x_1 x_2 : Unitization R A
simp :
  x.toProd.1 • x_2.toProd.2 + x_1.toProd.1 • x_2.toProd.2 + (x_2.toProd.1 • x.toProd.2 + x_2.toProd.1 • x_1.toProd.2) +
      (x.toProd.2 * x_2.toProd.2 + x_1.toProd.2 * x_2.toProd.2) =
    x.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x.toProd.2 + x.toProd.2 * x_2.toProd.2 +
      (x_1.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x_1.toProd.2 + x_1.toProd.2 * x_2.toProd.2)
⊢ ((x + x_1) * x_2).toProd.2 = (x * x_2 + x_1 * x_2).toProd.2

Tactic:
simp [smul_add, add_smul, add_mul]

Premises used: add_mul, add_smul, smul_add
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x x_1 x_2 : Unitization R A
⊢ x.toProd.1 • x_2.toProd.2 + x_1.toProd.1 • x_2.toProd.2 + (x_2.toProd.1 • x.toProd.2 + x_2.toProd.1 • x_1.toProd.2) +
      (x.toProd.2 * x_2.toProd.2 + x_1.toProd.2 * x_2.toProd.2) =
    x.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x.toProd.2 + x.toProd.2 * x_2.toProd.2 +
      (x_1.toProd.1 • x_2.toProd.2 + x_2.toProd.1 • x_1.toProd.2 + x_1.toProd.2 * x_2.toProd.2)

Tactic:
abel
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x : Unitization R A
⊢ (0 * x).toProd.2 = (toProd 0).2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
x : Unitization R A
⊢ (x * 0).toProd.2 = (toProd 0).2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : CommMonoid R
inst_1 : NonUnitalSemiring A
inst_2 : DistribMulAction R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x y z : Unitization R A
simp :
  (x.toProd.1 * y.toProd.1) • z.toProd.2 +
        ((x.toProd.1 * z.toProd.1) • y.toProd.2 + (y.toProd.1 * z.toProd.1) • x.toProd.2 +
          z.toProd.1 • (x.toProd.2 * y.toProd.2)) +
      (x.toProd.1 • (y.toProd.2 * z.toProd.2) + y.toProd.1 • (x.toProd.2 * z.toProd.2) +
        x.toProd.2 * (y.toProd.2 * z.toProd.2)) =
    (x.toProd.1 * y.toProd.1) • z.toProd.2 + (x.toProd.1 * z.toProd.1) • y.toProd.2 +
          x.toProd.1 • (y.toProd.2 * z.toProd.2) +
        (y.toProd.1 * z.toProd.1) • x.toProd.2 +
      (y.toProd.1 • (x.toProd.2 * z.toProd.2) + z.toProd.1 • (x.toProd.2 * y.toProd.2) +
        x.toProd.2 * (y.toProd.2 * z.toProd.2))
⊢ (x * y * z).toProd.2 = (x * (y * z)).toProd.2

Tactic:
simp only [snd_mul, fst_mul, smul_add, smul_smul, add_mul, smul_mul_assoc, mul_assoc, mul_add,
        mul_smul_comm, mul_comm z.fst x.fst, mul_comm z.fst y.fst]

Premises used: add_mul, Unitization.snd_mul, mul_assoc, Unitization.fst_mul, smul_smul, smul_mul_assoc, Prod.fst, Unitization.toProd, mul_comm, mul_smul_comm, mul_add, smul_add
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : CommMonoid R
inst_1 : NonUnitalSemiring A
inst_2 : DistribMulAction R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x y z : Unitization R A
⊢ (x.toProd.1 * y.toProd.1) • z.toProd.2 +
        ((x.toProd.1 * z.toProd.1) • y.toProd.2 + (y.toProd.1 * z.toProd.1) • x.toProd.2 +
          z.toProd.1 • (x.toProd.2 * y.toProd.2)) +
      (x.toProd.1 • (y.toProd.2 * z.toProd.2) + y.toProd.1 • (x.toProd.2 * z.toProd.2) +
        x.toProd.2 * (y.toProd.2 * z.toProd.2)) =
    (x.toProd.1 * y.toProd.1) • z.toProd.2 + (x.toProd.1 * z.toProd.1) • y.toProd.2 +
          x.toProd.1 • (y.toProd.2 * z.toProd.2) +
        (y.toProd.1 * z.toProd.1) • x.toProd.2 +
      (y.toProd.1 • (x.toProd.2 * z.toProd.2) + z.toProd.1 • (x.toProd.2 * y.toProd.2) +
        x.toProd.2 * (y.toProd.2 * z.toProd.2))

Tactic:
abel
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : CommMonoid R
inst_1 : NonUnitalCommSemiring A
inst_2 : DistribMulAction R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x x_1 : Unitization R A
⊢ (x * x_1).toProd.2 = (x_1 * x).toProd.2

Tactic:
simp [add_comm, mul_comm]

Premises used: add_comm, mul_comm
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : Star A
x : Unitization R A
⊢ (star x).toProd.1 = star x.toProd.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : Star A
x : Unitization R A
⊢ (star x).toProd.2 = star x.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : AddMonoid A
inst_2 : StarAddMonoid A
r : R
⊢ Eq.{u_2 + 1} (α := A) (toProd (inl (star r))).2 (toProd (star (inl r))).2

Tactic:
simp only [snd_star, star_zero, snd_inl]

Premises used: star_zero, Unitization.snd_star, Unitization.snd_inl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : AddMonoid R
inst_1 : StarAddMonoid R
inst_2 : Star A
a : A
⊢ Eq.{u_1 + 1} (α := R) (toProd (↑(star a) : Unitization R A)).1 (toProd (star (↑a : Unitization R A))).1

Tactic:
simp only [fst_star, star_zero, fst_inr]

Premises used: Unitization.fst_inr, star_zero, Unitization.fst_star
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid A
inst_3 : StarAddMonoid A
inst_4 : Module R A
inst_5 : StarModule R A
x : R
x_1 : Unitization R A
⊢ (star (x • x_1)).toProd.1 = (star x • star x_1).toProd.1

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid A
inst_3 : StarAddMonoid A
inst_4 : Module R A
inst_5 : StarModule R A
x : R
x_1 : Unitization R A
⊢ (star (x • x_1)).toProd.2 = (star x • star x_1).toProd.2

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
x y : Unitization R A
⊢ (star (x * y)).toProd.1 = (star y * star x).toProd.1

Tactic:
simp [-star_mul']

Premises used: star_mul'
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
x y : Unitization R A
⊢ (star (x * y)).toProd.2 = (star y * star x).toProd.2

Tactic:
simp [-star_mul', add_comm (star x.fst • star y.snd)]

Premises used: add_comm, Prod.fst, Unitization.toProd, HSMul.hSMul, star_mul', Prod.snd, Star.star
-- 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 : 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) (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)
⊢ 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:
change inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)

Premises used: Algebra.algebraMap, Unitization.inl, DFunLike.coe
-- 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 : 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
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)
⊢ 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)

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]

Premises used: add_mul, Unitization.inl_mul_inr, Algebra.algebraMap, Unitization.inl, Unitization.inl_mul_inl, Unitization.inr_mul_inl, mul_comm, mul_add, DFunLike.coe
-- 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 : 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) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R 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:
change _ = inl (algebraMap S R s) * _

Premises used: Algebra.algebraMap, Unitization.inl, DFunLike.coe
-- 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 : 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
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))
⊢ 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

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]

Premises used: Unitization.inl_mul_inr, Algebra.algebraMap, Unitization.inl, Unitization.inr_smul, Unitization.inl_mul_inl, Algebra.algebraMap_eq_smul_one, smul_one_smul, smul_one_mul, mul_add, Unitization.inl_smul, DFunLike.coe, smul_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 : 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
⊢ Eq (α := (a : S) → Unitization R A) (⇑(algebraMap S (Unitization R A)) : (a : S) → Unitization R A)
    (inl ∘ (⇑(algebraMap S R) : (a : S) → R))

Tactic:
rfl

Premises used: Unitization.inl, rfl
-- 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 : 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
⊢ Eq (α := S →+* Unitization R A) (algebraMap S (Unitization R A)) (RingHom.comp (inlRingHom R A) (algebraMap S R))

Tactic:
rfl

Premises used: rfl
-- 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 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := (a : R) → Unitization R A) (⇑(algebraMap R (Unitization R A)) : (a : R) → Unitization R A) inl

Tactic:
rfl

Premises used: Unitization.inl, rfl
-- 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 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := R →+* Unitization R A) (algebraMap R (Unitization R A)) (inlRingHom R A)

Tactic:
rfl

Premises used: Unitization.inl, Unitization.inlRingHom, rfl
-- 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
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)
⊢ φ = ψ

Tactic:
DFunLike.ext φ ψ (fun x ↦ ?_)

Premises used: DFunLike.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
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)
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 ↦ ?_)

Premises used: DFunLike.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
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
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)
⊢ Eq.{u_4 + 1} (α := B) ((φ : (a : Unitization R A) → B) x : B) ((ψ : (a : Unitization R A) → B) x : B)

Tactic:
induction x
-- 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
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)
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:
simp only [map_add, ← algebraMap_eq_inl, h, h']

Premises used: map_add, Unitization.algebraMap_eq_inl