awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
rw : Set.centralizer (Set.univ ∪ star Set.univ) = (↑(center R A) : Set A)
rw₁ : Set.centralizer Set.univ = (↑(center R A) : Set A)
rw₂ : Set.centralizer Set.univ = Set.center A
rw₃ rw₄ : Set.center A = Set.center A
⊢ (↑(centralizer R Set.univ) : Set A) = (↑(center R A) : Set A)

Tactic:
rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]

Premises used: NonUnitalStarSubalgebra.coe_centralizer, Set.univ_union, NonUnitalStarSubalgebra.coe_center, Set.centralizer_univ
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
⊢ Eq (α := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra (centralizer R s))
    (NonUnitalSubalgebra.centralizer R (s ∪ star s))

Tactic:
rfl

Premises used: NonUnitalSubalgebra.centralizer, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
rw :
  ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
rw₁ : ((↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A)).centralizer = (s ∪ star s).centralizer.centralizer
rw₂ : (↑(centralizer R s) : Set A).centralizer = (s ∪ star s).centralizer.centralizer
rw₃ rw₄ : (s ∪ star s).centralizer.centralizer = (s ∪ star s).centralizer.centralizer
⊢ (↑(centralizer R (↑(centralizer R s) : Set A)) : Set A) = (s ∪ star s).centralizer.centralizer

Tactic:
rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]

Premises used: StarMemClass.star_coe_eq, NonUnitalStarSubalgebra.coe_centralizer, Set.union_self
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
⊢ LE.le (α := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s))
    (NonUnitalSubalgebra.centralizer R (↑(NonUnitalSubalgebra.centralizer R (s ∪ star s)) : Set A))

Tactic:
NonUnitalAlgebra.adjoin_le_centralizer_centralizer R (s ∪ star s)

Premises used: NonUnitalAlgebra.adjoin_le_centralizer_centralizer, Union.union, Star.star
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
h :
  (↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A) =
    (↑(NonUnitalSubalgebra.centralizer R (s ∪ star s)) : Set A)
⊢ LE.le (α := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (s ∪ star s))
    (NonUnitalSubalgebra.centralizer R ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)))

Tactic:
convert! NonUnitalAlgebra.adjoin_le_centralizer_centralizer R (s ∪ star s)

Premises used: NonUnitalAlgebra.adjoin_le_centralizer_centralizer, Union.union, Star.star
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
h :
  (↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A) =
    (↑(NonUnitalSubalgebra.centralizer R (s ∪ star s)) : Set A)
⊢ (↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A) =
    (↑(NonUnitalSubalgebra.centralizer R (s ∪ star s)) : Set A)

Tactic:
rw [StarMemClass.star_coe_eq]

Premises used: StarMemClass.star_coe_eq
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
⊢ (↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A) =
    (↑(NonUnitalSubalgebra.centralizer R (s ∪ star s)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
a b_1 : A
s : Set A
hb_1 : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) b_1
h : ∀ b ∈ s, Commute a b
h_star : ∀ b ∈ s, Commute a (star b)
b : A
hb : b ∈ s ∪ star s
⊢ b ∈ star s → Commute a b

Tactic:
simpa using h_star (star b)

Premises used: Star.star
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
a b c : A
hc : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R {b}) c
h : Commute a b
h_star : Commute a (star b)
⊢ ∀ (b_1 : A), Membership.mem (γ := Set A) {b} b_1 → Commute a b_1

Tactic:
simpa
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
a b c : A
hc : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R {b}) c
h : Commute a b
h_star : Commute a (star b)
⊢ ∀ (b_1 : A), Membership.mem (γ := Set A) {b} b_1 → Commute a (star b_1)

Tactic:
simpa
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
a b : A
inst_8 : IsStarNormal a
hb : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R {a}) b
⊢ Commute a b

Tactic:
commute_of_mem_adjoin_singleton_of_commute hb rfl (isStarNormal_iff a |>.mp inferInstance).symm

