awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
⊢ SMulMemClass S ℤ R

Tactic:
have := AddSubgroupClass.zsmulMemClass (S := S)
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
this : SMulMemClass S ℤ R
rw :
  Eq (α := Subalgebra ℤ R)
    (AlgHom.range (A := Unitization ℤ ↥s) (NonUnitalSubalgebra.unitization s : Unitization ℤ ↥s →ₐ[ℤ] R))
    (subalgebraOfSubring (Subring.closure (↑s : Set R)))
rw₁ : Eq (α := Subalgebra ℤ R) (Algebra.adjoin ℤ (↑s : Set R)) (subalgebraOfSubring (Subring.closure (↑s : Set R)))
rw₂ rw₃ :
  Eq (α := Subalgebra ℤ R) (subalgebraOfSubring (Subring.closure (↑s : Set R)))
    (subalgebraOfSubring (Subring.closure (↑s : Set R)))
⊢ Eq (α := Subalgebra ℤ R) (AlgHom.range (A := Unitization ℤ ↥s) (unitization s))
    (subalgebraOfSubring (Subring.closure (↑s : Set R)))

Tactic:
rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_int]

Premises used: NonUnitalSubalgebra.unitization_range, Algebra.adjoin_int, NonUnitalSubring.unitization
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
⊢ StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S ↔
    NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
refine_1 :
  ∀ (h : StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S),
    NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
refine_2 :
  ∀ (h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra),
    StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S
⊢ StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S ↔
    NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S
