awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
rw :
  Eq (α := Subalgebra R A)
    (Algebra.adjoin R
      (↑(NonUnitalAlgHom.range (F := ↥s →ₙₐ[R] A) (A := ↥s) (NonUnitalSubalgebraClass.subtype s)) : Set A))
    (Algebra.adjoin R (↑s : Set A))
⊢ Eq (α := Subalgebra R A) (AlgHom.range (A := Unitization.{u_1, u_3} R ↥s) (unitization s))
    (Algebra.adjoin R (↑s : Set A))

Tactic:
rw [unitization, Unitization.lift_range]

Premises used: Unitization.lift_range, NonUnitalSubalgebra.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 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ Eq (α := Subalgebra R A)
    (Algebra.adjoin R
      (↑(NonUnitalAlgHom.range (F := ↥s →ₙₐ[R] A) (A := ↥s) (NonUnitalSubalgebraClass.subtype s)) : Set A))
    (Algebra.adjoin R (↑s : Set A))

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
⊢ Function.Injective (α := Unitization.{u_2, u_4} R ↥s) (β := A) (⇑f : (a : Unitization R ↥s) → A)

Tactic:
(injective_iff_map_eq_zero f).mpr fun x hx => ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
refine :
  ∀ (x : Unitization.{u_2, u_4} R ↥s) (hx : Eq.{u_4 + 1} (α := A) ((f : (a : Unitization R ↥s) → A) x : A) (0 : A)),
    x = 0
⊢ Function.Injective (α := Unitization.{u_2, u_4} R ↥s) (β := A) (⇑f : (a : Unitization R ↥s) → A)

Tactic:
refine (injective_iff_map_eq_zero f).mpr fun x hx => ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
a : ↥s
hx : Eq.{u_4 + 1} (α := A) ((f : (a : Unitization R ↥s) → A) (Unitization.inl r + (↑a : Unitization R ↥s)) : A) (0 : A)
⊢ HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (↑a : A) = 0

Tactic:
simp_rw [map_add, hf, ← Unitization.algebraMap_eq_inl, AlgHomClass.commutes] at hx

Premises used: map_add, Unitization.algebraMap_eq_inl, AlgHomClass.commutes
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
a : ↥s
hx : HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (↑a : A) = 0
inl_add_inr : ∀ (hx : (algebraMap R A : (a : R) → A) r = -(↑a : A)), Unitization.inl r = -(↑a : Unitization R ↥s)
⊢ Unitization.inl r + (↑a : Unitization R ↥s) = 0

Tactic:
rw [add_eq_zero_iff_eq_neg] at hx ⊢

Premises used: add_eq_zero_iff_eq_neg
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
a : ↥s
hx : (algebraMap R A : (a : R) → A) r = -(↑a : A)
pos : ∀ (hr : r = 0), Unitization.inl r = -(↑a : Unitization R ↥s)
neg : ∀ (hr : ¬r = 0), Unitization.inl r = -(↑a : Unitization R ↥s)
⊢ Unitization.inl r = -(↑a : Unitization R ↥s)

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
a : ↥s
hx : (algebraMap R A : (a : R) → A) r = -(↑a : A)
hr : r = 0
pos : (Unitization.toProd (Unitization.inl r)).1 = (Unitization.toProd (-(↑a : Unitization R ↥s))).1
pos₁ : (↑(Unitization.toProd (Unitization.inl r)).2 : A) = (↑(Unitization.toProd (-(↑a : Unitization R ↥s))).2 : A)
⊢ Unitization.inl r = -(↑a : Unitization R ↥s)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
a : ↥s
hx : (algebraMap R A : (a : R) → A) r = -(↑a : A)
hr : r = 0
⊢ (Unitization.toProd (Unitization.inl r)).1 = (Unitization.toProd (-(↑a : Unitization R ↥s))).1

Tactic:
simp [hr]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
a : ↥s
hx : (algebraMap R A : (a : R) → A) r = -(↑a : A)
hr : r = 0
⊢ (↑(Unitization.toProd (Unitization.inl r)).2 : A) = (↑(Unitization.toProd (-(↑a : Unitization R ↥s))).2 : A)

Tactic:
simpa [hr] using hx
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
a : ↥s
hx : (algebraMap R A : (a : R) → A) r = -(↑a : A)
hr : ¬r = 0
⊢ Unitization.inl r = -(↑a : Unitization R ↥s)

Tactic:
(h r hr <| hx ▸ (neg_mem a.property)).elim

