awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NonUnitalStarSubalgebra R A
s : Set A
⊢ adjoin R s ≤ S ↔ s ⊆ (↑S : Set A)

Tactic:
NonUnitalStarAlgebra.gc _ _

Premises used: NonUnitalStarAlgebra.gc
-- 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 t : Set A
H : s ⊆ t
⊢ LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s) (adjoin R t)

Tactic:
NonUnitalStarAlgebra.gc.monotone_l H

Premises used: NonUnitalStarAlgebra.gc, GaloisConnection.monotone_l
-- 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 : NonUnitalStarSubalgebra R A
⊢ adjoin R (↑s : Set A) = s

Tactic:
le_antisymm (adjoin_le le_rfl) (subset_adjoin R (s : Set A))

Premises used: le_rfl, NonUnitalStarAlgebra.adjoin_le, NonUnitalStarAlgebra.subset_adjoin, le_antisymm, SetLike.coe
-- 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
rw :
  Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (NonUnitalAlgebra.adjoin R (s ∪ star s)))
    (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
rw₁ rw₂ :
  Eq (α := Submodule R A) (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
    (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))
⊢ Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (toNonUnitalSubalgebra (adjoin R s)))
    (Submodule.span R (↑(Subsemigroup.closure (s ∪ star s)) : Set A))

Tactic:
rw [adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span]

Premises used: NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
A : Type v
inst : NonUnitalSemiring A
inst_1 : StarRing A
R : Type u_1
inst_2 : CommSemiring R
inst_3 : Module R A
s : NonUnitalStarSubalgebra R A
⊢ Submodule.span R (↑s : Set A) = s.toSubmodule

Tactic:
simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

Premises used: SetLike.ext'_iff, Submodule.coe_span_eq_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 : NonUnitalSubalgebra R A
⊢ Eq (α := NonUnitalStarSubalgebra R A) S.starClosure (adjoin R (↑S : Set A))

Tactic:
le_antisymm (NonUnitalSubalgebra.starClosure_le_iff.2 <| subset_adjoin R (S : Set A))
    (adjoin_le (le_sup_left : S ≤ S ⊔ star S))

Premises used: Iff.mpr, le_sup_left, NonUnitalSubalgebra.starClosure_le_iff, NonUnitalStarAlgebra.adjoin_le, NonUnitalStarAlgebra.subset_adjoin, le_antisymm, SetLike.coe
-- 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
⊢ (↑⊤ : Set A) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, 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
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- 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
h :
  ∀ (x : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊤) x ↔
      Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x
⊢ Eq.{v + 1} (α := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊤) ⊤

Tactic:
ext
-- 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
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊤) x ↔
    Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x

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
S : NonUnitalStarSubalgebra R A
⊢ S.toNonUnitalSubalgebra = ⊤ ↔ S = ⊤

Tactic:
NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective.eq_iff' top_toNonUnitalSubalgebra

Premises used: NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective, Function.Injective.eq_iff', NonUnitalStarAlgebra.top_toNonUnitalSubalgebra
-- 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 T : NonUnitalStarSubalgebra R A
⊢ S ≤ S ⊔ T

Tactic:
le_sup_left

Premises used: le_sup_left
-- 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 T : NonUnitalStarSubalgebra R A
⊢ S ≤ S ⊔ T

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- 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 T : NonUnitalStarSubalgebra R A
⊢ T ≤ S ⊔ T

Tactic:
le_sup_right

Premises used: le_sup_right
-- 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 T : NonUnitalStarSubalgebra R A
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- 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 T : NonUnitalStarSubalgebra R A
x y : A
hx : x ∈ S
hy : y ∈ T
⊢ x * y ∈ S ⊔ T

Tactic:
mul_mem (mem_sup_left hx) (mem_sup_right hy)

Premises used: NonUnitalStarAlgebra.mem_sup_right, NonUnitalStarAlgebra.mem_sup_left, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B B
inst_15 : SMulCommClass R B B
inst_16 : StarModule R B
f : F
S T : NonUnitalStarSubalgebra R A
⊢ Eq (α := NonUnitalStarSubalgebra R B) (map f (S ⊔ T)) (map f S ⊔ map f T)