x : A
⊢ Eq.{u_3 + 1} (α := C)
    ((AlgHom.toRingHom (R := R)
            (↑((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) : Unitization R A →ₐ[R] C) :
          (a : Unitization R A) → C)
        (↑x : Unitization R A) :
      C)
    ((f : (a : A) → C) x : C)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ S
x : A
⊢ Membership.mem (α := C) S.toNonUnitalStarSubalgebra
    (((↑(NonUnitalAlgHomClass.toNonUnitalAlgHom f) : A →ₙ+* C) : (a : A) → C) x : C)

Tactic:
exact @h (f x) ⟨x, by simp⟩

Premises used: Unitization.inr, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
r : R
a : A
⊢ Membership.mem (α := C) S
    ((AlgHom.toRingHom (R := R)
            (↑((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) : Unitization R A →ₐ[R] C) :
          (a : Unitization R A) → C)
        (inl r + (↑a : Unitization R A)) :
      C)

Tactic:
simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)

Premises used: algebraMap_mem, Exists.intro, AddMemClass.add_mem, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
x : Unitization R A
refine_2 :
  ∀ (r : R) (a : A),
    Membership.mem (α := C) S
      ((AlgHom.toRingHom (R := R)
              (↑((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) : Unitization R A →ₐ[R] C) :
            (a : Unitization R A) → C)
          (inl r + (↑a : Unitization R A)) :
        C)
⊢ Membership.mem (α := C) S
    ((AlgHom.toRingHom (R := R)
            (↑((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) : Unitization R A →ₐ[R] C) :
          (a : Unitization R A) → C)
        x :
      C)

Tactic:
induction x with
    | _ r a => simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
c : StarSubalgebra R C
rw : NonUnitalStarAlgHom.range f ≤ c.toNonUnitalStarSubalgebra ↔ (↑(NonUnitalStarAlgHom.range f) : Set C) ⊆ (↑c : Set C)
⊢ StarAlgHom.range (A := Unitization R A) ((starLift : (a : A →⋆ₙₐ[R] C) → Unitization R A →⋆ₐ[R] C) f) ≤ c ↔
    StarAlgebra.adjoin R (↑(NonUnitalStarAlgHom.range f) : Set C) ≤ c

Tactic:
rw [starLift_range_le, StarAlgebra.adjoin_le_iff]

Premises used: StarAlgebra.adjoin_le_iff, Unitization.starLift_range_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing R
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : StarModule R A
inst_8 : Semiring C
inst_9 : StarRing C
inst_10 : Algebra R C
inst_11 : StarModule R C
f : A →⋆ₙₐ[R] C
c : StarSubalgebra R C
⊢ NonUnitalStarAlgHom.range f ≤ c.toNonUnitalStarSubalgebra ↔ (↑(NonUnitalStarAlgHom.range f) : Set C) ⊆ (↑c : Set C)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
x : Unitization.{u_1, u_3} R ↥s
⊢ (unitization s : (a : Unitization R ↥s) → A) x =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.toProd.1 : A) (↑x.toProd.2 : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
rw :
  Eq (α := StarSubalgebra R A)
    (StarAlgebra.adjoin R
      (↑(NonUnitalStarAlgHom.range (F := ↥s →⋆ₙₐ[R] A) (NonUnitalStarSubalgebraClass.subtype s)) : Set A))
    (StarAlgebra.adjoin R (↑s : Set A))
⊢ Eq (α := StarSubalgebra R A) (StarAlgHom.range (A := Unitization.{u_1, u_3} R ↥s) (unitization s))
    (StarAlgebra.adjoin R (↑s : Set A))

Tactic:
rw [unitization, Unitization.starLift_range]

Premises used: Unitization.starLift_range, NonUnitalStarSubalgebra.unitization
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
simp : Eq (α := StarSubalgebra R A) (StarAlgebra.adjoin R {x : A | x ∈ s}) (StarAlgebra.adjoin R (↑s : Set A))
⊢ Eq (α := StarSubalgebra R A)
    (StarAlgebra.adjoin R
      (↑(NonUnitalStarAlgHom.range (F := ↥s →⋆ₙₐ[R] A) (NonUnitalStarSubalgebraClass.subtype s)) : Set A))
    (StarAlgebra.adjoin R (↑s : Set A))

Tactic:
simp only [NonUnitalStarAlgHom.coe_range, NonUnitalStarSubalgebraClass.coe_subtype,
    Subtype.range_coe_subtype]

Premises used: NonUnitalStarSubalgebraClass.coe_subtype, Subtype.range_coe_subtype, NonUnitalStarAlgHom.coe_range
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
⊢ Eq (α := StarSubalgebra R A) (StarAlgebra.adjoin R {x : A | x ∈ s}) (StarAlgebra.adjoin R (↑s : Set A))

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
x : ↥s
⊢ (unitization s : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
⊢ Function.Bijective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))

Tactic:
⟨?_, fun x ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
refine_1 :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))
refine_2 :
  ∀ (x : ↥(StarAlgebra.adjoin R (↑s : Set A))),
    ∃ (a : Unitization.{u_1, u_3} R ↥s),
      (starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))) a = x
⊢ Function.Bijective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))

Tactic:
refine ⟨?_, fun x ↦ ?_⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
x : ↥s
⊢ (StarAlgHom.comp (StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) starAlgHom : (a : Unitization R ↥s) → A)
      (↑x : Unitization R ↥s) =
    (↑x : A)

Tactic:
simp [starAlgHom]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) starAlgHom) :
      (a : Unitization R ↥s) → A)

Tactic:
have := AlgHomClass.unitization_injective s h1 ((StarSubalgebra.subtype _).comp starAlgHom)
        fun _ ↦ by simp [starAlgHom]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
this :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) starAlgHom) :
      (a : Unitization R ↥s) → A)
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (Function.comp (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
      (⇑(StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) : (a : ↥(StarAlgebra.adjoin R (↑s : Set A))) → A)
      (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))))

Tactic:
rw [StarAlgHom.coe_comp] at this

Premises used: StarAlgHom.coe_comp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
this :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (Function.comp (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
      (⇑(StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) : (a : ↥(StarAlgebra.adjoin R (↑s : Set A))) → A)
      (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))))
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))

Tactic:
this.of_comp

Premises used: Function.Injective.of_comp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
this :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (Function.comp (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
      (⇑(StarSubalgebra.subtype (StarAlgebra.adjoin R (↑s : Set A))) : (a : ↥(StarAlgebra.adjoin R (↑s : Set A))) → A)
      (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))))
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(StarAlgebra.adjoin R (↑s : Set A)))
    (⇑starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A)))