Premises used: isStarNormal_iff, inferInstance, NonUnitalStarAlgebra.commute_of_mem_adjoin_singleton_of_commute, Commute.symm, Iff.mp, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
⊢ LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))

Tactic:
have := adjoin_le_centralizer_centralizer R s
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
⊢ IsMulCommutative.{v} ↥(adjoin R s)

Tactic:
.of_setLike_mul_comm fun _ h₁ _ h₂ ↦ ?_

Premises used: IsMulCommutative.of_setLike_mul_comm
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
refine :
  ∀ (x : A) (h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x) (x_1 : A)
    (h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x_1), x * x_1 = x_1 * x
⊢ IsMulCommutative.{v} ↥(adjoin R s)

Tactic:
refine .of_setLike_mul_comm fun _ h₁ _ h₂ ↦ ?_
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x : A
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x
x_1 : A
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x_1
⊢ ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a

Tactic:
have hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a := fun a ha b hb ↦
    Set.union_star_self_comm (fun _ ha _ hb ↦ hcomm _ hb _ ha)
      (fun _ ha _ hb ↦ hcomm_star _ hb _ ha) b hb a ha
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x : A
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x
x_1 : A
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x_1
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x

Tactic:
apply this at h₁
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (adjoin R s) x_1
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1

Tactic:
apply this at h₂
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
⊢ x ∈ (s ∪ star s).centralizer.centralizer

Tactic:
rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂

Premises used: SetLike.mem_coe, NonUnitalStarSubalgebra.coe_centralizer_centralizer
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
h₂ : Membership.mem (γ := NonUnitalStarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
h₃ : x ∈ (s ∪ star s).centralizer.centralizer
⊢ x_1 ∈ (s ∪ star s).centralizer.centralizer

Tactic:
rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂

Premises used: SetLike.mem_coe, NonUnitalStarSubalgebra.coe_centralizer_centralizer
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x ∈ (s ∪ star s).centralizer.centralizer
h₂ : x_1 ∈ (s ∪ star s).centralizer.centralizer
⊢ x * x_1 = x_1 * x

Tactic:
Set.centralizer_centralizer_comm_of_comm hcomm _ h₁ _ h₂

Premises used: Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
s : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x ∈ (s ∪ star s).centralizer.centralizer
h₂ : x_1 ∈ (s ∪ star s).centralizer.centralizer
⊢ x * x_1 = x_1 * x

Tactic:
exact Set.centralizer_centralizer_comm_of_comm hcomm _ h₁ _ h₂

Premises used: Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
a : A
inst_8 : IsStarNormal a
⊢ ∀ (x : A), Membership.mem (γ := Set A) {a} x → ∀ (y : A), Membership.mem (γ := Set A) {a} y → x * y = y * x

Tactic:
simp
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
a : A
inst_8 : IsStarNormal a
⊢ ∀ (a_1 : A),
    Membership.mem (γ := Set A) {a} a_1 → ∀ (b : A), Membership.mem (γ := Set A) {a} b → a_1 * star b = star b * a_1

Tactic:
grind
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
S : Type u_1
inst_8 : SetLike S A
inst_9 : MulMemClass S A
inst_10 : StarMemClass S A
s : S
inst_11 : IsMulCommutative.{v} ↥s
⊢ IsMulCommutative.{v} ↥(adjoin R (↑s : Set A))

Tactic:
isMulCommutative_adjoin R
    (fun _ h₁ _ h₂ => setLike_mul_comm h₁ h₂)
    (fun _ h₁ _ h₂ => setLike_mul_comm h₁ (star_mem h₂))

Premises used: setLike_mul_comm, StarMemClass.star_mem, NonUnitalStarAlgebra.isMulCommutative_adjoin
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : Star R
p q : NonUnitalStarSubsemiring R
h :
  Eq.{v + 1} (α := Set R) ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s := p))
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s := q))
mk :
  ∀ (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
    (star_mem' : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring.carrier), star a ∈ toNonUnitalSubsemiring.carrier)
    (h :
      Eq.{v + 1} (α := Set R)
        ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
          { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
        ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s := q))),
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' : NonUnitalStarSubsemiring R } = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : Star R
q : NonUnitalStarSubsemiring R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
star_mem' : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring.carrier), star a ∈ toNonUnitalSubsemiring.carrier
h :
  Eq.{v + 1} (α := Set R)
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s := q))
mk :
  ∀ (toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R)
    (star_mem'_1 : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring_1.carrier), star a ∈ toNonUnitalSubsemiring_1.carrier)
    (h :
      Eq.{v + 1} (α := Set R)
        ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
          { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
        ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
          { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }))),
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' : NonUnitalStarSubsemiring R } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' : NonUnitalStarSubsemiring R } = q

