awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact star_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 : A
r : R
hy : Membership.mem (α := A) (↑(adjoin R {x}) : Set A) ((Algebra.algebraMap R A : (a : R) → A) r : A)
⊢ P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯

Tactic:
algebraMap r
-- 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
r : R
hy : Membership.mem (α := A) (↑(adjoin R {x}) : Set A) ((Algebra.algebraMap R A : (a : R) → A) r : A)
⊢ P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯

Tactic:
exact algebraMap r
-- 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 v : A
hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u
hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v
hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯
hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v ⋯
hy : u + v ∈ (↑(adjoin R {x}) : Set A)
⊢ P (u + v) ⋯

Tactic:
add u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)

Premises used: subset_closure
-- 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 v : A
hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u
hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v
hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯
hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v ⋯
hy : u + v ∈ (↑(adjoin R {x}) : Set A)
⊢ P (u + v) ⋯

Tactic:
exact add u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)

Premises used: subset_closure
-- 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 v : A
hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u
hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v
hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯
hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v ⋯
hy : u * v ∈ (↑(adjoin R {x}) : Set A)
⊢ P (u * v) ⋯

Tactic:
mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)

Premises used: subset_closure
-- 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 v : A
hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u
hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v
hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯
hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v ⋯
hy : u * v ∈ (↑(adjoin R {x}) : Set A)
⊢ P (u * v) ⋯

Tactic:
exact mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)

Premises used: subset_closure
-- 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_2 : y ∈ (↑(adjoin R {x}) : Set A)
hy : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) y
mem : ∀ (u : A) (hu : Membership.mem (γ := Set A) ({x} ∪ star {x}) u) (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯
algebraMap₁ :
  ∀ (r : R) (hy : Membership.mem (α := A) (↑(adjoin R {x}) : Set A) ((Algebra.algebraMap R A : (a : R) → A) r : A)),
    P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add₁ :
  ∀ (u v : A) (hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u)
    (hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v)
    (hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯) (hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v ⋯)
    (hy : u + v ∈ (↑(adjoin R {x}) : Set A)), P (u + v) ⋯
mul₁ :
  ∀ (u v : A) (hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u)
    (hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v)
    (hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯) (hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v ⋯)
    (hy : u * v ∈ (↑(adjoin R {x}) : Set A)), P (u * v) ⋯
⊢ P y ⋯

Tactic:
induction hy using Algebra.adjoin_induction with
  | mem u hu =>
    obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu
    · exact self
    · simp_rw [← hu, star_star] at star_self
      exact star_self
  | algebraMap r => exact algebraMap r
  | add u v hu_mem hv_mem hu hv =>
    exact add u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
  | mul u v hu_mem hv_mem hu hv =>
    exact mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)

Premises used: star_star, rfl
-- 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 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
⊢ φ = ψ

Tactic:
StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_

Premises used: StarAlgHomClass.ext_topologicalClosure
-- 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 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
refine :
  ∀ (x : ↥(adjoin R {a})),
    Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
          ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
            ↥(topologicalClosure (adjoin R {a}))) :
        B)
      ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
          ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
            ↥(topologicalClosure (adjoin R {a}))) :
        B)
⊢ φ = ψ

Tactic:
refine StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_

Premises used: StarAlgHomClass.ext_topologicalClosure
-- 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 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x : ↥(adjoin R {a})
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)

Tactic:
adjoin_induction_subtype x ?_ ?_ ?_ ?_ ?_

Premises used: StarAlgebra.adjoin_induction_subtype
-- 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 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x : ↥(adjoin R {a})
y : A
hy : Membership.mem (γ := Set A) {a} y
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) y ⋯) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) y ⋯) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)

Tactic:
simpa only [Set.mem_singleton_iff.mp hy] using h

Premises used: Set.mem_singleton_iff, Iff.mp
-- 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 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x : ↥(adjoin R {a})
r : R
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
            ((algebraMap R ↥(adjoin R {a}) : (a_1 : R) → ↥(adjoin R {a})) r) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
            ((algebraMap R ↥(adjoin R {a}) : (a_1 : R) → ↥(adjoin R {a})) r) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)

Tactic:
simp only [AlgHomClass.commutes]

Premises used: AlgHomClass.commutes
-- 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 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x_1 x y : ↥(adjoin R {a})
hx :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
hy :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) y :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) y :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (x + y) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (x + y) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)

Tactic:
simp only [map_add, hx, hy]

Premises used: map_add