awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Mul D
inst_4 : Star A
inst_5 : Star B
inst_6 : Star C
inst_7 : Star D
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
a : A
rw : e₂.toFun (star (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
rw₁ rw₂ : star (e₂.toFun (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
⊢ e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a))

Tactic:
rw [e₁.map_star', e₂.map_star']

Premises used: StarMulEquiv.map_star'
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
e : A ≃⋆* B
⊢ ∀ (x : B), (e : (a : A) → B) ((e.symm : (a : B) → A) x : A) = x

Tactic:
e.toMulEquiv.apply_symm_apply

Premises used: StarMulEquiv.toMulEquiv, MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
e : A ≃⋆* B
⊢ ∀ (x : A), (e.symm : (a : B) → A) ((e : (a : A) → B) x : B) = x

Tactic:
e.toMulEquiv.symm_apply_apply

Premises used: StarMulEquiv.toMulEquiv, MulEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Star A
inst_4 : Star B
inst_5 : Star C
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
x : C
⊢ Eq.{u_2 + 1} (α := A) (((e₁.trans e₂).symm : (a : C) → A) x : A)
    ((e₁.symm : (a : B) → A) ((e₂.symm : (a : C) → B) x : B) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Star A
inst_4 : Star B
inst_5 : Star C
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
⊢ Eq (α := (a : A) → C) (⇑(e₁.trans e₂) : (a : A) → C)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := B) (⇑e₂ : (a : B) → C) (⇑e₁ : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Star A
inst_4 : Star B
inst_5 : Star C
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
x : A
⊢ Eq.{u_4 + 1} (α := C) ((e₁.trans e₂ : (a : A) → C) x : C) ((e₂ : (a : B) → C) ((e₁ : (a : A) → B) x : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Mul A
inst_1 : Mul B
inst_2 : Mul C
inst_3 : Star A
inst_4 : Star B
inst_5 : Star C
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
⊢ (e₁.trans e₂).toMulEquiv = e₁.trans e₂.toMulEquiv

Tactic:
rfl

Premises used: MulEquiv.trans, rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
e : A ≃⋆* B
⊢ Function.LeftInverse.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑e.symm : (a : B) → A) (⇑e : (a : A) → B)

Tactic:
e.left_inv

Premises used: StarMulEquiv.toMulEquiv, MulEquiv.toEquiv, Equiv.left_inv
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Mul A
inst_1 : Mul B
inst_2 : Star A
inst_3 : Star B
e : A ≃⋆* B
⊢ Function.RightInverse.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑e.symm : (a : B) → A) (⇑e : (a : A) → B)

Tactic:
e.right_inv

Premises used: Equiv.right_inv, StarMulEquiv.toMulEquiv, MulEquiv.toEquiv
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : Star A
inst_3 : Star B
f : A →⋆* B
hf : Function.Bijective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Eq (α := (a : A) → B) (⇑(ofBijective f hf) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.MonoidHom
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : Star A
inst_3 : Star B
f : A →⋆* B
hf : Function.Bijective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
⊢ Eq.{u_3 + 1} (α := B) ((ofBijective f hf : (a : A) → B) a : B) ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Star A
inst_3 : Module R A
S : Type w''
inst_4 : SetLike S A
inst_5 : NonUnitalSubsemiringClass S A
hSR : SMulMemClass S R A
inst_6 : StarMemClass S A
s : S
x : ↥s
⊢ (subtype s : (a : ↥s) → A) x = (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Star A
inst_3 : Module R A
S : Type w''
inst_4 : SetLike S A
inst_5 : NonUnitalSubsemiringClass S A
hSR : SMulMemClass S R A
inst_6 : StarMemClass S A
s : S
⊢ Function.Injective (α := ↥s) (β := A) (⇑(subtype s) : (a : ↥s) → A)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Star A
inst_3 : Module R A
S : Type w''
inst_4 : SetLike S A
inst_5 : NonUnitalSubsemiringClass S A
hSR : SMulMemClass S R A
inst_6 : StarMemClass S A
s : S
⊢ Eq (α := (a : ↥s) → A) (⇑(subtype s) : (a : ↥s) → A) (Subtype.val (p := fun (x : A) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
p q : NonUnitalStarSubalgebra R A
h :
  Eq.{v + 1} (α := Set A) ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s := p))
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s := q))
mk :
  ∀ (toNonUnitalSubalgebra : NonUnitalSubalgebra R A)
    (star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier)
    (h :
      Eq.{v + 1} (α := Set A)
        ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
          { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
        ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s := q))),
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A } = q
⊢ p = q

Tactic:
cases p
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
q : NonUnitalStarSubalgebra R A
toNonUnitalSubalgebra : NonUnitalSubalgebra R A
star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier
h :
  Eq.{v + 1} (α := Set A)
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s := q))
mk :
  ∀ (toNonUnitalSubalgebra_1 : NonUnitalSubalgebra R A)
    (star_mem'_1 : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra_1.carrier), star a ∈ toNonUnitalSubalgebra_1.carrier)
    (h :
      Eq.{v + 1} (α := Set A)
        ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
          { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
        ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
          { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }))),
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A } =
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A } = q

