awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : Algebra R B
inst_12 : StarRing B
inst_13 : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥S.topologicalClosure) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥S.topologicalClosure) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥S.topologicalClosure) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h :
  ∀ (x : ↥S),
    Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
      ((ψ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
refine :
  ∀ (x : ↥S),
    Eq.{u_3 + 1} (α := B) ((StarAlgHom.comp (↑φ : ↥S.topologicalClosure →⋆ₐ[R] B) (inclusion ⋯) : (a : ↥S) → B) x : B)
      ((StarAlgHom.comp (↑ψ : ↥S.topologicalClosure →⋆ₐ[R] B) (inclusion ⋯) : (a : ↥S) → B) x : B)
⊢ Eq (α := StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B) (↑φ : ↥S.topologicalClosure →⋆ₐ[R] B)
    (↑ψ : ↥S.topologicalClosure →⋆ₐ[R] B)

Tactic:
refine StarAlgHom.ext_topologicalClosure (R := R) (A := A) (B := B) hφ hψ (StarAlgHom.ext ?_)

Premises used: StarAlgHom.ext_topologicalClosure, StarAlgHom.ext
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : Algebra R B
inst_12 : StarRing B
inst_13 : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥S.topologicalClosure) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥S.topologicalClosure) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥S.topologicalClosure) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h :
  ∀ (x : ↥S),
    Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
      ((ψ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
⊢ ∀ (x : ↥S),
    Eq.{u_3 + 1} (α := B) ((StarAlgHom.comp (↑φ : ↥S.topologicalClosure →⋆ₐ[R] B) (inclusion ⋯) : (a : ↥S) → B) x : B)
      ((StarAlgHom.comp (↑ψ : ↥S.topologicalClosure →⋆ₐ[R] B) (inclusion ⋯) : (a : ↥S) → B) x : B)

Tactic:
simpa only [StarAlgHom.coe_comp, StarAlgHom.coe_coe] using h

Premises used: StarAlgHom.coe_coe, StarAlgHom.coe_comp
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : Algebra R B
inst_12 : StarRing B
inst_13 : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥S.topologicalClosure) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥S.topologicalClosure) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥S.topologicalClosure) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h :
  ∀ (x : ↥S),
    Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
      ((ψ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
⊢ Eq (α := StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B) (↑φ : ↥S.topologicalClosure →⋆ₐ[R] B)
    (↑ψ : ↥S.topologicalClosure →⋆ₐ[R] B)

Tactic:
have : (φ : S.topologicalClosure →⋆ₐ[R] B) = (ψ : S.topologicalClosure →⋆ₐ[R] B) := by
    refine StarAlgHom.ext_topologicalClosure (R := R) (A := A) (B := B) hφ hψ (StarAlgHom.ext ?_)
    simpa only [StarAlgHom.coe_comp, StarAlgHom.coe_coe] using h
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : Algebra R B
inst_12 : StarRing B
inst_13 : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥S.topologicalClosure) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥S.topologicalClosure) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥S.topologicalClosure) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h :
  ∀ (x : ↥S),
    Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
      ((ψ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
this :
  Eq (α := StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B) (↑φ : ↥S.topologicalClosure →⋆ₐ[R] B)
    (↑ψ : ↥S.topologicalClosure →⋆ₐ[R] B)
rw :
  Eq (α := (a : ↥S.topologicalClosure) → B) (⇑(↑φ : ↥S.topologicalClosure →⋆ₐ[R] B) : (a : ↥S.topologicalClosure) → B)
    (⇑ψ : (a : ↥S.topologicalClosure) → B)
⊢ φ = ψ

Tactic:
rw [DFunLike.ext'_iff, ← StarAlgHom.coe_coe]

Premises used: DFunLike.ext'_iff, StarAlgHom.coe_coe
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : Algebra R B
inst_12 : StarRing B
inst_13 : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥S.topologicalClosure) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥S.topologicalClosure) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥S.topologicalClosure) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h :
  ∀ (x : ↥S),
    Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
      ((ψ : (a : ↥S.topologicalClosure) → B)
          ((inclusion ⋯ : (a : ↥S) → ↥S.topologicalClosure) x : ↥S.topologicalClosure) :
        B)