Premises used: False.elim, Eq.rec, Eq.symm, Subtype.property, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
a : ↥s
hx : (algebraMap R A : (a : R) → A) r = -(↑a : A)
hr : ¬r = 0
⊢ Unitization.inl r = -(↑a : Unitization R ↥s)

Tactic:
exact (h r hr <| hx ▸ (neg_mem a.property)).elim

Premises used: False.elim, Eq.rec, Eq.symm, Subtype.property, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → ((algebraMap R A : (a : R) → A) r : A) ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
x : Unitization.{u_2, u_4} R ↥s
hx : Eq.{u_4 + 1} (α := A) ((f : (a : Unitization R ↥s) → A) x : A) (0 : A)
inl_add_inr :
  ∀ (r : R) (a : ↥s)
    (hx :
      Eq.{u_4 + 1} (α := A) ((f : (a : Unitization R ↥s) → A) (Unitization.inl r + (↑a : Unitization R ↥s)) : A)
        (0 : A)),
    Unitization.inl r + (↑a : Unitization R ↥s) = 0
⊢ x = 0

Tactic:
induction x with
  | inl_add_inr r a =>
    simp_rw [map_add, hf, ← Unitization.algebraMap_eq_inl, AlgHomClass.commutes] at hx
    rw [add_eq_zero_iff_eq_neg] at hx ⊢
    by_cases hr : r = 0
    · ext
      · simp [hr]
      · simpa [hr] using hx
    · exact (h r hr <| hx ▸ (neg_mem a.property)).elim

Premises used: map_add, add_eq_zero_iff_eq_neg, Unitization.algebraMap_eq_inl, AlgHomClass.commutes
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : Field R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
⊢ Function.Injective (α := Unitization.{u_2, u_4} R ↥s) (β := A) (⇑f : (a : Unitization R ↥s) → A)

Tactic:
AlgHomClass.unitization_injective' s (fun r hr hr' ↦ ?_) f hf

Premises used: AlgHomClass.unitization_injective'
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : Field R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
refine :
  ∀ (r : R) (hr : r ≠ 0) (hr' : Membership.mem.{u_4, u_3} (α := A) s ((algebraMap R A : (a : R) → A) r : A)), False
⊢ Function.Injective (α := Unitization.{u_2, u_4} R ↥s) (β := A) (⇑f : (a : Unitization R ↥s) → A)

Tactic:
refine AlgHomClass.unitization_injective' s (fun r hr hr' ↦ ?_) f hf

Premises used: AlgHomClass.unitization_injective'
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : Field R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
hr : r ≠ 0
hr' : Membership.mem.{u_4, u_3} (α := A) s ((algebraMap R A : (a : R) → A) r : A)
⊢ HSMul.hSMul (β := A) r 1 ∈ s

Tactic:
rw [Algebra.algebraMap_eq_smul_one] at hr'

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : Field R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
hr : r ≠ 0
hr' : HSMul.hSMul (β := A) r 1 ∈ s
⊢ False

Tactic:
h1 <| inv_smul_smul₀ hr (1 : A) ▸ SMulMemClass.smul_mem r⁻¹ hr'

Premises used: SMulMemClass.smul_mem, inv_smul_smul₀, Eq.rec, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst : Field R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst_4 : FunLike F (Unitization.{u_2, u_4} R ↥s) A
inst_5 : AlgHomClass F R (Unitization.{u_2, u_4} R ↥s) A
f : F
hf : ∀ (x : ↥s), (f : (a : Unitization R ↥s) → A) (↑x : Unitization R ↥s) = (↑x : A)
r : R
hr : r ≠ 0
hr' : HSMul.hSMul (β := A) r 1 ∈ s
⊢ False

Tactic:
exact h1 <| inv_smul_smul₀ hr (1 : A) ▸ SMulMemClass.smul_mem r⁻¹ hr'
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R 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 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
⊢ Function.Bijective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(Algebra.adjoin R (↑s : Set A)))
    (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.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 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
refine_1 :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(Algebra.adjoin R (↑s : Set A)))
    (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A)))
refine_2 :
  ∀ (x : ↥(Algebra.adjoin R (↑s : Set A))),
    ∃ (a : Unitization.{u_1, u_3} R ↥s), (algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A))) a = x
