awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Star
Goal:
α : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
f : α → R
l : Filter α
y : R
h : Tendsto f l (𝓝 y)
⊢ Tendsto (fun (x : α) ↦ Star.star (f x)) l (𝓝 (Star.star y))

Tactic:
(continuous_star.tendsto y).comp h

Premises used: ContinuousStar.continuous_star, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Star
Goal:
α : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
inst_3 : TopologicalSpace α
f : α → R
hf : Continuous[inst_3, inst] f
⊢ Continuous[inst_3, inst] fun (x : α) ↦ Star.star (f x)

Tactic:
continuous_star.comp hf

Premises used: ContinuousStar.continuous_star, Continuous.comp
-- Module: Mathlib.Topology.Algebra.Star
Goal:
α : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
inst_3 : TopologicalSpace α
f : α → R
x : α
hf : ContinuousAt f x
⊢ ContinuousAt.{u_1, u_2} (Y := R) (fun (x : α) ↦ Star.star (f x)) x

Tactic:
continuousAt_star.comp hf

Premises used: ContinuousAt.comp, continuousAt_star
-- Module: Mathlib.Topology.Algebra.Star
Goal:
α : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
inst_3 : TopologicalSpace α
f : α → R
s : Set α
hf : ContinuousOn f s
⊢ ContinuousOn.{u_1, u_2} (Y := R) (fun (x : α) ↦ Star.star (f x)) s

Tactic:
continuous_star.comp_continuousOn hf

Premises used: ContinuousStar.continuous_star, Continuous.comp_continuousOn
-- Module: Mathlib.Topology.Algebra.Star
Goal:
α : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
inst_3 : TopologicalSpace α
f : α → R
s : Set α
x : α
hf : ContinuousWithinAt f s x
⊢ ContinuousWithinAt.{u_1, u_2} (Y := R) (fun (x : α) ↦ Star.star (f x)) s x

Tactic:
Filter.Tendsto.star hf

Premises used: ContinuousWithinAt, Filter.Tendsto.star
-- Module: Mathlib.Topology.Algebra.Star
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : Star R
inst_1 : Star S
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace S
inst_4 : ContinuousStar R
inst_5 : ContinuousStar S
⊢ ContinuousStar (R × S)

Tactic:
⟨(continuous_star.comp continuous_fst).prodMk (continuous_star.comp continuous_snd)⟩

Premises used: ContinuousStar.continuous_star, Continuous.comp, continuous_snd, continuous_fst, ContinuousStar.mk, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.Star
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : Star R
inst_1 : TopologicalSpace R
inst_2 : ContinuousStar R
⊢ ContinuousStar.{u_1} Rᵐᵒᵖ

Tactic:
⟨MulOpposite.continuous_op.comp <| MulOpposite.continuous_unop.star⟩

Premises used: Continuous.comp, ContinuousStar.mk, MulOpposite.continuous_unop, Continuous.star, MulOpposite.continuous_op
-- Module: Mathlib.Topology.Algebra.Star
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : ContinuousStar R
⊢ ContinuousStar.{u_1} Rˣ

Tactic:
⟨continuous_induced_rng.2 Units.continuous_embedProduct.star⟩

Premises used: Iff.mpr, ContinuousStar.mk, Units.continuous_embedProduct, Continuous.star, continuous_induced_rng
-- 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 : IsTopologicalSemiring A
s : StarSubalgebra R A
⊢ IsTopologicalSemiring.{u_2} ↥s

Tactic:
s.toSubalgebra.topologicalSemiring

Premises used: StarSubalgebra.toSubalgebra, Set.Mem, Subalgebra.toSubsemiring, Subsemiring.topologicalSemiring
-- 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
s : StarSubalgebra R A
⊢ IsSemitopologicalSemiring.{u_2} ↥s

Tactic:
s.toSubalgebra.semitopologicalSemiring