this :
  Eq (α := StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B) (↑φ : ↥S.topologicalClosure →⋆ₐ[R] B)
    (↑ψ : ↥S.topologicalClosure →⋆ₐ[R] B)
⊢ Eq (α := (a : ↥S.topologicalClosure) → B) (⇑(↑φ : ↥S.topologicalClosure →⋆ₐ[R] B) : (a : ↥S.topologicalClosure) → B)
    (⇑ψ : (a : ↥S.topologicalClosure) → B)

Tactic:
apply congrArg _ this

Premises used: congrArg
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) (elemental R x) x

Tactic:
le_topologicalClosure _ (self_mem_adjoin_singleton R x)

Premises used: Set.Mem, StarAlgebra.self_mem_adjoin_singleton, StarSubalgebra.le_topologicalClosure
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) (elemental R x) (star x)

Tactic:
star_mem <| self_mem R x

Premises used: StarMemClass.star_mem, StarAlgebra.elemental.self_mem
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x : A
⊢ IsClosed[inst_2] (↑(elemental R x) : Set A)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A_1
inst_3 : Semiring A_1
inst_4 : StarRing A_1
inst_5 : IsSemitopologicalSemiring A_1
inst_6 : ContinuousStar A_1
inst_7 : Algebra R A_1
inst_8 : StarModule R A_1
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
A : Type u_4
inst_13 : UniformSpace A
inst_14 : CompleteSpace A
inst_15 : Semiring A
inst_16 : StarRing A
inst_17 : IsSemitopologicalSemiring A
inst_18 : ContinuousStar A
inst_19 : Algebra R A
inst_20 : StarModule R A
x : A
⊢ CompleteSpace.{u_4} ↥(elemental R x)

Tactic:
isClosed_closure.completeSpace_coe

Premises used: Set.Mem, setOf, closure, IsClosed.completeSpace_coe, Set.sInter
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
S : StarSubalgebra R A
hS : IsClosed[inst_2] (↑S : Set A)
x : A
hx : x ∈ S
⊢ elemental R x ≤ S

Tactic:
topologicalClosure_minimal (adjoin_le <| Set.singleton_subset_iff.2 hx) hS

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Mem, StarSubalgebra.topologicalClosure_minimal, StarAlgebra.adjoin_le
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x : A
s : StarSubalgebra R A
hs : IsClosed[inst_2] (↑s : Set A)
⊢ elemental R x ≤ s ↔ x ∈ s

Tactic:
⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

Premises used: StarAlgebra.elemental.le_of_mem, StarAlgebra.elemental.self_mem, Iff.intro
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x : A
⊢ IsClosed[inst_2]
    (Set.range (ι := ↥(elemental R x))
      (Subtype.val (p := fun (x_1 : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R x) x_1)))

Tactic:
simpa using isClosed R x

Premises used: StarAlgebra.elemental.isClosed
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : T2Space A
x : A
⊢ LE.le (α := StarSubalgebra R A) (elemental R x) (centralizer R (↑(centralizer R {x}) : Set A))

Tactic:
topologicalClosure_adjoin_le_centralizer_centralizer ..

Premises used: Set.Mem, StarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x y : A
hy : Membership.mem (γ := StarSubalgebra R A) (elemental R x) y
P : (u : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R x) u → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u + v) ⋯
mul :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R x) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
apply : ∀ (y : A) (hy : y ∈ (↑(adjoin R {x}) : Set A)), P y ⋯
⊢ P y hy

Tactic:
apply closure (adjoin R {x} : Set A) subset_closure (fun y hy ↦ ?_) y hy

Premises used: subset_closure, StarAlgebra.adjoin, SetLike.coe, Singleton.singleton
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x y_1 : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R x) y_1
P : (u : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R x) u → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u + v) ⋯
mul :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R x) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
y : A
hy : y ∈ (↑(adjoin R {x}) : Set A)
⊢ Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) y