⊢ Function.Bijective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(Algebra.adjoin R (↑s : Set A)))
    (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.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 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
x : ↥s
⊢ (AlgHom.comp (Subalgebra.val (Algebra.adjoin R (↑s : Set A))) algHom : (a : Unitization R ↥s) → A)
      (↑x : Unitization R ↥s) =
    (↑x : A)

Tactic:
simp [algHom]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (⇑(AlgHom.comp (Subalgebra.val (Algebra.adjoin R (↑s : Set A))) algHom) : (a : Unitization R ↥s) → A)

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

Tactic:
rw [AlgHom.coe_comp] at this

Premises used: AlgHom.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 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
this :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (Function.comp (β := ↥(Algebra.adjoin R (↑s : Set A)))
      (⇑(Subalgebra.val (Algebra.adjoin R (↑s : Set A))) : (a : ↥(Algebra.adjoin R (↑s : Set A))) → A)
      (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A))))
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(Algebra.adjoin R (↑s : Set A)))
    (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.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 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
this :
  Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := A)
    (Function.comp (β := ↥(Algebra.adjoin R (↑s : Set A)))
      (⇑(Subalgebra.val (Algebra.adjoin R (↑s : Set A))) : (a : ↥(Algebra.adjoin R (↑s : Set A))) → A)
      (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A))))
⊢ Function.Injective (α := Unitization.{u_1, u_3} R ↥s) (β := ↥(Algebra.adjoin R (↑s : Set A)))
    (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.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 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
x : ↥(Algebra.adjoin R (↑s : Set A))
refine_2 :
  ∀ (a : Unitization.{u_1, u_3} R ↥s)
    (ha : (AlgHom.toRingHom (unitization s) : (a : Unitization R ↥s) → A) a = (↑x : A)),
    ∃ (a : Unitization.{u_1, u_3} R ↥s), (algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A))) a = x
⊢ ∃ (a : Unitization.{u_1, u_3} R ↥s), (algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A))) a = x

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

Premises used: Eq.ge, NonUnitalSubalgebra.unitization_range, Subtype.val, AlgHom.range, Subtype.property, NonUnitalSubalgebra.unitization
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Field R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
x : ↥(Algebra.adjoin R (↑s : Set A))
a : Unitization.{u_1, u_3} R ↥s
ha : (AlgHom.toRingHom (unitization s) : (a : Unitization R ↥s) → A) a = (↑x : A)
⊢ ∃ (a : Unitization.{u_1, u_3} R ↥s), (algHom : (a : Unitization R ↥s) → ↥(Algebra.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 : Ring A
inst_2 : Algebra R A
inst_3 : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization.{u_1, u_3} R ↥s →ₐ[R] ↥(Algebra.adjoin R (↑s : Set A)) :=
  AlgHom.codRestrict (unitization s) (Algebra.adjoin R (↑s : Set A)) ⋯
x : ↥(Algebra.adjoin R (↑s : Set A))
a : Unitization.{u_1, u_3} R ↥s
ha : (AlgHom.toRingHom (unitization s) : (a : Unitization R ↥s) → A) a = (↑x : A)
⊢ ∃ (a : Unitization.{u_1, u_3} R ↥s), (algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A))) a = x

Tactic:
exact ⟨a, Subtype.ext ha⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
x : Unitization ℕ ↥s
⊢ (unitization s : (a : Unitization ℕ ↥s) → R) x = (↑x.toProd.1 : R) + (↑x.toProd.2 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
⊢ SMulMemClass S ℕ R

Tactic:
have := AddSubmonoidClass.nsmulMemClass (S := S)
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
this : SMulMemClass S ℕ R
rw :
  Eq (α := Subalgebra ℕ R)
    (AlgHom.range (A := Unitization ℕ ↥s) (NonUnitalSubalgebra.unitization s : Unitization ℕ ↥s →ₐ[ℕ] R))
    (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
rw₁ :
  Eq (α := Subalgebra ℕ R) (Algebra.adjoin ℕ (↑s : Set R)) (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
rw₂ rw₃ :
  Eq (α := Subalgebra ℕ R) (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
    (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
⊢ Eq (α := Subalgebra ℕ R) (AlgHom.range (A := Unitization ℕ ↥s) (unitization s))
    (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))

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

Premises used: NonUnitalSubsemiring.unitization, NonUnitalSubalgebra.unitization_range, Algebra.adjoin_nat
-- 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
x : Unitization ℤ ↥s
⊢ (unitization s : (a : Unitization ℤ ↥s) → R) x = (↑x.toProd.1 : R) + (↑x.toProd.2 : R)

Tactic:
rfl

Premises used: rfl