awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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:
simp [NonUnitalAlgHomClass.toNonUnitalAlgHom]

Premises used: NonUnitalAlgHomClass.toNonUnitalAlgHom
-- 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
φ : Unitization R A →ₐ[R] C
h :
  ∀ (x : A),
    Eq.{u_5 + 1} (α := C)
      ((NonUnitalAlgHom.comp
              (↑(NonUnitalAlgHom.toAlgHom
                    ((fun (φ : Unitization R A →ₐ[R] C) ↦ (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A))
                      φ)) :
                Unitization R A →ₙₐ[R] C)
              (inrNonUnitalAlgHom R A) :
            (a : A) → C)
          x :
        C)
      (((↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A) : (a : A) → C) x : C)
⊢ NonUnitalAlgHom.toAlgHom
      ((fun (φ : Unitization R A →ₐ[R] C) ↦ (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A)) φ) =
    φ

Tactic:
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
φ : Unitization R A →ₐ[R] C
x : A
⊢ Eq.{u_5 + 1} (α := C)
    ((NonUnitalAlgHom.comp
            (↑(NonUnitalAlgHom.toAlgHom
                  ((fun (φ : Unitization R A →ₐ[R] C) ↦ (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A))
                    φ)) :
              Unitization R A →ₙₐ[R] C)
            (inrNonUnitalAlgHom R A) :
          (a : A) → C)
        x :
      C)
    (((↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A) : (a : A) → C) x : C)

Tactic:
simp [NonUnitalAlgHomClass.toNonUnitalAlgHom]

Premises used: NonUnitalAlgHomClass.toNonUnitalAlgHom
-- 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
a : A
⊢ Eq.{u_5 + 1} (α := C)
    ((((Equiv.symm lift : (a : Unitization R A →ₐ[R] C) → A →ₙₐ[R] C) φ : A →ₙₐ[R] C) : (a : A) → C) a : C)
    ((φ : (a : Unitization R A) → C) (↑a : Unitization R A) : C)

Tactic:
rfl

Premises used: Unitization.inr, 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 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
h : ∀ (x : Unitization R A), (NonUnitalAlgHom.toAlgHom 0 : (a : Unitization R A) → R) x = x.toProd.1
⊢ Eq (α := (a : Unitization R A) → R) (⇑(NonUnitalAlgHom.toAlgHom 0) : (a : Unitization R A) → R)
    fun (x : Unitization R A) ↦ x.toProd.1

Tactic:
ext
-- 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
x : Unitization R A
⊢ (NonUnitalAlgHom.toAlgHom 0 : (a : Unitization R A) → R) x = x.toProd.1

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
φ ψ : Unitization R A →⋆ₐ[R] C
h :
  Eq (α := A →⋆ₙₐ[R] C) (NonUnitalStarAlgHom.comp (↑φ : Unitization R A →⋆ₙₐ[R] C) (inrNonUnitalStarAlgHom R A))
    (NonUnitalStarAlgHom.comp (↑ψ : Unitization R A →⋆ₙₐ[R] C) (inrNonUnitalStarAlgHom R A))
⊢ φ = ψ

Tactic:
Unitization.algHom_ext'' <| DFunLike.congr_fun h

Premises used: DFunLike.congr_fun, Unitization.algHom_ext''
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
inst_10 : StarModule R C
φ : A →⋆ₙₐ[R] C
x : Unitization R A
⊢ Eq.{u_3 + 1} (α := C)
    (OneHom.toFun
      (↑(↑(AlgHom.toRingHom (R := R) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom)) :
            Unitization R A →* C) :
        OneHom (Unitization R A) C)
      (star x))
    (star
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := R) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom)) :
              Unitization R A →* C) :
          OneHom (Unitization R A) C)
        x))

Tactic:
simp [map_star]