Tactic:
rw [SetLike.mem_coe, ← mem_toSubalgebra, adjoin_toSubalgebra] at hy

Premises used: StarSubalgebra.mem_toSubalgebra, StarAlgebra.adjoin_toSubalgebra, SetLike.mem_coe
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x y_1 : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R x) y_1
P : (u : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R x) u → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u + v) ⋯
mul :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R x) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
y u : A
hu : Membership.mem (γ := Set A) ({x} ∪ star {x}) u
hy : u ∈ (↑(adjoin R {x}) : Set A)
⊢ u = x ∨ star u = x

Tactic:
simpa using hu
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x y_1 : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R x) y_1
P : (u : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R x) u → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u + v) ⋯
mul :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R x) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
y u : A
hu : Membership.mem (γ := Set A) ({x} ∪ star {x}) u
hy : u ∈ (↑(adjoin R {x}) : Set A)
mem :
  ∀ (hy : Membership.mem (γ := StarSubalgebra R A) (elemental R u) y_1)
    {P : (u_1 : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1 → Prop} (self : P u ⋯)
    (star_self : P (star u) ⋯) (algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯)
    (add :
      ∀ (u_1 : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1) (v : A)
        (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R u) v), P u_1 hu → P v hv → P (u_1 + v) ⋯)
    (mul :
      ∀ (u_1 : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1) (v : A)
        (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R u) v), P u_1 hu → P v hv → P (u_1 * v) ⋯)
    (closure :
      ∀ (s : Set A) (hs : s ⊆ (↑(elemental R u) : Set A)),
        (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯)
    (hu : Membership.mem (γ := Set A) ({u} ∪ star {u}) u) (hy : u ∈ (↑(adjoin R {u}) : Set A)), P u ⋯
mem₁ : ∀ (hu : star u = x), P u ⋯
⊢ P u ⋯

Tactic:
obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu

Premises used: rfl, Star.star
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
y_1 y u : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R u) y_1
P : (u_1 : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1 → Prop
self : P u ⋯
star_self : P (star u) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u_1 : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R u) v), P u_1 hu → P v hv → P (u_1 + v) ⋯
mul :
  ∀ (u_1 : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R u) v), P u_1 hu → P v hv → P (u_1 * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R u) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
hu : Membership.mem (γ := Set A) ({u} ∪ star {u}) u
hy : u ∈ (↑(adjoin R {u}) : Set A)
⊢ P u ⋯

Tactic:
self
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
y_1 y u : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R u) y_1
P : (u_1 : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1 → Prop
self : P u ⋯
star_self : P (star u) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u_1 : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R u) v), P u_1 hu → P v hv → P (u_1 + v) ⋯
mul :
  ∀ (u_1 : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R u) u_1) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R u) v), P u_1 hu → P v hv → P (u_1 * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R u) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
hu : Membership.mem (γ := Set A) ({u} ∪ star {u}) u
hy : u ∈ (↑(adjoin R {u}) : Set A)
⊢ P u ⋯

Tactic:
exact self
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x y_1 : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R x) y_1
P : (u : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R x) u → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u + v) ⋯
mul :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R x) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
y u : A
hu_1 : Membership.mem (γ := Set A) ({x} ∪ star {x}) u
hy : u ∈ (↑(adjoin R {x}) : Set A)
hu : star u = x
⊢ P u ⋯

Tactic:
simp_rw [← hu, star_star] at star_self

Premises used: star_star
-- Module: Mathlib.Topology.Algebra.StarSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x y_1 : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R x) y_1
P : (u : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R x) u → Prop
self : P x ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u + v) ⋯
mul :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R x) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
y u : A
hu_1 : Membership.mem (γ := Set A) ({x} ∪ star {x}) u
hy : u ∈ (↑(adjoin R {x}) : Set A)
hu : star u = x
star_self : P u ⋯
⊢ P u ⋯

Tactic:
star_self