awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
S : NonUnitalSubalgebra R A
r : R
x : A
hx : x ∈ star S.carrier
⊢ r • x ∈ star S.carrier

Tactic:
simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier]
        using (star_smul r x).symm ▸ SMulMemClass.smul_mem (star r) hx

Premises used: NonUnitalSubalgebra.mem_carrier, Set.mem_star
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
S : NonUnitalSubalgebra R A
x : A
⊢ x ∈ star S ↔ star x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
S : NonUnitalSubalgebra R A
x : A
⊢ star x ∈ star S ↔ x ∈ S

Tactic:
simp
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
S : NonUnitalSubalgebra R A
⊢ (↑(star S) : Set A) = star (↑S : Set A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
⊢ Monotone.{v, v} (α := NonUnitalSubalgebra R A) star

Tactic:
fun _ _ h _ hx => h hx

Premises used: Set.Mem, Monotone, setOf, Set.preimage
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
s : Set A
this :
  ∀ (t : Set A),
    LE.le (α := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star t)) (star (NonUnitalAlgebra.adjoin R t))
⊢ LE.le (α := NonUnitalSubalgebra R A) (star (NonUnitalAlgebra.adjoin R s)) (NonUnitalAlgebra.adjoin R (star s))

Tactic:
simpa only [star_star] using NonUnitalSubalgebra.star_mono (this (star s))

Premises used: star_star, NonUnitalSubalgebra.star_mono, Star.star
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
a : A
ha : a ∈ (S ⊔ star S).carrier
⊢ star a ∈ (S ⊔ star S).carrier

Tactic:
simpa [← mem_star_iff _ a, ← (@NonUnitalAlgebra.gi R A _ _ _ _ _).l_sup_u _ _, star_adjoin_comm,
      Set.union_comm] using ha

Premises used: GaloisInsertion.l_sup_u, NonUnitalSubalgebra.mem_star_iff, Set.union_comm, NonUnitalAlgebra.gi, NonUnitalSubalgebra.star_adjoin_comm
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
⊢ (↑S.starClosure : Set A) = (↑(S ⊔ star S) : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) S.starClosure x ↔ x ∈ S ⊔ star S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
⊢ NonUnitalStarSubalgebra.toNonUnitalSubalgebra S.starClosure = S ⊔ star S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
S₁ : NonUnitalSubalgebra R A
S₂ : NonUnitalStarSubalgebra R A
h : S₁ ≤ S₂.toNonUnitalSubalgebra
⊢ S₁.starClosure ≤ S₂

Tactic:
NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff.1 <|
    sup_le h fun x hx =>
      (star_star x ▸ star_mem (show star x ∈ S₂ from h <| (S₁.mem_star_iff _).1 hx) : x ∈ S₂)

Premises used: star_star, NonUnitalSubalgebra.mem_star_iff, Eq.rec, StarMemClass.star_mem, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff, Iff.mp, sup_le
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
S₁ : NonUnitalSubalgebra R A
S₂ : NonUnitalStarSubalgebra R A
⊢ S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toNonUnitalSubalgebra

Tactic:
⟨fun h => le_sup_left.trans h, starClosure_le⟩

Premises used: le_sup_left, NonUnitalSubalgebra.starClosure_le, Iff.intro, LE.le.trans
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
⊢ Monotone.{v, v} (α := NonUnitalSubalgebra R A) (β := NonUnitalStarSubalgebra R A) starClosure

Tactic:
fun _ _ h => starClosure_le <| h.trans le_sup_left

Premises used: le_sup_left, Monotone, NonUnitalSubalgebra.starClosure_le, LE.le.trans
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
s : Set A
a : A
h :
  a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))
rwa : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s)) (star a)
rwa₁ : Membership.mem (γ := NonUnitalSubalgebra R A) (star (NonUnitalAlgebra.adjoin R (s ∪ star s))) a
rwa₂ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star (s ∪ star s))) a
rwa₃ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star s ∪ star (star s))) a
rwa₄ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (star s ∪ s)) a
rwa₅ rwa₆ rwa₇ rwa₈ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s)) a
⊢ star a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgebra.adjoin R (s ∪ star s)))))

Tactic:
rwa [NonUnitalSubalgebra.mem_carrier, ← NonUnitalSubalgebra.mem_star_iff,
      NonUnitalSubalgebra.star_adjoin_comm, Set.union_star, star_star, Set.union_comm]

Premises used: star_star, NonUnitalSubalgebra.mem_star_iff, Set.union_comm, Set.union_star, NonUnitalSubalgebra.mem_carrier, NonUnitalSubalgebra.star_adjoin_comm
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
⊢ Eq (α := NonUnitalStarSubalgebra R A) (adjoin R s) (NonUnitalSubalgebra.starClosure (NonUnitalAlgebra.adjoin R s))