Tactic:
(NonUnitalStarSubalgebra.gc_map_comap f).l_sup

Premises used: NonUnitalStarSubalgebra.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B B
inst_15 : SMulCommClass R B B
inst_16 : StarModule R B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S T : NonUnitalStarSubalgebra R A
⊢ Eq (α := NonUnitalStarSubalgebra R B) (map f (S ⊓ T)) (map f S ⊓ map f T)

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, SetLike.coe_injective
-- 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 T : NonUnitalStarSubalgebra R A
⊢ (↑(S ⊓ T) : Set A) = (↑S : Set A) ∩ (↑T : Set A)

Tactic:
rfl

Premises used: setOf, Set.inter, 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 T : NonUnitalStarSubalgebra R A
x : A
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- 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 T : NonUnitalStarSubalgebra R A
⊢ (S ⊓ T).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra ⊓ T.toNonUnitalSubalgebra

Tactic:
SetLike.coe_injective <| coe_inf _ _

Premises used: SetLike.coe_injective, NonUnitalStarAlgebra.coe_inf
-- 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 (NonUnitalStarSubalgebra R A)
⊢ (↑(sInf S) : Set A) = ⋂ s ∈ S, (↑s : Set A)

Tactic:
sInf_image

Premises used: Set.iInter, setOf, sInf_image
-- 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 (NonUnitalStarSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

Premises used: NonUnitalStarAlgebra.coe_sInf, Set.mem_iInter₂, SetLike.mem_coe
-- 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 (NonUnitalStarSubalgebra R A)
⊢ (↑(sInf S).toNonUnitalSubalgebra : Set A) = (↑(sInf (toNonUnitalSubalgebra '' 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
ι : Sort u_1
S : ι → NonUnitalStarSubalgebra R A
⊢ (↑(⨅ (i : ι), S i) : Set A) = ⋂ (i : ι), (↑(S i) : Set A)

Tactic:
simp [iInf]

Premises used: iInf
-- 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
ι : Sort u_1
S : ι → NonUnitalStarSubalgebra R A
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, NonUnitalStarAlgebra.mem_sInf
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
ι : Sort u_1
inst_14 : Nonempty ι
inst_15 : IsScalarTower R B B
inst_16 : SMulCommClass R B B
inst_17 : StarModule R B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S : ι → NonUnitalStarSubalgebra R A
a : (↑(map f (⨅ (i : ι), S i)) : Set B) = (↑(⨅ (i : ι), map f (S i)) : Set B)
⊢ Eq (α := NonUnitalStarSubalgebra R B) (map f (⨅ (i : ι), S i)) (⨅ (i : ι), map f (S i))

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
ι : Sort u_1
inst_14 : Nonempty ι
inst_15 : IsScalarTower R B B
inst_16 : SMulCommClass R B B
inst_17 : StarModule R B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S : ι → NonUnitalStarSubalgebra R A
⊢ (↑(map f (⨅ (i : ι), S i)) : Set B) = (↑(⨅ (i : ι), map f (S i)) : Set B)

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ S)

Premises used: Set.InjOn.image_iInter_eq, Set.injOn_of_injective
-- 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
ι : Sort u_1
S : ι → NonUnitalStarSubalgebra R A
⊢ (↑(toNonUnitalSubalgebra (⨅ (i : ι), S i)) : Set A) = (↑(⨅ (i : ι), (S i).toNonUnitalSubalgebra) : 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
x : A
rw : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ ∅)) x ↔ x = 0
rw₁ : Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R ∅) x ↔ x = 0
rw₂ : Membership.mem (γ := NonUnitalSubalgebra R A) ⊥ x ↔ x = 0
rw₃ rw₄ : x = 0 ↔ x = 0
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (NonUnitalAlgebra.adjoin R (∅ ∪ star ∅)) x ↔ x = 0

Tactic:
rw [Set.star_empty, Set.union_empty, NonUnitalAlgebra.adjoin_empty, NonUnitalAlgebra.mem_bot]

Premises used: Set.union_empty, NonUnitalAlgebra.adjoin_empty, NonUnitalAlgebra.mem_bot, Set.star_empty
-- 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
h :
  ∀ (x : A),
    Membership.mem (γ := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊥) x ↔
      Membership.mem (γ := NonUnitalSubalgebra R A) ⊥ x
⊢ Eq.{v + 1} (α := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊥) ⊥

Tactic:
ext x
-- 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
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra ⊥) x ↔
    Membership.mem (γ := NonUnitalSubalgebra R A) ⊥ x

