[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
a : A
ha : a ∈ ↑s
⊢ ↑↑(AlgHom.comp (Subalgebra.val (Algebra.adjoin R ↑s)) (unitization s)) ↑{ val := a, property := ha } = a
[PROOFSTEP]
simp
[GOAL]
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
⊢ Function.Injective ↑(unitization s)
[PROOFSTEP]
refine' (injective_iff_map_eq_zero _).mpr fun x hx => _
[GOAL]
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx : ↑(unitization s) x = 0
⊢ x = 0
[PROOFSTEP]
induction' x using Unitization.ind with r a
[GOAL]
case h
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r + ↑a) = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
rw [map_add] at hx 
[GOAL]
case h
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
have hx' := congr_arg (Subtype.val : _ → A) hx
[GOAL]
case h
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a) = ↑0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
simp only [NonUnitalSubalgebra.unitization_apply_coe, Unitization.fst_inl, Subalgebra.coe_algebraMap,
  Unitization.snd_inl, ZeroMemClass.coe_zero, add_zero, map_neg, AddSubgroupClass.coe_neg, Unitization.fst_inr,
  map_zero, Unitization.snd_inr, Subalgebra.coe_add, zero_add] at hx' 
[GOAL]
case h
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r + ↑a = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
by_cases hr : r = 0
[GOAL]
case pos
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r + ↑a = 0
hr : r = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
simp only [hr, map_zero, Unitization.inl_zero, zero_add] at hx' ⊢
[GOAL]
case pos
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hr : r = 0
hx' : ↑a = 0
⊢ ↑a = 0
[PROOFSTEP]
rw [← ZeroMemClass.coe_zero s] at hx' 
[GOAL]
case pos
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hr : r = 0
hx' : ↑a = ↑0
⊢ ↑a = 0
[PROOFSTEP]
exact congr_arg _ (Subtype.coe_injective hx')
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r + ↑a = 0
hr : ¬r = 0
⊢ Unitization.inl r + ↑a = 0
[PROOFSTEP]
refine' False.elim (h1 _)
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r + ↑a = 0
hr : ¬r = 0
⊢ 1 ∈ s
[PROOFSTEP]
rw [← eq_sub_iff_add_eq, zero_sub] at hx' 
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hx' : ↑(algebraMap R A) r = -↑a
hr : ¬r = 0
⊢ 1 ∈ s
[PROOFSTEP]
replace hx' := congr_arg (fun y => r⁻¹ • y) hx'
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hr : ¬r = 0
hx' : (fun y => r⁻¹ • y) (↑(algebraMap R A) r) = (fun y => r⁻¹ • y) (-↑a)
⊢ 1 ∈ s
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, ← smul_assoc, smul_eq_mul, inv_mul_cancel hr, one_smul] at hx' 
[GOAL]
case neg
R✝¹ : Type u_1
S✝¹ : Type u_2
A✝¹ : Type u_3
inst✝¹¹ : CommSemiring R✝¹
inst✝¹⁰ : Semiring A✝¹
inst✝⁹ : Algebra R✝¹ A✝¹
inst✝⁸ : SetLike S✝¹ A✝¹
hSA✝¹ : NonUnitalSubsemiringClass S✝¹ A✝¹
hSRA✝¹ : SMulMemClass S✝¹ R✝¹ A✝¹
s✝¹ : S✝¹
R✝ : Type u_4
S✝ : Type u_5
A✝ : Type u_6
inst✝⁷ : Field R✝
inst✝⁶ : Ring A✝
inst✝⁵ : Algebra R✝ A✝
inst✝⁴ : SetLike S✝ A✝
hSA✝ : NonUnitalSubringClass S✝ A✝
hSRA✝ : SMulMemClass S✝ R✝ A✝
s✝ : S✝
R : Type u_7
S : Type u_8
A : Type u_9
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : ¬1 ∈ s
x : Unitization R { x // x ∈ s }
hx✝ : ↑(unitization s) x = 0
r : R
a : { x // x ∈ s }
hx : ↑(unitization s) (Unitization.inl r) + ↑(unitization s) ↑a = 0
hr : ¬r = 0
hx' : 1 = r⁻¹ • -↑a
⊢ 1 ∈ s
[PROOFSTEP]
exact hx'.symm ▸ SMulMemClass.smul_mem r⁻¹ (neg_mem a.prop)
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
S : Subsemiring R
⊢ NonUnitalSubsemiring.toSubsemiring (toNonUnitalSubsemiring S) (_ : 1 ∈ S) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
inst✝ : NonAssocSemiring R
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
⊢ NonUnitalSubsemiring.toSubsemiring
      (toNonUnitalSubsemiring { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ })
      (_ : 1 ∈ { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
S : NonUnitalSubsemiring R
h1 : 1 ∈ S
⊢ Subsemiring.toNonUnitalSubsemiring (toSubsemiring S h1) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
inst✝ : NonAssocSemiring R
toAddSubmonoid✝ : AddSubmonoid R
mul_mem'✝ : ∀ {a b : R}, a ∈ toAddSubmonoid✝.carrier → b ∈ toAddSubmonoid✝.carrier → a * b ∈ toAddSubmonoid✝.carrier
h1 : 1 ∈ { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ }
⊢ Subsemiring.toNonUnitalSubsemiring (toSubsemiring { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ } h1) =
    { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R✝ : Type u_1
inst✝¹ : NonAssocSemiring R✝
R : Type u_2
inst✝ : Semiring R
S : NonUnitalSubsemiring R
⊢ Function.Surjective ↑(unitization S)
[PROOFSTEP]
simpa [unitization, AlgEquiv.arrowCongr] using
  NonUnitalSubalgebra.unitization_surjective (hSRA := AddSubmonoidClass.nsmulMemClass) S
[GOAL]
R : Type u_1
inst✝ : Ring R
S : Subring R
⊢ NonUnitalSubring.toSubring (toNonUnitalSubring S) (_ : 1 ∈ S) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
⊢ NonUnitalSubring.toSubring (toNonUnitalSubring { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ })
      (_ : 1 ∈ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }) =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Ring R
S : NonUnitalSubring R
h1 : 1 ∈ S
⊢ Subring.toNonUnitalSubring (toSubring S h1) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
inst✝ : Ring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ Subring.toNonUnitalSubring
      (toSubring { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } h1) =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Ring R
S : NonUnitalSubring R
⊢ Function.Surjective ↑(unitization S)
[PROOFSTEP]
simpa [unitization, AlgEquiv.arrowCongr] using
  NonUnitalSubalgebra.unitization_surjective (hSRA := AddSubgroupClass.zsmulMemClass) S
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ NonUnitalSubalgebra.toSubalgebra (toNonUnitalSubalgebra S) (_ : 1 ∈ S) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), ↑(algebraMap R A) r ∈ toSubsemiring✝.carrier
⊢ NonUnitalSubalgebra.toSubalgebra
      (toNonUnitalSubalgebra { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ })
      (_ : 1 ∈ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }) =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
⊢ Subalgebra.toNonUnitalSubalgebra (toSubalgebra S h1) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ Subalgebra.toNonUnitalSubalgebra
      (toSubalgebra { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ } h1) =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : StarSubalgebra R A
⊢ NonUnitalStarSubalgebra.toStarSubalgebra (toNonUnitalStarSubalgebra S) (_ : 1 ∈ S.carrier) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toSubalgebra✝ : Subalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toSubalgebra✝.carrier → star a ∈ toSubalgebra✝.carrier
⊢ NonUnitalStarSubalgebra.toStarSubalgebra
      (toNonUnitalStarSubalgebra { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ })
      (_ :
        1 ∈
          { toSubalgebra := toSubalgebra✝,
                      star_mem' := star_mem'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) =
    { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h1 : 1 ∈ S
⊢ StarSubalgebra.toNonUnitalStarSubalgebra (toStarSubalgebra S h1) = S
[PROOFSTEP]
cases S
[GOAL]
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h1 : 1 ∈ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
⊢ StarSubalgebra.toNonUnitalStarSubalgebra
      (toStarSubalgebra { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ } h1) =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
a : A
ha : a ∈ ↑S
⊢ ↑↑(StarAlgHom.comp (StarSubalgebra.subtype (StarSubalgebra.adjoin R ↑S)) (unitization S)).toAlgHom
      ↑{ val := a, property := ha } =
    a
[PROOFSTEP]
simp
