awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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 : 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
S : StarSubalgebra R A
f : A →⋆ₐ[R] B
⊢ toSubalgebra (map f S) = Subalgebra.map (↑f : A →ₐ[R] B) S.toSubalgebra

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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 : 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
S : StarSubalgebra R A
f : A →⋆ₐ[R] B
⊢ (↑(map f S) : Set B) = (⇑f : (a : A) → B) '' (↑S : Set A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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 : 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
S : StarSubalgebra R A
f : A →⋆ₐ[R] B
U : StarSubalgebra R B
⊢ map f S ≤ U ↔ S ≤ comap f U

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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 : 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
f : A →⋆ₐ[R] B
⊢ GaloisConnection (α := StarSubalgebra R A) (β := StarSubalgebra R B) (map f) (comap f)

Tactic:
fun _S _U =>
  map_le_iff_le_comap

Premises used: StarSubalgebra.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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 : 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
S₁ S₂ : StarSubalgebra R B
f : A →⋆ₐ[R] B
⊢ S₁ ≤ S₂ → LE.le (α := StarSubalgebra R A) (comap f S₁) (comap f S₂)

Tactic:
Set.preimage_mono

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage_mono, Set.preimage
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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 : 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
f : A →⋆ₐ[R] B
hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Injective (α := StarSubalgebra R B) (β := StarSubalgebra R A) (comap f)

Tactic:
fun _S₁ _S₂ h =>
  ext fun b =>
    let ⟨x, hx⟩ := hf b
    let this := SetLike.ext_iff.1 h x
    hx ▸ this

Premises used: Membership.mem, Eq.rec, SetLike.ext_iff, StarSubalgebra.ext, Iff, Iff.mp, _private.0.StarSubalgebra.comap_injective.match_1, Function.Injective
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : StarSubalgebra R A
⊢ comap (StarAlgHom.id R A) S = S

Tactic:
SetLike.coe_injective <| Set.preimage_id

Premises used: Set.preimage_id, SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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
S : StarSubalgebra R C
g : B →⋆ₐ[R] C
f : A →⋆ₐ[R] B
⊢ (↑(comap f (comap g S)) : Set A) = (↑(comap (g.comp f) S) : Set A)

Tactic:
Set.preimage_preimage

Premises used: Set.preimage_preimage, Set.Mem, setOf, Set.preimage, AlgHom.comp
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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
S : StarSubalgebra R C
g : B →⋆ₐ[R] C
f : A →⋆ₐ[R] B
⊢ (↑(comap f (comap g S)) : Set A) = (↑(comap (g.comp f) S) : Set A)

Tactic:
exact Set.preimage_preimage

Premises used: Set.preimage_preimage
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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 : 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
S : StarSubalgebra R B
f : A →⋆ₐ[R] B
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) (comap f S) x ↔ Membership.mem (α := B) S ((f : (a : A) → B) x : B)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
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 : 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
S : StarSubalgebra R B
f : A →⋆ₐ[R] B
⊢ (↑(comap f S) : Set A) = (⇑f : (a : A) → B) ⁻¹' (↑S : Set B)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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 s) : Set A) = (s ∪ star s).centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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
z : A
⊢ Membership.mem (γ := StarSubalgebra R A) (centralizer R s) z ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Tactic:
simp [← SetLike.mem_coe, centralizer_union, ← image_star, mem_centralizer_iff, forall_and]

Premises used: Set.image_star, SetLike.mem_coe, StarSubalgebra.mem_centralizer_iff, Set.centralizer_union, forall_and
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : Set A
h : s ⊆ t
⊢ LE.le (α := StarSubalgebra R A) (centralizer R t) (centralizer R s)

Tactic:
Set.centralizer_subset (Set.union_subset_union h <| Set.preimage_mono h)

Premises used: Set.union_subset_union, Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset, Set.preimage_mono
-- Module: Mathlib.Algebra.Star.Subalgebra
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
⊢ Eq (α := Subalgebra R A) (toSubalgebra (centralizer R s)) (Subalgebra.centralizer R (s ∪ star s))

Tactic:
rfl

Premises used: Subalgebra.centralizer, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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
rw₃ rw₄ : (s ∪ star s).centralizer.centralizer = (s ∪ star s).centralizer.centralizer
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer

