-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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})
refine_1 :
  ∀ (x : A) (h : Membership.mem (γ := Set A) {a} x),
    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) x ⋯) :
            ↥(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) x ⋯) :
            ↥(topologicalClosure (adjoin R {a}))) :
        B)
refine_2 :
  ∀ (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)
refine_3 :
  ∀ (x y : ↥(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) →
      Eq.{u_3 + 1} (α := B)
          ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
              ((inclusion ⋯ : (a_2 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) y :
                ↥(topologicalClosure (adjoin R {a}))) :
            B)
          ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
              ((inclusion ⋯ : (a_2 : ↥(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_3 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (x + y) :
                ↥(topologicalClosure (adjoin R {a}))) :
            B)
          ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
              ((inclusion ⋯ : (a_3 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (x + 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 :
          ↥(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)
have refine_4 : ∀ (x y : ↥(adjoin R {a})),
  Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
          ((inclusion sorry : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
            ↥(topologicalClosure (adjoin R {a}))) :
        B)
      ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
          ((inclusion sorry : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
            ↥(topologicalClosure (adjoin R {a}))) :
        B) →
    Eq.{u_3 + 1} (α := B)
        ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
            ((inclusion sorry : (a_2 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) y :
              ↥(topologicalClosure (adjoin R {a}))) :
          B)
        ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
            ((inclusion sorry : (a_2 : ↥(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 sorry : (a_3 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (x * y) :
              ↥(topologicalClosure (adjoin R {a}))) :
          B)
        ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
            ((inclusion sorry : (a_3 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) (x * y) :
              ↥(topologicalClosure (adjoin R {a}))) :
          B)
Tactic: refine adjoin_induction_subtype x ?_ ?_ ?_ ?_ ?_