awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
p q : StarSubalgebra R A
h :
  Eq.{u_3 + 1} (α := Set A) ((fun (S : StarSubalgebra R A) ↦ S.carrier) p)
    ((fun (S : StarSubalgebra R A) ↦ S.carrier) q)
obtain :
  ∀ (carrier : Set A) (mul_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier)
    (one_mem' : 1 ∈ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup A }.carrier)
    (add_mem' :
      ∀ {a b : A},
        a ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
          b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
            a + b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier)
    (zero_mem' : 0 ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier)
    (algebraMap_mem' :
      ∀ (r : R),
        Membership.mem (α := A)
          { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
              zero_mem' := zero_mem' : Subsemiring A }.carrier
          ((algebraMap R A : (a : R) → A) r : A))
    (star_mem' :
      ∀ {a : A},
        a ∈
            { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
                zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier →
          star a ∈
            { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
                zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier)
    (h :
      Eq.{u_3 + 1} (α := Set A)
        ((fun (S : StarSubalgebra R A) ↦ S.carrier)
          { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' })
        ((fun (S : StarSubalgebra R A) ↦ S.carrier) q)),
    { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
        algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' } =
      q
⊢ p = q

Tactic:
obtain ⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩ := p
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
q : StarSubalgebra R A
carrier : Set A
mul_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
one_mem' : 1 ∈ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup A }.carrier
add_mem' :
  ∀ {a b : A},
    a ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
      b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
        a + b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier
zero_mem' : 0 ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier
algebraMap_mem' :
  ∀ (r : R),
    Membership.mem (α := A)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem' :
          Subsemiring A }.carrier
      ((algebraMap R A : (a : R) → A) r : A)
star_mem' :
  ∀ {a : A},
    a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier →
      star a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier
h :
  Eq.{u_3 + 1} (α := Set A)
    ((fun (S : StarSubalgebra R A) ↦ S.carrier)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
        algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' })
    ((fun (S : StarSubalgebra R A) ↦ S.carrier) q)
mk :
  ∀ (toSubalgebra : Subalgebra R A) (star_mem'_1 : ∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier)
    (h :
      Eq.{u_3 + 1} (α := Set A)
        ((fun (S : StarSubalgebra R A) ↦ S.carrier)
          { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' })
        ((fun (S : StarSubalgebra R A) ↦ S.carrier) { toSubalgebra := toSubalgebra, star_mem' := @star_mem'_1 })),
    Eq (α := StarSubalgebra R A)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
        algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' }
      { toSubalgebra := toSubalgebra, star_mem' := @star_mem'_1 }
⊢ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' } =
    q

Tactic:
cases q
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
carrier : Set A
mul_mem' : ∀ {a b : A}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
one_mem' : 1 ∈ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup A }.carrier
add_mem' :
  ∀ {a b : A},
    a ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
      b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier →
        a + b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier
zero_mem' : 0 ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid A }.carrier
algebraMap_mem' :
  ∀ (r : R),
    Membership.mem (α := A)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem' :
          Subsemiring A }.carrier
      ((algebraMap R A : (a : R) → A) r : A)
star_mem' :
  ∀ {a : A},
    a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier →
      star a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem', algebraMap_mem' := algebraMap_mem' : Subalgebra R A }.carrier
toSubalgebra : Subalgebra R A
star_mem'_1 : ∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier
h :
  Eq.{u_3 + 1} (α := Set A)
    ((fun (S : StarSubalgebra R A) ↦ S.carrier)
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
        algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' })
    ((fun (S : StarSubalgebra R A) ↦ S.carrier) { toSubalgebra := toSubalgebra, star_mem' := @star_mem'_1 })
⊢ Eq (α := StarSubalgebra R A)
    { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      algebraMap_mem' := algebraMap_mem', star_mem' := @star_mem' }
    { toSubalgebra := toSubalgebra, star_mem' := @star_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧
      (∀ (r : R), Membership.mem (α := A) s ((algebraMap R A : (a : R) → A) r : A)) ∧ ∀ {x : A}, x ∈ s → star x ∈ s
⊢ 1 ∈ s

Tactic:
simpa using h.2.2.1 1

Premises used: And.right, And.left, OfNat.ofNat
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧
      (∀ (r : R), Membership.mem (α := A) s ((algebraMap R A : (a : R) → A) r : A)) ∧ ∀ {x : A}, x ∈ s → star x ∈ s
⊢ 0 ∈ s

Tactic:
simpa using h.2.2.1 0

Premises used: And.right, And.left, OfNat.ofNat
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ 1 ∈ S.toNonUnitalStarSubalgebra

Tactic:
S.one_mem'

Premises used: StarSubalgebra.toSubalgebra, Set.Mem, Subalgebra.toSubsemiring, Subsemiring.toSubmonoid, Submonoid.one_mem'
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
x : A
⊢ x ∈ S.toNonUnitalStarSubalgebra ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
x x_1 : StarSubalgebra R A
⊢ x.toNonUnitalStarSubalgebra = x_1.toNonUnitalStarSubalgebra → x = x_1

Tactic:
simp [SetLike.ext_iff]

Premises used: SetLike.ext_iff
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S U : StarSubalgebra R A
⊢ S.toNonUnitalStarSubalgebra = U.toNonUnitalStarSubalgebra ↔ S = U

Tactic:
toNonUnitalStarSubalgebra_injective.eq_iff

Premises used: StarSubalgebra.toNonUnitalStarSubalgebra_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
s : StarSubalgebra R A
x : A
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S T : StarSubalgebra R A
h : ∀ (x : A), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : Subalgebra R A
h : ∀ {a : A}, a ∈ S.carrier → star a ∈ S.carrier
⊢ (↑{ toSubalgebra := S, star_mem' := @h : StarSubalgebra R A } : Set A) = (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
x : A
⊢ x ∈ S.toSubalgebra ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ (↑S.toSubalgebra : Set A) = (↑S : Set A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
rw : x ∈ S.toSubalgebra ↔ x ∈ T
rw₁ : x ∈ S.toSubalgebra ↔ x ∈ T.toSubalgebra
rw₂ rw₃ : x ∈ T.toSubalgebra ↔ x ∈ T.toSubalgebra
⊢ x ∈ S ↔ x ∈ T

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

Premises used: StarSubalgebra.mem_toSubalgebra
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S U : StarSubalgebra R A
⊢ S.toSubalgebra = U.toSubalgebra ↔ S = U

Tactic:
toSubalgebra_injective.eq_iff

Premises used: Function.Injective.eq_iff, StarSubalgebra.toSubalgebra_injective
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S₁ S₂ : StarSubalgebra R A
⊢ S₁.toSubalgebra ≤ S₂.toSubalgebra ↔ S₁ ≤ S₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
S : StarSubalgebra R A
s : Set A
hs : s = (↑S : Set A)
a : A
ha : a ∈ (S.copy s hs).carrier
⊢ a ∈ S.carrier

Tactic:
simpa [hs] using ha
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
S : StarSubalgebra R A
a : A
hs : (↑S : Set A) = (↑S : Set A)
__Subalgebra : Subalgebra R A := S.copy (↑S : Set A) hs
ha : a ∈ (S.copy (↑S : Set A) hs).carrier
⊢ a ∈ S.carrier

Tactic:
simpa [hs] using ha
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra 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.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra 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.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
r : R
⊢ Membership.mem (α := A) S ((algebraMap R A : (a : R) → A) r : A)

Tactic:
S.algebraMap_mem' r

Premises used: StarSubalgebra.toSubalgebra, Set.Mem, Subalgebra.algebraMap_mem'
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ RingHom.rangeS (algebraMap R A) ≤ S.toSubsemiring

Tactic:
fun _x ⟨r, hr⟩ =>
  hr ▸ S.algebraMap_mem r

Premises used: StarSubalgebra.toSubalgebra, Membership.mem, Eq.rec, Subalgebra.toSubsemiring, StarSubalgebra.algebraMap_mem, _private.0.StarSubalgebra.rangeS_le.match_1
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ⊆ (↑S : Set A)

Tactic:
fun _x ⟨r, hr⟩ => hr ▸ S.algebraMap_mem r

Premises used: Membership.mem, Eq.rec, Set.Subset, _private.0.StarSubalgebra.range_subset.match_1, StarSubalgebra.algebraMap_mem, SetLike.coe
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ≤ (↑S : Set A)

Tactic:
S.range_subset

Premises used: StarSubalgebra.range_subset
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
x : A
hx : x ∈ S
r : R
⊢ r • x ∈ S

Tactic:
(Algebra.smul_def r x).symm ▸ mul_mem (S.algebraMap_mem r) hx

Premises used: Eq.rec, StarSubalgebra.algebraMap_mem, Algebra.smul_def, Eq.symm, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ Eq (α := (a : ↥S) → A) (⇑S.subtype : (a : ↥S) → A) (Subtype.val (p := fun (x : A) ↦ x ∈ S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
x : ↥S
⊢ (S.subtype : (a : ↥S) → A) x = (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ S.val = (↑S.subtype : ↥S →ₐ[R] A)

Tactic:
rfl

Premises used: Set.Mem, Subalgebra.val, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
⊢ Function.Injective (α := ↥S₁) (β := ↥S₂) (⇑(inclusion h) : (a : ↥S₁) → ↥S₂)

Tactic:
Set.inclusion_injective h

Premises used: Subtype.map, Set.inclusion_injective
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
⊢ S₂.subtype.comp (inclusion h) = S₁.subtype

Tactic:
rfl

Premises used: Set.Mem, StarSubalgebra.subtype, StarAlgHom.comp, AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
S_1 : StarSubalgebra R A
f : A →⋆ₐ[R] B
S : StarSubalgebra R A
a : A
ha : a ∈ (↑S.toSubsemiring : Set A)
⊢ Membership.mem (α := B) (Subalgebra.map (↑f : A →ₐ[R] B) S.toSubalgebra).carrier
    (star (((↑(↑f : A →ₐ[R] B) : A →+* B) : (a : A) → B) a) : B)

Tactic:
map_star f a ▸ Set.mem_image_of_mem _ (S.star_mem' ha)

Premises used: Set.Mem, Eq.rec, StarHomClass.map_star, StarSubalgebra.star_mem', Set.mem_image_of_mem
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
S_1 : StarSubalgebra R A
f : A →⋆ₐ[R] B
S : StarSubalgebra R A
a : A
ha : a ∈ (↑S.toSubsemiring : Set A)
⊢ Membership.mem (α := B) (Subalgebra.map (↑f : A →ₐ[R] B) S.toSubalgebra).carrier
    (star (((↑(↑f : A →ₐ[R] B) : A →+* B) : (a : A) → B) a) : B)

Tactic:
exact map_star f a ▸ Set.mem_image_of_mem _ (S.star_mem' ha)
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
S₁ S₂ : StarSubalgebra R A
f : A →⋆ₐ[R] B
⊢ S₁ ≤ S₂ → LE.le (α := StarSubalgebra R B) (map f S₁) (map f S₂)

Tactic:
Set.image_mono

Premises used: Set.Mem, Set.image_mono, setOf, Set.Subset, Set.image
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
f : A →⋆ₐ[R] B
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Injective (α := StarSubalgebra R A) (β := StarSubalgebra R B) (map f)

Tactic:
fun _S₁ _S₂ ih =>
  ext <| Set.ext_iff.1 <| Set.image_injective.2 hf <| Set.ext <| SetLike.ext_iff.mp ih

Premises used: Iff.mpr, Set.ext, Set.image_injective, SetLike.ext_iff, StarSubalgebra.ext, Iff.mp, Set.ext_iff, Function.Injective
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ map (StarAlgHom.id R A) S = S

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
inst_10 : Semiring C
inst_11 : StarRing C
inst_12 : Algebra R C
inst_13 : StarModule R C
S : StarSubalgebra R A
g : B →⋆ₐ[R] C
f : A →⋆ₐ[R] B
⊢ Eq (α := StarSubalgebra R C) (map g (map f S)) (map (g.comp f) S)

Tactic:
SetLike.coe_injective <| Set.image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
inst_6 : Semiring B
inst_7 : StarRing B
inst_8 : Algebra R B
inst_9 : StarModule R B
S : StarSubalgebra R A
f : A →⋆ₐ[R] B
y : B
⊢ Membership.mem (γ := StarSubalgebra R B) (map f S) y ↔ ∃ x ∈ S, (f : (a : A) → B) x = y

Tactic:
Subsemiring.mem_map

Premises used: Set.Mem, Subsemiring.mem_map