Tactic:
cases q
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : Star R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
star_mem' : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring.carrier), star a ∈ toNonUnitalSubsemiring.carrier
toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R
star_mem'_1 : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring_1.carrier), star a ∈ toNonUnitalSubsemiring_1.carrier
h :
  Eq.{v + 1} (α := Set R)
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }))
mk : toNonUnitalSubsemiring = toNonUnitalSubsemiring_1
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' : NonUnitalStarSubsemiring R } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : Star R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
star_mem' : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring.carrier), star a ∈ toNonUnitalSubsemiring.carrier
toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R
star_mem'_1 : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring_1.carrier), star a ∈ toNonUnitalSubsemiring_1.carrier
h :
  Eq.{v + 1} (α := Set R)
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }))
⊢ toNonUnitalSubsemiring = toNonUnitalSubsemiring_1

Tactic:
SetLike.coe_injective h

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : Star R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
star_mem' : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring.carrier), star a ∈ toNonUnitalSubsemiring.carrier
toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R
star_mem'_1 : ∀ {a : R} (_ha : a ∈ toNonUnitalSubsemiring_1.carrier), star a ∈ toNonUnitalSubsemiring_1.carrier
h :
  Eq.{v + 1} (α := Set R)
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubsemiring R} ↦ s.carrier) (s :=
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := @star_mem'_1 }))
⊢ toNonUnitalSubsemiring = toNonUnitalSubsemiring_1

Tactic:
exact SetLike.coe_injective h

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
s : NonUnitalStarSubsemiring R
x : R
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
x : R
hx : x ∈ s
change : star x ∈ s
⊢ star x ∈ (S.copy s hs).carrier

Tactic:
change star x ∈ s

Premises used: Star.star
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
x : R
hx : x ∈ s
rw : ∀ (hx : x ∈ (↑S : Set R)), star x ∈ (↑S : Set R)
⊢ star x ∈ s

Tactic:
rw [hs] at hx ⊢
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
x : R
hx : x ∈ (↑S : Set R)
⊢ star x ∈ (↑S : Set R)

Tactic:
S.star_mem' hx

Premises used: Set.Mem, NonUnitalStarSubsemiring.star_mem'
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
A : Type v
B : Type w
C : Type w'
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
x : R
hx : x ∈ (↑S : Set R)
⊢ star x ∈ (↑S : Set R)

Tactic:
exact S.star_mem' hx

Premises used: NonUnitalStarSubsemiring.star_mem'
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
⊢ (↑(S.copy s hs) : Set R) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubsemiring
Goal:
R : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.Pi
Goal:
I : Type u
f : I → Type v
inst : (i : I) → AddMonoid (f i)
inst_1 : (i : I) → StarAddMonoid (f i)
inst_2 : DecidableEq I
i : I
a : f i
⊢ single (M := f) i (star a) = star (single (M := f) i a)

Tactic:
single_op (fun i => @star (f i) _) (fun _ => star_zero _) i a

Premises used: star_zero, Pi.single_op, Star.star