Tactic:
simp only [mem_bot, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, NonUnitalAlgebra.mem_bot]

Premises used: NonUnitalStarAlgebra.mem_bot, NonUnitalAlgebra.mem_bot, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra
-- 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
⊢ (↑⊥ : Set A) = {0}

Tactic:
simp only [Set.ext_iff, NonUnitalStarAlgebra.mem_bot, SetLike.mem_coe, Set.mem_singleton_iff,
    forall_const]

Premises used: NonUnitalStarAlgebra.mem_bot, Set.mem_singleton_iff, SetLike.mem_coe, forall_const, Set.ext_iff
-- 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 : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
rw : Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x
⊢ x ∈ S

Tactic:
rw [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 : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x

Tactic:
mem_top

Premises used: NonUnitalStarAlgebra.mem_top
-- 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 : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x

Tactic:
exact mem_top

Premises used: NonUnitalStarAlgebra.mem_top
-- 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 : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
h₁ : ∀ (x : A), x ∈ S ↔ Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x
⊢ S = ⊤

Tactic:
ext x
-- 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 : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x

Tactic:
⟨fun _ => mem_top, fun _ => h x⟩

Premises used: NonUnitalStarAlgebra.mem_top, Iff.intro
-- 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 : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ Membership.mem (γ := NonUnitalStarSubalgebra R A) ⊤ x

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩
-- 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
⊢ Eq (α := NonUnitalStarSubalgebra R A) (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[R] A) (NonUnitalStarAlgHom.id R A)) ⊤

Tactic:
SetLike.coe_injective Set.range_id

Premises used: SetLike.coe_injective, Set.range_id
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B B
inst_15 : SMulCommClass R B B
inst_16 : StarModule R B
f : F
⊢ (↑(map f ⊥) : Set B) = (↑⊥ : Set B)

Tactic:
simp [NonUnitalStarSubalgebra.coe_map]

Premises used: NonUnitalStarSubalgebra.coe_map
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B B
inst_15 : SMulCommClass R B B
inst_16 : StarModule R B
f : F
⊢ Eq (α := NonUnitalStarSubalgebra R A) (comap f ⊤) ⊤

Tactic:
eq_top_iff.2 fun _x => mem_top

Premises used: Iff.mpr, NonUnitalStarAlgebra.mem_top, NonUnitalStarAlgebra.eq_top_iff
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R B B
inst_12 : SMulCommClass R B B
inst_13 : StarModule R B
f : F
⊢ Eq (α := NonUnitalStarSubalgebra R B) (NonUnitalStarAlgHom.range f) ⊤ ↔
    Function.Surjective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
NonUnitalStarAlgebra.eq_top_iff

Premises used: Set.Mem, setOf, NonUnitalStarAlgebra.eq_top_iff, Set.range, Function.Surjective
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : NonUnitalSemiring B
inst_6 : StarRing B
inst_7 : Module R B
inst_8 : FunLike F A B
inst_9 : NonUnitalAlgHomClass F R A B
inst_10 : StarHomClass F A B
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
f : F
⊢ Eq (α := NonUnitalStarSubalgebra R B) (NonUnitalStarSubalgebra.map f ⊤) (NonUnitalStarAlgHom.range f)

Tactic:
SetLike.coe_injective Set.image_univ

Premises used: Set.image_univ, SetLike.coe_injective
-- 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
S T : NonUnitalStarSubalgebra R A
h : S ≤ T
⊢ Function.Injective (α := ↥S) (β := ↥T) (⇑(inclusion h) : (a : ↥S) → ↥T)

Tactic:
fun _ _ => Subtype.ext ∘ Subtype.mk.inj

Premises used: Function.comp, Subtype.mk.inj, Function.Injective, Subtype.ext