Tactic:
rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]

Premises used: StarMemClass.star_coe_eq, StarSubalgebra.coe_centralizer, Set.union_self
-- Module: Mathlib.Algebra.Star.Subalgebra
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
simp : ∀ (hx : star x ∈ S) (hy : star y ∈ S), star (x * y) ∈ S
⊢ x * y ∈ star S.carrier

Tactic:
simp only [Set.mem_star, Subalgebra.mem_carrier] at *

Premises used: Subalgebra.mem_carrier, Set.mem_star
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : star x ∈ S
hy : star y ∈ S
⊢ star (x * y) ∈ S

Tactic:
(star_mul x y).symm ▸ mul_mem hy hx

Premises used: Set.Mem, Eq.rec, StarMul.star_mul, Eq.symm, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : star x ∈ S
hy : star y ∈ S
⊢ star (x * y) ∈ S

Tactic:
exact (star_mul x y).symm ▸ mul_mem hy hx
-- Module: Mathlib.Algebra.Star.Subalgebra
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
simp : ∀ (hx : star x ∈ S) (hy : star y ∈ S), star (x + y) ∈ S
⊢ x + y ∈ star S.carrier

Tactic:
simp only [Set.mem_star, Subalgebra.mem_carrier] at *

Premises used: Subalgebra.mem_carrier, Set.mem_star
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : star x ∈ S
hy : star y ∈ S
⊢ star (x + y) ∈ S

Tactic:
(star_add x y).symm ▸ add_mem hx hy

Premises used: Set.Mem, StarAddMonoid.star_add, Eq.rec, AddMemClass.add_mem, Eq.symm
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : star x ∈ S
hy : star y ∈ S
⊢ star (x + y) ∈ S

Tactic:
exact (star_add x y).symm ▸ add_mem hx hy
-- Module: Mathlib.Algebra.Star.Subalgebra
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
r : R
⊢ Membership.mem (α := A) (star S.carrier) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
simpa only [Set.mem_star, Subalgebra.mem_carrier, ← algebraMap_star_comm] using
          S.algebraMap_mem (star r)

Premises used: Subalgebra.mem_carrier, Set.mem_star, Subalgebra.algebraMap_mem, algebraMap_star_comm, Star.star
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : Subalgebra 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.Subalgebra
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 : Subalgebra R A
x : A
⊢ star x ∈ star S ↔ x ∈ S

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : Subalgebra R A
⊢ (↑(star S) : Set A) = star (↑S : Set A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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
⊢ Monotone.{u_3, u_3} (α := Subalgebra R A) star

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

Premises used: Set.Mem, Monotone, setOf, Set.preimage
-- Module: Mathlib.Algebra.Star.Subalgebra
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
this : ∀ (t : Set A), LE.le (α := Subalgebra R A) (Algebra.adjoin R (star t)) (star (Algebra.adjoin R t))
⊢ LE.le (α := Subalgebra R A) (star (Algebra.adjoin R s)) (Algebra.adjoin R (star s))

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

Premises used: star_star, Subalgebra.star_mono, Star.star
-- Module: Mathlib.Algebra.Star.Subalgebra
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
⊢ 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 *

Premises used: GaloisInsertion.l_sup_u, Subalgebra.mem_carrier, Algebra.gi
-- Module: Mathlib.Algebra.Star.Subalgebra
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
rw : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (star ((↑(star S) : Set A) ⊔ (↑S : Set A)))) a
⊢ Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ⊔ (↑(star S) : Set A))) (star a)

Tactic:
rw [← mem_star_iff _ a, star_adjoin_comm, sup_comm]

Premises used: Subalgebra.star_adjoin_comm, sup_comm, Subalgebra.mem_star_iff
-- Module: Mathlib.Algebra.Star.Subalgebra
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 (star ((↑(star S) : Set A) ⊔ (↑S : Set A)))) a

Tactic:
simpa using ha
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : Subalgebra R A
⊢ (↑S.starClosure : Set A) = (↑(S ⊔ star S) : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : Subalgebra R A
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) S.starClosure x ↔ x ∈ S ⊔ star S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : Subalgebra R A
⊢ StarSubalgebra.toSubalgebra S.starClosure = S ⊔ star S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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₁ : Subalgebra R A
S₂ : StarSubalgebra R A
h : S₁ ≤ S₂.toSubalgebra
⊢ S₁.starClosure ≤ S₂