Tactic:
exact this.of_comp

Premises used: Function.Injective.of_comp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
x : ↥(StarAlgebra.adjoin R (↑s : Set A))
refine_2 :
  ∀ (a : Unitization.{u_1, u_3} R ↥s)
    (ha : (AlgHom.toRingHom (↑(unitization s) : Unitization R ↥s →ₐ[R] A) : (a : Unitization R ↥s) → A) a = (↑x : A)),
    ∃ (a : Unitization.{u_1, u_3} R ↥s),
      (starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))) a = x
⊢ ∃ (a : Unitization.{u_1, u_3} R ↥s),
    (starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))) a = x

Tactic:
obtain (⟨a, ha⟩ : (x : A) ∈ (unitization s).range) :=
        (unitization_range s).ge x.property

Premises used: StarAlgHom.range, Eq.ge, NonUnitalStarSubalgebra.unitization_range, NonUnitalStarSubalgebra.unitization, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
x : ↥(StarAlgebra.adjoin R (↑s : Set A))
a : Unitization.{u_1, u_3} R ↥s
ha : (AlgHom.toRingHom (↑(unitization s) : Unitization R ↥s →ₐ[R] A) : (a : Unitization R ↥s) → A) a = (↑x : A)
⊢ ∃ (a : Unitization.{u_1, u_3} R ↥s),
    (starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))) a = x

Tactic:
⟨a, Subtype.ext ha⟩

Premises used: Exists.intro, Subtype.ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : StarRing R
inst_2 : Ring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst_7 : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization.{u_1, u_3} R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R (↑s : Set A)) :=
  StarAlgHom.codRestrict (unitization s) (StarAlgebra.adjoin R (↑s : Set A)) ⋯
x : ↥(StarAlgebra.adjoin R (↑s : Set A))
a : Unitization.{u_1, u_3} R ↥s
ha : (AlgHom.toRingHom (↑(unitization s) : Unitization R ↥s →ₐ[R] A) : (a : Unitization R ↥s) → A) a = (↑x : A)
⊢ ∃ (a : Unitization.{u_1, u_3} R ↥s),
    (starAlgHom : (a : Unitization R ↥s) → ↥(StarAlgebra.adjoin R (↑s : Set A))) a = x

Tactic:
exact ⟨a, Subtype.ext ha⟩
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
a : A
⊢ Eq.{v₁ + 1} (α := (a : M) → M) (⇑((lsmul R B M : (a : A) → Module.End B M) a : Module.End B M) : (a : M) → M)
    fun (x : M) ↦ a • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
B : Type u₁
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
a : A
m : M
⊢ (((lsmul R B M : (a : A) → Module.End B M) a : Module.End B M) : (a : M) → M) m = a • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
a : A
⊢ (lsmul R R M : (a : A) → Module.End R M) a = HSMul.hSMul (β := Module.End R M) a 1

Tactic:
rfl

Premises used: DistribSMul.toLinearMap, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : MulAction A M
inst_4 : SMul R M
inst_5 : IsScalarTower R A M
r : R
x : M
rw : HSMul.hSMul (β := A) r 1 • x = r • x
rw₁ : r • HSMul.hSMul.{w, v₁, v₁} (α := A) 1 x = r • x
rw₂ rw₃ : r • x = r • x
⊢ HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x

Tactic:
rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Premises used: one_smul, Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : MulAction A M
inst_4 : SMul R M
h : ∀ (r : R) (x : M), HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) x = r • x
r : R
a : A
x : M
rw : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a • x = r • a • x
rw₁ : HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) (a • x) = r • a • x
rw₂ rw₃ : r • a • x = r • a • x
⊢ (r • a) • x = r • a • x

Tactic:
rw [Algebra.smul_def, mul_smul, h]

Premises used: Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : MulAction A M
⊢ IsScalarTower R A M

Tactic:
letI := MulAction.compHom M (algebraMap R A : R →* A); of_algebraMap_smul fun _ _ ↦ rfl

Premises used: IsScalarTower.of_algebraMap_smul, rfl