awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Tower (goal)
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ Eq (α := Submodule R A)
    (LinearMap.range (M := ↥S) (τ₁₂ := RingHom.id R)
      (↑(toAlgHom R (↥S) A) :
        [inst_3 : FunLike (↥S →ₐ[R] A) (↥S) A] → [SemilinearMapClass (↥S →ₐ[R] A) (RingHom.id R) (↥S) A] → ↥S →ₗ[R] A))
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)
have h : ∀ (x : A),
  Membership.mem (γ := Submodule R A)
      (LinearMap.range (M := ↥S) (τ₁₂ := RingHom.id R)
        (↑(toAlgHom R (↥S) A) :
          [inst_3 : FunLike (↥S →ₐ[R] A) (↥S) A] →
            [SemilinearMapClass (↥S →ₐ[R] A) (RingHom.id R) (↥S) A] → ↥S →ₗ[R] A))
      x ↔
    Membership.mem (γ := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : 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
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
⊢ AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S ↔
    NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
have refine_1 : ∀ (h : AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S),
  NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : 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
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
refine_1 :
  ∀ (h : AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S),
    NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
⊢ AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S ↔
    NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
have refine_2 : ∀ (h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra),
  AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ S
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : 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
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
x : Unitization R A
⊢ Membership.mem (α := C) S
    ((AlgHom.toRingHom (R := R) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) : (a : Unitization R A) → C) x :
      C)
have refine_2 : ∀ (r : R) (a : A),
  Membership.mem (α := C) S
    ((AlgHom.toRingHom (R := R) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) : (a : Unitization R A) → C)
        (inl r + (↑a : Unitization R A)) :
      C)
Tactic: induction x with
    | _ r a => simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : 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
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ AlgHom.range (A := Unitization R A) ((lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) f) ≤ c ↔
    Algebra.adjoin R (↑(NonUnitalAlgHom.range f) : Set C) ≤ c
have rw : NonUnitalAlgHom.range f ≤ c.toNonUnitalSubalgebra ↔ (↑(NonUnitalAlgHom.range f) : Set C) ⊆ (↑c : Set C)
Tactic: rw [lift_range_le, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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) (AlgHom.range (A := Unitization.{u_1, u_3} R ↥s) (unitization s))
    (Algebra.adjoin R (↑s : Set A))
have 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))
Tactic: rw [unitization, Unitization.lift_range]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)
have 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
Tactic: refine (injective_iff_map_eq_zero f).mpr fun x hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (hypothesis)
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)
⊢ Unitization.inl r + (↑a : Unitization R ↥s) = 0
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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
⊢ Unitization.inl r + (↑a : Unitization R ↥s) = 0
have inl_add_inr : ∀ (hx : (algebraMap R A : (a : R) → A) r = -(↑a : A)), Unitization.inl r = -(↑a : Unitization R ↥s)
Tactic: rw [add_eq_zero_iff_eq_neg] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)
⊢ Unitization.inl r = -(↑a : Unitization R ↥s)
have pos : ∀ (hr : r = 0), Unitization.inl r = -(↑a : Unitization R ↥s)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)
⊢ Unitization.inl r = -(↑a : Unitization R ↥s)
have neg : ∀ (hr : ¬r = 0), Unitization.inl r = -(↑a : Unitization R ↥s)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)
have pos : (Unitization.toProd (Unitization.inl r)).1 = (Unitization.toProd (-(↑a : Unitization R ↥s))).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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
⊢ Unitization.inl r = -(↑a : Unitization R ↥s)
have pos₁ : (↑(Unitization.toProd (Unitization.inl r)).2 : A) = (↑(Unitization.toProd (-(↑a : Unitization R ↥s))).2 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)
⊢ x = 0
have 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
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
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)
have refine : ∀ (r : R) (hr : r ≠ 0) (hr' : Membership.mem.{u_4, u_3} (α := A) s ((algebraMap R A : (a : R) → A) r : A)), False
Tactic: refine AlgHomClass.unitization_injective' s (fun r hr hr' ↦ ?_) f hf
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (hypothesis)
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)
⊢ False
have hr'₁ : HSMul.hSMul (β := A) r 1 ∈ s
Tactic: rw [Algebra.algebraMap_eq_smul_one] at hr'
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)))
have 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)))
Tactic: refine ⟨?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)))
⊢ 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)))
have 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
Tactic: refine ⟨?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (hypothesis)
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) (β := ↥(Algebra.adjoin R (↑s : Set A)))
    (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A)))