Tactic:
StarSubalgebra.toSubalgebra_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, Eq.rec, StarMemClass.star_mem, StarSubalgebra.toSubalgebra_le_iff, Iff.mp, sup_le, Subalgebra.mem_star_iff
-- Module: Mathlib.Algebra.Star.Subalgebra
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₁ : Subalgebra R A
S₂ : StarSubalgebra R A
⊢ S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toSubalgebra

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

Premises used: Subalgebra.starClosure_le, le_sup_left, Iff.intro, LE.le.trans
-- Module: Mathlib.Algebra.Star.Subalgebra
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
rwa₅ rwa₆ rwa₇ rwa₈ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R (s ∪ star s)) a
⊢ star a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (Algebra.adjoin R (s ∪ star s)))))

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

Premises used: Subalgebra.star_adjoin_comm, star_star, Subalgebra.mem_carrier, Set.union_comm, Set.union_star, Subalgebra.mem_star_iff
-- Module: Mathlib.Algebra.Star.Subalgebra
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
⊢ Eq (α := StarSubalgebra R A) (adjoin R s) (Subalgebra.starClosure (Algebra.adjoin R s))

Tactic:
toSubalgebra_injective <|
    show Algebra.adjoin R (s ∪ star s) = Algebra.adjoin R s ⊔ star (Algebra.adjoin R s) from
      (Subalgebra.star_adjoin_comm R s).symm ▸ Algebra.adjoin_union s (star s)

Premises used: Subalgebra.star_adjoin_comm, Algebra.adjoin_union, Eq.rec, StarSubalgebra.toSubalgebra_injective, Eq.symm, Star.star
-- Module: Mathlib.Algebra.Star.Subalgebra
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
⊢ Eq (α := Subalgebra R A) (toSubalgebra (adjoin R s)) (Algebra.adjoin R (s ∪ star s))

Tactic:
rfl

Premises used: Algebra.adjoin, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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 ⊆ (↑(adjoin R s) : Set A)

Tactic:
Set.subset_union_left.trans Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin, HasSubset.Subset.trans, Set.subset_union_left
-- Module: Mathlib.Algebra.Star.Subalgebra
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
x : A
hx : x ∈ s
⊢ Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x

Tactic:
subset_adjoin R s hx

Premises used: StarAlgebra.subset_adjoin
-- Module: Mathlib.Algebra.Star.Subalgebra
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
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) (adjoin R {x}) x

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

Premises used: Set.mem_singleton, Set.Mem, Algebra.subset_adjoin, Set.mem_union_left
-- Module: Mathlib.Algebra.Star.Subalgebra
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
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) (adjoin R {x}) (star x)

Tactic:
star_mem <| self_mem_adjoin_singleton R x

Premises used: StarAlgebra.self_mem_adjoin_singleton, StarMemClass.star_mem
-- Module: Mathlib.Algebra.Star.Subalgebra
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
rw : s ∪ star s ⊆ (↑S : Set A) ↔ s ≤ (↑S : Set A)
⊢ adjoin R s ≤ S ↔ s ≤ (↑S : Set A)

Tactic:
rw [← toSubalgebra_le_iff, adjoin_toSubalgebra, Algebra.adjoin_le_iff, coe_toSubalgebra]

Premises used: StarSubalgebra.toSubalgebra_le_iff, Algebra.adjoin_le_iff, StarAlgebra.adjoin_toSubalgebra, StarSubalgebra.coe_toSubalgebra
-- Module: Mathlib.Algebra.Star.Subalgebra
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
⊢ 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.Subalgebra
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
⊢ 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.Subalgebra
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 : StarSubalgebra R A
s : Set A
hs : s ⊆ (↑S : Set A)
⊢ adjoin R s ≤ S

Tactic:
StarAlgebra.gc.l_le hs

Premises used: GaloisConnection.l_le, StarAlgebra.gc
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : StarSubalgebra R A
s : Set A
⊢ adjoin R s ≤ S ↔ s ⊆ (↑S : Set A)

Tactic:
StarAlgebra.gc _ _

Premises used: StarAlgebra.gc