Tactic:
cases q
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
toNonUnitalSubalgebra : NonUnitalSubalgebra R A
star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier
toNonUnitalSubalgebra_1 : NonUnitalSubalgebra R A
star_mem'_1 : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra_1.carrier), star a ∈ toNonUnitalSubalgebra_1.carrier
h :
  Eq.{v + 1} (α := Set A)
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }))
mk : toNonUnitalSubalgebra = toNonUnitalSubalgebra_1
⊢ { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A } =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }

Tactic:
congr
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
toNonUnitalSubalgebra : NonUnitalSubalgebra R A
star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier
toNonUnitalSubalgebra_1 : NonUnitalSubalgebra R A
star_mem'_1 : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra_1.carrier), star a ∈ toNonUnitalSubalgebra_1.carrier
h :
  Eq.{v + 1} (α := Set A)
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }))
⊢ toNonUnitalSubalgebra = toNonUnitalSubalgebra_1

Tactic:
SetLike.coe_injective h

Premises used: SetLike.coe_injective
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
toNonUnitalSubalgebra : NonUnitalSubalgebra R A
star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier
toNonUnitalSubalgebra_1 : NonUnitalSubalgebra R A
star_mem'_1 : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra_1.carrier), star a ∈ toNonUnitalSubalgebra_1.carrier
h :
  Eq.{v + 1} (α := Set A)
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }))
    ((fun {s : NonUnitalStarSubalgebra R A} ↦ s.carrier) (s :=
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := @star_mem'_1 }))
⊢ toNonUnitalSubalgebra = toNonUnitalSubalgebra_1

Tactic:
exact SetLike.coe_injective h

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R_1 : Type u
A_1 : Type v
B : Type w
C : Type w'
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : Module R_1 A_1
inst_3 : Star A_1
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R_1 B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R_1 C
inst_9 : Star C
inst_10 : FunLike F A_1 B
inst_11 : NonUnitalAlgHomClass F R_1 A_1 B
inst_12 : StarHomClass F A_1 B
R : Type u
A : Type v
inst_13 : CommRing R
inst_14 : NonUnitalNonAssocRing A
inst_15 : Module R A
inst_16 : Star A
⊢ NonUnitalSubringClass (NonUnitalStarSubalgebra R A) A

Tactic:
{ NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass with
    neg_mem := fun _S {x} hx => neg_one_smul R x ▸ SMulMemClass.smul_mem _ hx }

Premises used: NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass, NonUnitalSubringClass.mk
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
s : NonUnitalStarSubalgebra R A
x : A
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
x : A
⊢ x ∈ S.toNonUnitalSubalgebra ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
⊢ (↑S.toNonUnitalSubalgebra : Set A) = (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubalgebra = T.toNonUnitalSubalgebra
x : A
rw : x ∈ S.toNonUnitalSubalgebra ↔ x ∈ T
rw₁ : x ∈ S.toNonUnitalSubalgebra ↔ x ∈ T.toNonUnitalSubalgebra
rw₂ rw₃ : x ∈ T.toNonUnitalSubalgebra ↔ x ∈ T.toNonUnitalSubalgebra
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubalgebra, ← mem_toNonUnitalSubalgebra, h]

Premises used: NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S U : NonUnitalStarSubalgebra R A
⊢ S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra ↔ S = U

Tactic:
toNonUnitalSubalgebra_injective.eq_iff

Premises used: Function.Injective.eq_iff, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S₁ S₂ : NonUnitalStarSubalgebra R A
⊢ S₁.toNonUnitalSubalgebra ≤ S₂.toNonUnitalSubalgebra ↔ S₁ ≤ S₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
x : A
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.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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
x : A
hx : x ∈ s
rw : ∀ (hx : x ∈ (↑S : Set A)), star x ∈ (↑S : Set A)
⊢ star x ∈ s

Tactic:
rw [hs] at hx ⊢
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
x : A
hx : x ∈ (↑S : Set A)
⊢ star x ∈ (↑S : Set A)

Tactic:
S.star_mem' hx

Premises used: Set.Mem, NonUnitalStarSubalgebra.star_mem'
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
x : A
hx : x ∈ (↑S : Set A)
⊢ star x ∈ (↑S : Set A)

Tactic:
exact S.star_mem' hx

Premises used: NonUnitalStarSubalgebra.star_mem'
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
⊢ (↑(S.copy s hs) : Set A) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
x : A
⊢ x ∈ S.toNonUnitalSubring ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
⊢ (↑S.toNonUnitalSubring : Set A) = (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
rw : x ∈ S.toNonUnitalSubring ↔ x ∈ T
rw₁ : x ∈ S.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
rw₂ rw₃ : x ∈ T.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

Premises used: NonUnitalStarSubalgebra.mem_toNonUnitalSubring
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Star A
S U : NonUnitalStarSubalgebra R A
⊢ S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U

Tactic:
toNonUnitalSubring_injective.eq_iff

Premises used: Function.Injective.eq_iff, NonUnitalStarSubalgebra.toNonUnitalSubring_injective
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S_1 S T : NonUnitalStarSubalgebra R A
h :
  Eq.{v + 1} (α := NonUnitalSubalgebra R A) ((fun (S : NonUnitalStarSubalgebra R A) ↦ S.toNonUnitalSubalgebra) S)
    ((fun (S : NonUnitalStarSubalgebra R A) ↦ S.toNonUnitalSubalgebra) T)
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
apply SetLike.ext_iff.1 h

Premises used: SetLike.ext_iff, Iff.mp
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
inst_13 : Semiring R'
inst_14 : SMul R' R
inst_15 : Module R' A
inst_16 : IsScalarTower R' R A
⊢ IsScalarTower.{u', u, v} R' R ↥S

Tactic:
S.toNonUnitalSubalgebra.instIsScalarTower'

Premises used: NonUnitalSubalgebra.instIsScalarTower', Set.Mem
-- 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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : Module R C
inst_9 : Star C
inst_10 : FunLike F A B
inst_11 : NonUnitalAlgHomClass F R A B
inst_12 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
inst_13 : IsTorsionFree R A
⊢ ∀ (r : R) (m : ↥S), (↑(r • m) : A) = r • (↑m : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
x y : ↥S
⊢ (↑(x + y) : A) = (↑x : A) + (↑y : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
x y : ↥S
⊢ (↑(x * y) : A) = (↑x : A) * (↑y : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
⊢ Eq.{v + 1} (α := A) (↑0 : A) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
x : ↥S
⊢ (↑(-x) : A) = -(↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
x y : ↥S
⊢ (↑(x - y) : A) = (↑x : A) - (↑y : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R' : Type u'
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
inst_4 : SMul R' R
inst_5 : SMul R' A
inst_6 : IsScalarTower R' R A
r : R'
x : ↥S
⊢ (↑(r • x) : A) = r • (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
x : ↥S
⊢ (↑x : A) = 0 ↔ x = 0

Tactic:
ZeroMemClass.coe_eq_zero

Premises used: ZeroMemClass.coe_eq_zero