awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
hf : f ⁻¹' {(1, 1)} = (↑(unitary R) : Set R)
⊢ IsClosed (↑(unitary R) : Set R)
have rw : IsClosed (f ⁻¹' {(1, 1)})
Tactic: rw [← hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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 (α := Set ↥S₂) (Subtype.val (p := fun (x : A) ↦ x ∈ S₂) ⁻¹' (↑S₁ : Set A))
    (Set.range (ι := ↥S₁) (⇑(inclusion h) : (a : ↥S₁) → ↥S₂))
have h₁ : (↑S₁ : Set A) = id '' {x : A | x ∈ S₁}
Tactic: convert! (Set.range_subtype_map id _).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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₁}
⊢ Eq (α := Set ↥S₂) (Subtype.val (p := fun (x : A) ↦ x ∈ S₂) ⁻¹' (↑S₁ : Set A))
    (Set.range (ι := ↥S₁) (⇑(inclusion h) : (a : ↥S₁) → ↥S₂))
have convert_4 : ∀ x ∈ S₁, id x ∈ S₂
Tactic: convert! (Set.range_subtype_map id _).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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) = id '' {x : A | x ∈ S₁}
have h₁ : (↑S₁ : Set A) = {x : A | x ∈ S₁}
Tactic: rw [Set.image_id]
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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
⊢ (star s).topologicalClosure = star s.topologicalClosure
have suffices : ∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.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)))
-- 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 : 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 ⋯)
⊢ φ = ψ
have rw : Eq (α := (a : ↥S.topologicalClosure) → B) (⇑φ : (a : ↥S.topologicalClosure) → B) (⇑ψ : (a : ↥S.topologicalClosure) → B)
Tactic: rw [DFunLike.ext'_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (hypothesis)
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 ⋯)
⊢ Eq (α := (a : ↥S.topologicalClosure) → B) (⇑φ : (a : ↥S.topologicalClosure) → B)
    (⇑ψ : (a : ↥S.topologicalClosure) → B)
have this : DenseRange (X := (↑(↑S.topologicalClosure : Set A) : Type u_2))
  (Set.inclusion (s := (↑S : Set A)) (t := (↑S.topologicalClosure : Set A)) sorry)
Tactic: have : DenseRange (Set.inclusion (le_topologicalClosure S)) := by simp [-SetLike.coe_sort_coe]
-- 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 : 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)
have 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)) sorry))
Tactic: refine Continuous.ext_on this hφ hψ ?_
-- 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 : 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)
have refine : ∀ (x : ↥S),
  Eq.{u_3 + 1} (α := B) ((StarAlgHom.comp (↑φ : ↥S.topologicalClosure →⋆ₐ[R] B) (inclusion sorry) : (a : ↥S) → B) x : B)
    ((StarAlgHom.comp (↑ψ : ↥S.topologicalClosure →⋆ₐ[R] B) (inclusion sorry) : (a : ↥S) → B) x : B)
Tactic: refine StarAlgHom.ext_topologicalClosure (R := R) (A := A) (B := B) hφ hψ (StarAlgHom.ext ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (hypothesis)
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)
⊢ φ = ψ
have this : 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
-- 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 : 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)
⊢ φ = ψ
have 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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 ⋯
⊢ P y hy
have apply : ∀ (y : A) (hy : y ∈ (↑(adjoin R {x}) : Set A)), P y sorry
Tactic: apply closure (adjoin R {x} : Set A) subset_closure (fun y hy ↦ ?_) y hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (hypothesis)
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)
⊢ P y ⋯
have hy₁ : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) y
Tactic: rw [SetLike.mem_coe, ← mem_toSubalgebra, adjoin_toSubalgebra] at hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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)
⊢ P u ⋯
have 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 sorry)
  (star_self : P (star u) sorry) (algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) sorry)
  (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) sorry)
  (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) sorry)
  (closure :
    ∀ (s : Set A) (hs : s ⊆ (↑(elemental R u) : Set A)),
      (∀ (u : A) (hu : u ∈ s), P u sorry) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v sorry)
  (hu : Membership.mem (γ := Set A) ({u} ∪ star {u}) u) (hy : u ∈ (↑(adjoin R {u}) : Set A)), P u sorry
Tactic: obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu
Cleared hypotheses: x, hy_1, P, self, star_self, algebraMap, add, mul, closure, hu, hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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 ⋯
⊢ P u ⋯
have mem₁ : ∀ (hu : star u = x), P u sorry
Tactic: obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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
⊢ P y ⋯
have mem : ∀ (u : A) (hu : Membership.mem (γ := Set A) ({x} ∪ star {x}) u) (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u sorry
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)
Cleared hypotheses: hy_2, hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
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 ⋯
⊢ P y ⋯
have 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) sorry
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)
Cleared hypotheses: hy_2, hy