Premises used: StarSubalgebra.toSubalgebra, Subsemiring.semitopologicalSemiring, Set.Mem, Subalgebra.toSubsemiring
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed[inst_2] (↑S₁ : Set A)
⊢ Eq.{u_2 + 1} (α := Set ↥S₂) (Subtype.val (p := fun (x : A) ↦ x ∈ S₂) ⁻¹' id '' {x : A | x ∈ S₁})
    (Set.range (ι := ↥S₁) (Subtype.map (p := fun (x : A) ↦ x ∈ S₁) (q := fun (x : A) ↦ x ∈ S₂) id ⋯))

Tactic:
(Set.range_subtype_map id _).symm

Premises used: id, Set.range_subtype_map, Eq.symm
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed[inst_2] (↑S₁ : Set A)
h₁ : (↑S₁ : Set A) = id '' {x : A | x ∈ S₁}
convert_4 : ∀ x ∈ S₁, id x ∈ S₂
⊢ Eq (α := Set ↥S₂) (Subtype.val (p := fun (x : A) ↦ x ∈ S₂) ⁻¹' (↑S₁ : Set A))
    (Set.range (ι := ↥S₁) (⇑(inclusion h) : (a : ↥S₁) → ↥S₂))

Tactic:
convert! (Set.range_subtype_map id _).symm

Premises used: id, Set.range_subtype_map, Eq.symm
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed[inst_2] (↑S₁ : Set A)
h₁ : (↑S₁ : Set A) = {x : A | x ∈ S₁}
⊢ (↑S₁ : Set A) = id '' {x : A | x ∈ S₁}

Tactic:
rw [Set.image_id]

Premises used: Set.image_id
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed[inst_2] (↑S₁ : Set A)
⊢ (↑S₁ : Set A) = {x : A | x ∈ S₁}

Tactic:
rfl
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed[inst_2] (↑S₁ : Set A)
x : A
h' : x ∈ S₁
⊢ id x ∈ S₂

Tactic:
apply h h'
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s : StarSubalgebra R A
⊢ s.topologicalClosure.toSubalgebra = s.topologicalClosure

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s : StarSubalgebra R A
⊢ (↑s.topologicalClosure : Set A) = closure[inst_2] (↑s : Set A)

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s : StarSubalgebra R A
⊢ s ≤ s.topologicalClosure

Tactic:
subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s : StarSubalgebra R A
⊢ IsClosed[inst_2] (↑s.topologicalClosure : 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 : Algebra R A_1
inst_5 : StarRing A_1
inst_6 : StarModule R A_1
inst_7 : IsSemitopologicalSemiring A_1
inst_8 : ContinuousStar A_1
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : Algebra R B
inst_12 : StarRing 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
S : StarSubalgebra R A
⊢ CompleteSpace.{u_4} ↥S.topologicalClosure

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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s t : StarSubalgebra R A
h : s ≤ t
ht : IsClosed[inst_2] (↑t : Set A)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
⊢ Monotone.{u_2, u_2} (α := StarSubalgebra R A) topologicalClosure

Tactic:
fun _ S₂ h =>
  topologicalClosure_minimal (h.trans <| le_topologicalClosure S₂) (isClosed_topologicalClosure S₂)

Premises used: Monotone, StarSubalgebra.isClosed_topologicalClosure, StarSubalgebra.topologicalClosure_minimal, LE.le.trans, StarSubalgebra.le_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 : 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 : StarModule R B
inst_14 : IsSemitopologicalSemiring B
inst_15 : ContinuousStar B
s : StarSubalgebra R A
φ : A →⋆ₐ[R] B
hφ : IsClosedMap.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
⊢ LE.le (α := StarSubalgebra R B) (topologicalClosure (map φ s)) (map φ s.topologicalClosure)

Tactic:
hφ.closure_image_subset _

Premises used: IsClosedMap.closure_image_subset, Set.Mem, setOf, Set.Subset, closure, Set.image, Set.sInter
-- 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 : StarModule R B
inst_14 : IsSemitopologicalSemiring B
inst_15 : ContinuousStar B
s : StarSubalgebra R A
φ : A →⋆ₐ[R] B
hφ : Continuous[inst_2, inst_9] (⇑φ : (a : A) → B)
⊢ LE.le (α := StarSubalgebra R B) (map φ s.topologicalClosure) (topologicalClosure (map φ s))

Tactic:
image_closure_subset_closure_image hφ

Premises used: Set.Mem, setOf, Set.Subset, closure, image_closure_subset_closure_image, Set.image, Set.sInter
-- 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 : StarModule R B
inst_14 : IsSemitopologicalSemiring B
inst_15 : ContinuousStar B
s : StarSubalgebra R A
φ : A →⋆ₐ[R] B
hφ : IsClosedMap.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
hφ' : Continuous[inst_2, inst_9] (⇑φ : (a : A) → B)
⊢ Eq (α := StarSubalgebra R B) (topologicalClosure (map φ s)) (map φ s.topologicalClosure)

Tactic:
SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _

Premises used: SetLike.coe_injective, IsClosedMap.closure_image_eq_of_continuous
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
inst_9 : T2Space A
s : Set A
⊢ LE.le (α := StarSubalgebra R A) (topologicalClosure (adjoin R s)) (centralizer R (↑(centralizer R s) : Set A))

Tactic:
topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)

Premises used: StarAlgebra.adjoin_le_centralizer_centralizer, StarSubalgebra.topologicalClosure_minimal, Set.isClosed_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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s : Subalgebra R A
this : ∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.topologicalClosure
⊢ star s.topologicalClosure ≤ (star s).topologicalClosure

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

Premises used: star_star, Subalgebra.star_mono, 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s : Subalgebra R A
suffices : ∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.topologicalClosure
⊢ (star s).topologicalClosure = star s.topologicalClosure

Tactic:
suffices ∀ t : Subalgebra R A, (star t).topologicalClosure ≤ star t.topologicalClosure from
    le_antisymm (this s) (by simpa only [star_star] using Subalgebra.star_mono (this (star s)))
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s : Subalgebra R A
⊢ ∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.topologicalClosure

Tactic:
fun t => (star t).topologicalClosure_minimal (Subalgebra.star_mono subset_closure)
    (isClosed_closure.preimage continuous_star)

Premises used: ContinuousStar.continuous_star, subset_closure, Subalgebra.topologicalClosure_minimal, IsClosed.preimage, isClosed_closure, Subalgebra.star_mono
-- 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 : Algebra R A
inst_5 : StarRing A
inst_6 : StarModule R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : ContinuousStar A
s : Subalgebra R A
⊢ ∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.topologicalClosure

Tactic:
exact fun t => (star t).topologicalClosure_minimal (Subalgebra.star_mono subset_closure)
    (isClosed_closure.preimage continuous_star)
-- 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
S : StarSubalgebra R A
φ ψ : StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
rw :
  Eq (α := (a : ↥S.topologicalClosure) → B) (⇑φ : (a : ↥S.topologicalClosure) → B)
    (⇑ψ : (a : ↥S.topologicalClosure) → B)
⊢ φ = ψ

Tactic:
rw [DFunLike.ext'_iff]

Premises used: DFunLike.ext'_iff
-- 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
S : StarSubalgebra R A
φ ψ : StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
⊢ DenseRange (X := (↑(↑S.topologicalClosure : Set A) : Type u_2))
    (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) ⋯)

Tactic:
simp [-SetLike.coe_sort_coe]

Premises used: SetLike.coe_sort_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
S : StarSubalgebra R A
φ ψ : StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
⊢ DenseRange (X := (↑(↑S.topologicalClosure : Set A) : Type u_2))
    (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) ⋯)

Tactic:
have : DenseRange (Set.inclusion (le_topologicalClosure S)) := by simp [-SetLike.coe_sort_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
S : StarSubalgebra R A
φ ψ : StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
this :
  DenseRange (X := (↑(↑S.topologicalClosure : Set A) : Type u_2))
    (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) ⋯)
⊢ Eq (α := (a : ↥S.topologicalClosure) → B) (⇑φ : (a : ↥S.topologicalClosure) → B)
    (⇑ψ : (a : ↥S.topologicalClosure) → B)

Tactic:
Continuous.ext_on this hφ hψ ?_

Premises used: Continuous.ext_on
-- 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
S : StarSubalgebra R A
φ ψ : StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
this :
  DenseRange (X := (↑(↑S.topologicalClosure : Set A) : Type u_2))
    (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) ⋯)