Premises used: StarHomClass.map_star
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
inst_10 : StarModule R C
x : A →⋆ₙₐ[R] C
h :
  ∀ (x_1 : A),
    Eq.{u_3 + 1} (α := C)
      (((fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
              ((fun (φ : A →⋆ₙₐ[R] C) ↦
                  let __AlgHom : Unitization R A →ₐ[R] C :=
                    (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
                  ({ toAlgHom := __AlgHom, map_star' := ⋯ } : Unitization R A →⋆ₐ[R] C))
                x) :
            (a : A) → C)
          x_1 :
        C)
      ((x : (a : A) → C) x_1 : C)
⊢ (fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
      ((fun (φ : A →⋆ₙₐ[R] C) ↦
          let __AlgHom : Unitization R A →ₐ[R] C :=
            (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
          ({ toAlgHom := __AlgHom, map_star' := ⋯ } : Unitization R A →⋆ₐ[R] C))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
inst_10 : StarModule R C
x : A →⋆ₙₐ[R] C
x_1 : A
⊢ Eq.{u_3 + 1} (α := C)
    (((fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
            ((fun (φ : A →⋆ₙₐ[R] C) ↦
                let __AlgHom : Unitization R A →ₐ[R] C :=
                  (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
                ({ toAlgHom := __AlgHom, map_star' := ⋯ } : Unitization R A →⋆ₐ[R] C))
              x) :
          (a : A) → C)
        x_1 :
      C)
    ((x : (a : A) → C) x_1 : C)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
inst_10 : StarModule R C
x : Unitization R A →⋆ₐ[R] C
h :
  ∀ (x_1 : A),
    Eq.{u_3 + 1} (α := C)
      ((NonUnitalStarAlgHom.comp
              (↑((fun (φ : A →⋆ₙₐ[R] C) ↦
                      let __AlgHom : Unitization R A →ₐ[R] C :=
                        (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
                      ({ toAlgHom := __AlgHom, map_star' := ⋯ } : Unitization R A →⋆ₐ[R] C))
                    ((fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
                      x)) :
                Unitization R A →⋆ₙₐ[R] C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → C)
          x_1 :
        C)
      ((NonUnitalStarAlgHom.comp (↑x : Unitization R A →⋆ₙₐ[R] C) (inrNonUnitalStarAlgHom R A) : (a : A) → C) x_1 : C)
⊢ (fun (φ : A →⋆ₙₐ[R] C) ↦
        let __AlgHom : Unitization R A →ₐ[R] C :=
          (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
        ({ toAlgHom := __AlgHom, map_star' := ⋯ } : Unitization R A →⋆ₐ[R] C))
      ((fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A)) x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
inst_10 : StarModule R C
x : Unitization R A →⋆ₐ[R] C
x_1 : A
⊢ Eq.{u_3 + 1} (α := C)
    ((NonUnitalStarAlgHom.comp
            (↑((fun (φ : A →⋆ₙₐ[R] C) ↦
                    let __AlgHom : Unitization R A →ₐ[R] C :=
                      (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
                    ({ toAlgHom := __AlgHom, map_star' := ⋯ } : Unitization R A →⋆ₐ[R] C))
                  ((fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
                    x)) :
              Unitization R A →⋆ₙₐ[R] C)
            (inrNonUnitalStarAlgHom R A) :
          (a : A) → C)
        x_1 :
      C)
    ((NonUnitalStarAlgHom.comp (↑x : Unitization R A →⋆ₙₐ[R] C) (inrNonUnitalStarAlgHom R A) : (a : A) → C) x_1 : C)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
inst_10 : StarModule R C
φ : Unitization R A →⋆ₐ[R] C
a : A
⊢ Eq.{u_3 + 1} (α := C)
    ((((Equiv.symm starLift : (a : Unitization R A →⋆ₐ[R] C) → A →⋆ₙₐ[R] C) φ : A →⋆ₙₐ[R] C) : (a : A) → C) a : C)
    ((φ : (a : Unitization R A) → C) (↑a : Unitization R A) : C)

Tactic:
rfl

Premises used: Unitization.inr, rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
a : A
⊢ Eq (α := Unitization R B)
    ((starMap φ : (a : Unitization R A) → Unitization R B) (↑a : Unitization R A) : Unitization R B)
    ((↑((φ : (a : A) → B) a) : Unitization R B) : Unitization R B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
r : R
⊢ Eq (α := Unitization R B) ((starMap φ : (a : Unitization R A) → Unitization R B) (inl r) : Unitization R B)
    ((algebraMap R (Unitization R B) : (a : R) → Unitization R B) r : Unitization R B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
x y : Unitization R A
h :
  Eq (α := Unitization R B) ((starMap φ : (a : Unitization R A) → Unitization R B) x : Unitization R B)
    ((starMap φ : (a : Unitization R A) → Unitization R B) y : Unitization R B)
fst : x.toProd.1 = y.toProd.1
snd : x.toProd.2 = y.toProd.2
⊢ x = y

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
x y : Unitization R A
h :
  Eq (α := Unitization R B) ((starMap φ : (a : Unitization R A) → Unitization R B) x : Unitization R B)
    ((starMap φ : (a : Unitization R A) → Unitization R B) y : Unitization R B)
⊢ x.toProd.1 = y.toProd.1

Tactic:
simpa using congr($(h).fst)
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
x y : Unitization R A
h :
  Eq (α := Unitization R B) ((starMap φ : (a : Unitization R A) → Unitization R B) x : Unitization R B)
    ((starMap φ : (a : Unitization R A) → Unitization R B) y : Unitization R B)
⊢ Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) x.toProd.2 : B) ((φ : (a : A) → B) y.toProd.2 : B)

Tactic:
simpa [algebraMap_eq_inl] using congr($(h).snd)

Premises used: Unitization.algebraMap_eq_inl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
x y : Unitization R A
h :
  Eq (α := Unitization R B) ((starMap φ : (a : Unitization R A) → Unitization R B) x : Unitization R B)
    ((starMap φ : (a : Unitization R A) → Unitization R B) y : Unitization R B)
⊢ x.toProd.2 = y.toProd.2

Tactic:
exact hφ <| by simpa [algebraMap_eq_inl] using congr($(h).snd)
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
r : R
b : B
inl_add_inr :
  ∀ (a : A),
    ∃ (a_1 : Unitization R A),
      (starMap φ : (a : Unitization R A) → Unitization R B) a_1 =
        HAdd.hAdd (α := Unitization R B) (β := Unitization R B) (inl r : Unitization R B)
          ((↑((φ : (a : A) → B) a) : Unitization R B) : Unitization R B)
⊢ ∃ (a : Unitization R A), (starMap φ : (a : Unitization R A) → Unitization R B) a = inl r + (↑b : Unitization R B)

Tactic:
obtain ⟨a, rfl⟩ := hφ b

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
r : R
a : A
⊢ (starMap φ : (a : Unitization R A) → Unitization R B) (mk (r, a)) =
    HAdd.hAdd (α := Unitization R B) (β := Unitization R B) (inl r : Unitization R B)
      ((↑((φ : (a : A) → B) a) : Unitization R B) : Unitization R B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
r : R
a : A
⊢ ∃ (a_1 : Unitization R A),
    (starMap φ : (a : Unitization R A) → Unitization R B) a_1 =
      HAdd.hAdd (α := Unitization R B) (β := Unitization R B) (inl r : Unitization R B)
        ((↑((φ : (a : A) → B) a) : Unitization R B) : Unitization R B)

Tactic:
exact ⟨mk (r, a), by rfl⟩
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
x : Unitization R B
inl_add_inr :
  ∀ (r : R) (b : B),
    ∃ (a : Unitization R A), (starMap φ : (a : Unitization R A) → Unitization R B) a = inl r + (↑b : Unitization R B)
⊢ ∃ (a : Unitization R A), (starMap φ : (a : Unitization R A) → Unitization R B) a = x

Tactic:
induction x using Unitization.ind with
  | inl_add_inr r b =>
    obtain ⟨a, rfl⟩ := hφ b
    exact ⟨mk (r, a), by rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : NonUnitalSemiring C
inst_13 : StarRing C
inst_14 : Module R C
inst_15 : SMulCommClass R C C
inst_16 : IsScalarTower R C C
inst_17 : StarModule R B
inst_18 : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
h :
  ∀ (x : A),
    Eq.{u_1 + 1} (α := R)
      (toProd
          ((NonUnitalStarAlgHom.comp (↑(starMap (ψ.comp φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
                (inrNonUnitalStarAlgHom R A) :
              (a : A) → Unitization R C)
            x)).1
      (toProd
          ((NonUnitalStarAlgHom.comp
                (↑(StarAlgHom.comp (starMap ψ) (starMap φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
                (inrNonUnitalStarAlgHom R A) :
              (a : A) → Unitization R C)
            x)).1
h₁ :
  ∀ (x : A),
    Eq.{u_4 + 1} (α := C)
      (toProd
          ((NonUnitalStarAlgHom.comp (↑(starMap (ψ.comp φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
                (inrNonUnitalStarAlgHom R A) :
              (a : A) → Unitization R C)
            x)).2
      (toProd
          ((NonUnitalStarAlgHom.comp
                (↑(StarAlgHom.comp (starMap ψ) (starMap φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
                (inrNonUnitalStarAlgHom R A) :
              (a : A) → Unitization R C)
            x)).2
⊢ Eq (α := Unitization R A →⋆ₐ[R] Unitization R C) (starMap (ψ.comp φ)) (StarAlgHom.comp (starMap ψ) (starMap φ))

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : NonUnitalSemiring C
inst_13 : StarRing C
inst_14 : Module R C
inst_15 : SMulCommClass R C C
inst_16 : IsScalarTower R C C
inst_17 : StarModule R B
inst_18 : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
x : A
⊢ Eq.{u_1 + 1} (α := R)
    (toProd
        ((NonUnitalStarAlgHom.comp (↑(starMap (ψ.comp φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → Unitization R C)
          x)).1
    (toProd
        ((NonUnitalStarAlgHom.comp
              (↑(StarAlgHom.comp (starMap ψ) (starMap φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → Unitization R C)
          x)).1

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : NonUnitalSemiring C
inst_13 : StarRing C
inst_14 : Module R C
inst_15 : SMulCommClass R C C
inst_16 : IsScalarTower R C C
inst_17 : StarModule R B
inst_18 : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
x : A
⊢ Eq.{u_4 + 1} (α := C)
    (toProd
        ((NonUnitalStarAlgHom.comp (↑(starMap (ψ.comp φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → Unitization R C)
          x)).2
    (toProd
        ((NonUnitalStarAlgHom.comp
              (↑(StarAlgHom.comp (starMap ψ) (starMap φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → Unitization R C)
          x)).2

Tactic:
simp