have 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)
Tactic: have := AlgHomClass.unitization_injective s h1
        ((Subalgebra.val _).comp algHom) fun _ ↦ by simp [algHom]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (hypothesis)
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) (β := ↥(Algebra.adjoin R (↑s : Set A)))
    (⇑algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A)))
have 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))))
Tactic: rw [AlgHom.coe_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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), (algHom : (a : Unitization R ↥s) → ↥(Algebra.adjoin R (↑s : Set A))) a = x
have 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
Tactic: obtain (⟨a, ha⟩ : (x : A) ∈ (unitization s).range) :=
        (unitization_range s).ge x.property
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
⊢ Eq (α := Subalgebra ℕ R) (AlgHom.range (A := Unitization ℕ ↥s) (unitization s))
    (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
have this : SMulMemClass S ℕ R
Tactic: have := AddSubmonoidClass.nsmulMemClass (S := S)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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
⊢ Eq (α := Subalgebra ℕ R) (AlgHom.range (A := Unitization ℕ ↥s) (unitization s))
    (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
have rw : Eq (α := Subalgebra ℕ R)
  (AlgHom.range (A := Unitization ℕ ↥s) (NonUnitalSubalgebra.unitization s : Unitization ℕ ↥s →ₐ[ℕ] R))
  (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
Tactic: rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_nat]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)))
⊢ Eq (α := Subalgebra ℕ R) (AlgHom.range (A := Unitization ℕ ↥s) (unitization s))
    (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
have rw₁ : Eq (α := Subalgebra ℕ R) (Algebra.adjoin ℕ (↑s : Set R)) (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
Tactic: rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_nat]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)))
⊢ Eq (α := Subalgebra ℕ R) (AlgHom.range (A := Unitization ℕ ↥s) (unitization s))
    (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
have rw₂ : Eq (α := Subalgebra ℕ R) (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
  (subalgebraOfSubsemiring (Subsemiring.closure (↑s : Set R)))
Tactic: rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_nat]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
⊢ Eq (α := Subalgebra ℤ R) (AlgHom.range (A := Unitization ℤ ↥s) (unitization s))
    (subalgebraOfSubring (Subring.closure (↑s : Set R)))
have this : SMulMemClass S ℤ R
Tactic: have := AddSubgroupClass.zsmulMemClass (S := S)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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
⊢ Eq (α := Subalgebra ℤ R) (AlgHom.range (A := Unitization ℤ ↥s) (unitization s))
    (subalgebraOfSubring (Subring.closure (↑s : Set R)))
have rw : Eq (α := Subalgebra ℤ R)
  (AlgHom.range (A := Unitization ℤ ↥s) (NonUnitalSubalgebra.unitization s : Unitization ℤ ↥s →ₐ[ℤ] R))
  (subalgebraOfSubring (Subring.closure (↑s : Set R)))
Tactic: rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_int]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)))
⊢ Eq (α := Subalgebra ℤ R) (AlgHom.range (A := Unitization ℤ ↥s) (unitization s))
    (subalgebraOfSubring (Subring.closure (↑s : Set R)))
have rw₁ : Eq (α := Subalgebra ℤ R) (Algebra.adjoin ℤ (↑s : Set R)) (subalgebraOfSubring (Subring.closure (↑s : Set R)))
Tactic: rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_int]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Unitization (goal)
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)))
⊢ Eq (α := Subalgebra ℤ R) (AlgHom.range (A := Unitization ℤ ↥s) (unitization s))
    (subalgebraOfSubring (Subring.closure (↑s : Set R)))
have rw₂ : Eq (α := Subalgebra ℤ R) (subalgebraOfSubring (Subring.closure (↑s : Set R)))
  (subalgebraOfSubring (Subring.closure (↑s : Set R)))
Tactic: rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_int]