refine :
  Set.EqOn.{u_2, u_3} (α := (↑(↑S.topologicalClosure : Set A) : Type u_2)) (β := B)
    (⇑φ : (a : ↥S.topologicalClosure) → B) (⇑ψ : (a : ↥S.topologicalClosure) → B)
    (Set.range (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) ⋯))
⊢ Eq (α := (a : ↥S.topologicalClosure) → B) (⇑φ : (a : ↥S.topologicalClosure) → B)
    (⇑ψ : (a : ↥S.topologicalClosure) → B)

Tactic:
refine Continuous.ext_on this hφ hψ ?_

Premises used: Continuous.ext_on
-- 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
S : StarSubalgebra R A
φ ψ : StarAlgHom.{u_1, u_2, u_3} R (↥S.topologicalClosure) B
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥S.topologicalClosure) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥S.topologicalClosure) → B)
h : φ.comp (inclusion ⋯) = ψ.comp (inclusion ⋯)
this :
  DenseRange (X := (↑(↑S.topologicalClosure : Set A) : Type u_2))
    (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) ⋯)
x : (↑(↑S : Set A) : Type u_2)
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥S.topologicalClosure) → B)
        (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) ⋯ x) :
      B)
    ((ψ : (a : ↥S.topologicalClosure) → B)
        (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) ⋯ x) :
      B)

Tactic:
simpa only using DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- 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:
StarAlgHom.ext_topologicalClosure (R := R) (A := A) (B := B) hφ hψ (StarAlgHom.ext ?_)

Premises used: StarAlgHom.ext_topologicalClosure, StarAlgHom.ext