awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.StarRingHom (goal)
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →⋆ₙ+* B
h₁ :
  ∀ (x y : A),
    (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
h₂ : { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun (x + y) =
      { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun x +
        { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₙ+* B }.toFun (star a) =
      star ({ toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₙ+* B }.toFun a)
⊢ { toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ : A →⋆ₙ+* B } = f
have h : ∀ (x : A),
  Eq.{u_2 + 1} (α := B)
    (({ toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ : A →⋆ₙ+* B } :
          (a : A) → B)
        x :
      B)
    ((f : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.StarRingHom (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
f g : A ≃⋆+* B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g
have rcases : ∀ (toFun : A → B) (invFun : B → A) (left_inv : Function.LeftInverse invFun toFun)
  (right_inv : Function.RightInverse invFun toFun)
  (map_mul' :
    ∀ (x y : A),
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun (x * y) =
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun x *
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun y)
  (map_add' :
    ∀ (x y : A),
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun (x + y) =
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun x +
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun y)
  (map_star' :
    ∀ (a : A),
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
              map_add' := map_add' : A ≃+* B }.toFun
          (star a) =
        star
          ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                map_add' := map_add' : A ≃+* B }.toFun
            a))
  (h₁ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', map_star' := map_star' : A ≃⋆+* B }.toFun =
      g.toFun)
  (h₂ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', map_star' := map_star' : A ≃⋆+* B }.invFun =
      g.invFun),
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
      map_add' := map_add', map_star' := map_star' : A ≃⋆+* B } =
    g
Tactic: rcases f with ⟨⟨⟨_, _, _⟩, _⟩, _⟩
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Star.StarRingHom (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
e₁ : A ≃⋆+* B
e₂ : B ≃⋆+* C
a : A
⊢ e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a))
have rw : e₂.toFun (star (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
Tactic: rw [e₁.map_star', e₂.map_star']
-- Lean 4 proof step from Mathlib.Algebra.Star.StarRingHom (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
e₁ : A ≃⋆+* B
e₂ : B ≃⋆+* C
a : A
rw : e₂.toFun (star (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
⊢ e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a))
have rw₁ : star (e₂.toFun (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
Tactic: rw [e₁.map_star', e₂.map_star']
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
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 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
p q : StarSubalgebra R A
h :
  Eq.{u_3 + 1} (α := Set A) ((fun (S : StarSubalgebra R A) ↦ S.carrier) p)
    ((fun (S : StarSubalgebra R A) ↦ S.carrier) q)
⊢ p = q
have obtain : ∀ (carrier : Set A) (mul_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier)
  (one_mem' : 1 ∈ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup A }.carrier)
  (add_mem' :
    ∀ {a b : A},
      a ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
        b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
          a + b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier)
  (zero_mem' : 0 ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier)
  (algebraMap_mem' :
    ∀ (r : R),
      Membership.mem (α := A)
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem' : Subsemiring A }.carrier
        ((algebraMap R A : (a : R) → A) r : A))
  (star_mem' :
    ∀ {a : A},
      a ∈
          { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
              zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier →
        star a ∈
          { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
              zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier)
  (h :
    Eq.{u_3 + 1} (α := Set A)
      ((fun (S : StarSubalgebra R A) ↦ S.carrier)
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
          zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' })
      ((fun (S : StarSubalgebra R A) ↦ S.carrier) q)),
  { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' } =
    q
Tactic: obtain ⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩ := p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
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 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
q : StarSubalgebra R A
carrier : Set A
mul_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
one_mem' : 1 ∈ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup A }.carrier
add_mem' :
  ∀ {a b : A},
    a ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
      b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
        a + b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier
zero_mem' : 0 ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier
algebraMap_mem' :
  ∀ (r : R),
    Membership.mem (α := A)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem' :
          Subsemiring A }.carrier
      ((algebraMap R A : (a : R) → A) r : A)
star_mem' :
  ∀ {a : A},
    a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier →
      star a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier
h :
  Eq.{u_3 + 1} (α := Set A)
    ((fun (S : StarSubalgebra R A) ↦ S.carrier)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
        algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' })
    ((fun (S : StarSubalgebra R A) ↦ S.carrier) q)
⊢ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' } =
    q
have mk : ∀ (toSubalgebra : Subalgebra R A) (star_mem'_1 : ∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier)
  (h :
    Eq.{u_3 + 1} (α := Set A)
      ((fun (S : StarSubalgebra R A) ↦ S.carrier)
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
          zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' })
      ((fun (S : StarSubalgebra R A) ↦ S.carrier) { toSubalgebra := toSubalgebra, star_mem' := @star_mem'_1 })),
  Eq (α := StarSubalgebra R A)
    { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' }
    { toSubalgebra := toSubalgebra, star_mem' := @star_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : 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
S T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
⊢ x ∈ S ↔ x ∈ T
have rw : x ∈ S.toSubalgebra ↔ x ∈ T
Tactic: rw [← mem_toSubalgebra, ← mem_toSubalgebra, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : 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
S T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
rw : x ∈ S.toSubalgebra ↔ x ∈ T
⊢ x ∈ S ↔ x ∈ T
have rw₁ : x ∈ S.toSubalgebra ↔ x ∈ T.toSubalgebra
Tactic: rw [← mem_toSubalgebra, ← mem_toSubalgebra, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : 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
S T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
rw : x ∈ S.toSubalgebra ↔ x ∈ T
rw₁ : x ∈ S.toSubalgebra ↔ x ∈ T.toSubalgebra
⊢ x ∈ S ↔ x ∈ T
have rw₂ : x ∈ T.toSubalgebra ↔ x ∈ T.toSubalgebra
Tactic: rw [← mem_toSubalgebra, ← mem_toSubalgebra, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : 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
s : Set A
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer
have rw : ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
Tactic: rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : 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
s : Set A
rw :
  ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer
have rw₁ : ((↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
Tactic: rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : 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
s : Set A
rw :
  ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
rw₁ : ((↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer
have rw₂ : (↑(centralizer R s) : Set A).centralizer = (s ∪ star s).centralizer.centralizer
Tactic: rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : 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
s : Set A
rw :
  ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
rw₁ : ((↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
rw₂ : (↑(centralizer R s) : Set A).centralizer = (s ∪ star s).centralizer.centralizer
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer
have rw₃ : (s ∪ star s).centralizer.centralizer = (s ∪ star s).centralizer.centralizer
Tactic: rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
S : Subalgebra R A
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x * y ∈ star S.carrier
have simp : ∀ (hx : star x ∈ S) (hy : star y ∈ S), star (x * y) ∈ S
Tactic: simp only [Set.mem_star, Subalgebra.mem_carrier] at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
S : Subalgebra R A
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x + y ∈ star S.carrier
have simp : ∀ (hx : star x ∈ S) (hy : star y ∈ S), star (x + y) ∈ S
Tactic: simp only [Set.mem_star, Subalgebra.mem_carrier] at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (hypothesis)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ (S ⊔ star S).carrier
⊢ star a ∈ (S ⊔ star S).carrier
have ha₁ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ⊔ (↑(star S) : Set A))) a
Tactic: simp only [Subalgebra.mem_carrier, ← (@Algebra.gi R A _ _ _).l_sup_u _ _] at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
S : Subalgebra R A
a : A
ha : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ⊔ (↑(star S) : Set A))) a
⊢ Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ⊔ (↑(star S) : Set A))) (star a)
have rw : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star ((↑(star S) : Set A) ⊔ (↑S : Set A)))) a
Tactic: rw [← mem_star_iff _ a, star_adjoin_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
s : Set A
a : A
hx :
  a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
⊢ star a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
have rwa : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (s ∪ star s)) (star a)
Tactic: rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
        Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
s : Set A
a : A
hx :
  a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (s ∪ star s)) (star a)
⊢ star a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
have rwa₁ : Membership.mem (γ := Subalgebra R A) (star (Algebra.adjoin R (s ∪ star s))) a
Tactic: rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
        Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
s : Set A
a : A
hx :
  a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (s ∪ star s)) (star a)
rwa₁ : Membership.mem (γ := Subalgebra R A) (star (Algebra.adjoin R (s ∪ star s))) a
⊢ star a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
have rwa₂ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star (s ∪ star s))) a
Tactic: rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
        Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
s : Set A
a : A
hx :
  a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (s ∪ star s)) (star a)
rwa₁ : Membership.mem (γ := Subalgebra R A) (star (Algebra.adjoin R (s ∪ star s))) a
rwa₂ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star (s ∪ star s))) a
⊢ star a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
have rwa₃ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star s ∪ star (star s))) a
Tactic: rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
        Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
s : Set A
a : A
hx :
  a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (s ∪ star s)) (star a)
rwa₁ : Membership.mem (γ := Subalgebra R A) (star (Algebra.adjoin R (s ∪ star s))) a
rwa₂ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star (s ∪ star s))) a
rwa₃ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star s ∪ star (star s))) a
⊢ star a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
have rwa₄ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star s ∪ s)) a
Tactic: rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
        Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
s : Set A
a : A
hx :
  a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (s ∪ star s)) (star a)
rwa₁ : Membership.mem (γ := Subalgebra R A) (star (Algebra.adjoin R (s ∪ star s))) a
rwa₂ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star (s ∪ star s))) a
rwa₃ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star s ∪ star (star s))) a
rwa₄ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star s ∪ s)) a
⊢ star a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))
have rwa₅ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (s ∪ star s)) a
Tactic: rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
        Set.union_star, star_star, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
S : StarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ≤ (↑S : Set A)
have rw : s ∪ star s ⊆ (↑S : Set A) ↔ s ≤ (↑S : Set A)
Tactic: rw [← toSubalgebra_le_iff, adjoin_toSubalgebra, Algebra.adjoin_le_iff, coe_toSubalgebra]