Tactic:
toNonUnitalSubalgebra_injective <| show
    NonUnitalAlgebra.adjoin R (s ∪ star s) =
      NonUnitalAlgebra.adjoin R s ⊔ star (NonUnitalAlgebra.adjoin R s)
    from
      (NonUnitalSubalgebra.star_adjoin_comm R s).symm ▸ NonUnitalAlgebra.adjoin_union s (star s)

Premises used: NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective, Eq.rec, Eq.symm, NonUnitalAlgebra.adjoin_union, Star.star, NonUnitalSubalgebra.star_adjoin_comm
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
⊢ Eq (α := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra (adjoin R s)) (NonUnitalAlgebra.adjoin R (s ∪ star s))

Tactic:
rfl

Premises used: NonUnitalAlgebra.adjoin, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
⊢ s ⊆ (↑(adjoin R s) : Set A)

Tactic:
Set.subset_union_left.trans <| NonUnitalAlgebra.subset_adjoin R

Premises used: NonUnitalAlgebra.subset_adjoin, HasSubset.Subset.trans, Set.subset_union_left
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
⊢ star s ⊆ (↑(adjoin R s) : Set A)

Tactic:
Set.subset_union_right.trans <| NonUnitalAlgebra.subset_adjoin R

Premises used: NonUnitalAlgebra.subset_adjoin, Set.subset_union_right, HasSubset.Subset.trans
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
x : A
hx : x ∈ s
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x

Tactic:
subset_adjoin R s hx

Premises used: NonUnitalStarAlgebra.subset_adjoin
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R {x}) x

Tactic:
NonUnitalAlgebra.subset_adjoin R <| Set.mem_union_left _ (Set.mem_singleton x)

Premises used: Set.mem_singleton, Set.Mem, NonUnitalAlgebra.subset_adjoin, Set.mem_union_left
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R {x}) (star x)

Tactic:
star_mem <| self_mem_adjoin_singleton R x

Premises used: StarMemClass.star_mem, NonUnitalStarAlgebra.self_mem_adjoin_singleton
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
⊢ p a ha

Tactic:
NonUnitalAlgebra.adjoin_induction (fun x hx ↦ ?_) add zero mul smul ha

Premises used: NonUnitalAlgebra.adjoin_induction
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
refine : ∀ (x : A) (hx : x ∈ s ∪ Star.star s), p x ⋯
⊢ p a ha

Tactic:
refine NonUnitalAlgebra.adjoin_induction (fun x hx ↦ ?_) add zero mul smul ha
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx : x ∈ s ∪ Star.star s
⊢ x ∈ s ∨ Star.star x ∈ s

Tactic:
push _ ∈ _ at hx
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : x ∈ s ∨ Star.star x ∈ s
inl : ∀ (hx : x ∈ s), p x ⋯
inr : ∀ (hx : Star.star x ∈ s), p x ⋯
⊢ p x ⋯

Tactic:
obtain (hx | hx) := hx
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : x ∈ s
⊢ p x ⋯

Tactic:
mem x hx
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : x ∈ s
⊢ p x ⋯

Tactic:
exact mem x hx
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ Star.star x ∈ s ∪ Star.star s

Tactic:
simpa using Or.inl hx

Premises used: Or.inl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ p x ⋯

Tactic:
simpa using star _ (NonUnitalAlgebra.subset_adjoin R (by simpa using Or.inl hx)) (mem _ hx)

Premises used: NonUnitalAlgebra.subset_adjoin
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
rw : s ∪ star s ⊆ (↑S : Set A) ↔ s ≤ (↑S : Set A)
⊢ adjoin R s ≤ S ↔ s ≤ (↑S : Set A)

Tactic:
rw [← toNonUnitalSubalgebra_le_iff, adjoin_toNonUnitalSubalgebra,
    NonUnitalAlgebra.adjoin_le_iff, coe_toNonUnitalSubalgebra]

Premises used: NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_le_iff, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff, NonUnitalStarSubalgebra.coe_toNonUnitalSubalgebra
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ (↑S : Set A) ↔ s ≤ (↑S : Set A)

Tactic:
⟨fun h => Set.subset_union_left.trans h,
    fun h => Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩

Premises used: star_star, Eq.rec, StarMemClass.star_mem, HasSubset.Subset.trans, Set.union_subset, Set.subset_union_left, Iff.intro
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ (↑S : Set A) ↔ s ≤ (↑S : Set A)

Tactic:
exact ⟨fun h => Set.subset_union_left.trans h,
    fun h => Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s ⊆ (↑S : Set A)
⊢ adjoin R s ≤ S

Tactic:
NonUnitalStarAlgebra.gc.l_le hs

Premises used: GaloisConnection.l_le, NonUnitalStarAlgebra.gc