awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := ↥S →ₙₐ[R] A) (NonUnitalSubalgebraClass.subtype S)
    (NonUnitalAlgHomClass.toNonUnitalAlgHom (F := ↥S →⋆ₙₐ[R] A) (NonUnitalStarSubalgebraClass.subtype S))

Tactic:
rfl

Premises used: NonUnitalSubalgebraClass.subtype, rfl, NonUnitalAlgHomClass.toNonUnitalAlgHom
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
⊢ Eq (α := ↥S →ₙ+* A) (NonUnitalSubringClass.subtype S) (↑(NonUnitalStarSubalgebraClass.subtype S) : ↥S →ₙ+* A)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, NonUnitalSubringClass.subtype, NonUnitalRingHomClass.toNonUnitalRingHom, 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_1 : NonUnitalStarSubalgebra R A
f : F
S : NonUnitalStarSubalgebra R A
a : A
ha : a ∈ (↑S.toNonUnitalSubsemiring : Set A)
⊢ Membership.mem.{w, w} (α := B) (γ := Set B)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring
            (NonUnitalSubalgebra.map (F := A →ₙₐ[R] B) (NonUnitalAlgHomClass.toNonUnitalAlgHom f)
              S.toNonUnitalSubalgebra)))))
    (star (((↑(NonUnitalAlgHomClass.toNonUnitalAlgHom f) : A →ₙ+* B) : (a : A) → B) a) : B)

Tactic:
⟨star a, star_mem (s := S) ha, map_star f a⟩

Premises used: Set.Mem, setOf, StarMemClass.star_mem, StarHomClass.map_star, And.intro, Exists.intro, Set.image, 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_1 : NonUnitalStarSubalgebra R A
f : F
S : NonUnitalStarSubalgebra R A
a : A
ha : a ∈ (↑S.toNonUnitalSubsemiring : Set A)
⊢ Membership.mem.{w, w} (α := B) (γ := Set B)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring
            (NonUnitalSubalgebra.map (F := A →ₙₐ[R] B) (NonUnitalAlgHomClass.toNonUnitalAlgHom f)
              S.toNonUnitalSubalgebra)))))
    (star (((↑(NonUnitalAlgHomClass.toNonUnitalAlgHom f) : A →ₙ+* B) : (a : A) → B) a) : B)

Tactic:
exact ⟨star a, star_mem (s := S) ha, map_star f a⟩
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S₁ S₂ : NonUnitalStarSubalgebra R A
f : F
⊢ S₁ ≤ S₂ → LE.le (α := NonUnitalStarSubalgebra 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.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Injective (α := NonUnitalStarSubalgebra R A) (β := NonUnitalStarSubalgebra 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, NonUnitalStarSubalgebra.ext, SetLike.ext_iff, Iff.mp, Set.ext_iff, Function.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 : NonUnitalStarSubalgebra R A
⊢ map (F := A →⋆ₙₐ[R] A) (NonUnitalStarAlgHom.id R A) S = S

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
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
S : NonUnitalStarSubalgebra R A
g : B →⋆ₙₐ[R] C
f : A →⋆ₙₐ[R] B
⊢ Eq (α := NonUnitalStarSubalgebra 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.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
f : F
y : B
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R B) (map f S) y ↔ ∃ x ∈ S, (f : (a : A) → B) x = y

Tactic:
NonUnitalSubalgebra.mem_map

Premises used: Set.Mem, NonUnitalSubalgebra.mem_map
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
f : F
⊢ Eq (α := NonUnitalSubalgebra R B) (toNonUnitalSubalgebra (map f S))
    (NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra)

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
f : F
⊢ (↑(map f S) : Set B) = (⇑f : (a : A) → B) '' (↑S : Set A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
f : F
U : NonUnitalStarSubalgebra R B
⊢ map f S ≤ U ↔ S ≤ comap f U

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
f : F
⊢ GaloisConnection (α := NonUnitalStarSubalgebra R A) (β := NonUnitalStarSubalgebra R B) (map f) (comap f)

Tactic:
fun _S _U => map_le

Premises used: NonUnitalStarSubalgebra.map_le, GaloisConnection
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R B
f : F
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (comap f S) x ↔ Membership.mem (α := B) S ((f : (a : A) → B) x : B)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R B
f : F
⊢ (↑(comap f S) : Set A) = (⇑f : (a : A) → B) ⁻¹' (↑S : Set B)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- 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
S_1 : NonUnitalStarSubalgebra R_1 A_1
R : Type u_1
A : Type u_2
inst_13 : CommSemiring R
inst_14 : NonUnitalSemiring A
inst_15 : NoZeroDivisors A
inst_16 : Module R A
inst_17 : Star A
S : NonUnitalStarSubalgebra R A
⊢ NoZeroDivisors.{u_2} ↥S

Tactic:
NonUnitalSubsemiringClass.noZeroDivisors S

Premises used: NonUnitalSubsemiringClass.noZeroDivisors
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
s : NonUnitalSubalgebra R A
h_star : ∀ x ∈ s, star x ∈ s
x : A
⊢ x ∈ s.toNonUnitalStarSubalgebra h_star ↔ 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 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
s : NonUnitalSubalgebra R A
h_star : ∀ x ∈ s, star x ∈ s
⊢ (↑(s.toNonUnitalStarSubalgebra h_star) : 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 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
s : NonUnitalSubalgebra R A
h_star : ∀ x ∈ s, star x ∈ s
⊢ (s.toNonUnitalStarSubalgebra h_star).toNonUnitalSubalgebra = s

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
S : NonUnitalStarSubalgebra R A
⊢ S.toNonUnitalStarSubalgebra ⋯ = S

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, 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
φ : F
a : A
⊢ Membership.mem.{w, w} (α := B) (γ := Set B)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring
            (NonUnitalAlgHom.range (F := A →ₙₐ[R] B) (NonUnitalAlgHomClass.toNonUnitalAlgHom φ))))))
    (star (((↑(NonUnitalAlgHomClass.toNonUnitalAlgHom φ) : A →ₙ+* B) : (a : A) → B) a) : B)

Tactic:
⟨star a, map_star φ a⟩

Premises used: Set.Mem, setOf, StarHomClass.map_star, Exists.intro, Set.range, 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
φ : F
a : A
⊢ Membership.mem.{w, w} (α := B) (γ := Set B)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring
            (NonUnitalAlgHom.range (F := A →ₙₐ[R] B) (NonUnitalAlgHomClass.toNonUnitalAlgHom φ))))))
    (star (((↑(NonUnitalAlgHomClass.toNonUnitalAlgHom φ) : A →ₙ+* B) : (a : A) → B) a) : B)

Tactic:
exact ⟨star a, map_star φ a⟩
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
φ : F
y : B
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R B) (NonUnitalStarAlgHom.range φ) y ↔ ∃ (x : A), (φ : (a : A) → B) x = y

Tactic:
NonUnitalRingHom.mem_srange

Premises used: NonUnitalRingHom.mem_srange, Set.Mem
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
φ : F
x : A
⊢ Membership.mem (α := B) (γ := NonUnitalStarSubalgebra R B) (NonUnitalStarAlgHom.range φ) ((φ : (a : A) → B) x : B)

Tactic:
(NonUnitalAlgHom.mem_range φ).2 ⟨x, rfl⟩

Premises used: Iff.mpr, Set.Mem, NonUnitalAlgHom.mem_range, Exists.intro, rfl, NonUnitalAlgHomClass.toNonUnitalAlgHom
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
φ : F
⊢ (↑(NonUnitalStarAlgHom.range φ) : Set B) = Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
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
f : A →⋆ₙₐ[R] B
g : B →⋆ₙₐ[R] C
⊢ Eq (α := NonUnitalStarSubalgebra R C) (NonUnitalStarAlgHom.range (g.comp f))
    (NonUnitalStarSubalgebra.map g (NonUnitalStarAlgHom.range f))

Tactic:
SetLike.coe_injective (Set.range_comp g f)

Premises used: Set.range_comp, SetLike.coe_injective, DFunLike.coe
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
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
f : A →⋆ₙₐ[R] B
g : B →⋆ₙₐ[R] C
⊢ LE.le (α := NonUnitalStarSubalgebra R C) (NonUnitalStarAlgHom.range (g.comp f)) (NonUnitalStarAlgHom.range g)

Tactic:
SetLike.coe_mono (Set.range_comp_subset_range f g)

Premises used: Set.range_comp_subset_range, Set.Subset, DFunLike.coe, SetLike.coe_mono
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
f : F
S : NonUnitalStarSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
⊢ Eq (α := A →⋆ₙₐ[R] B) (comp (NonUnitalStarSubalgebraClass.subtype S) (codRestrict f S hf)) (↑f : A →⋆ₙₐ[R] B)

Tactic:
NonUnitalStarAlgHom.ext fun _ => rfl

Premises used: rfl, NonUnitalStarAlgHom.ext
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
f : F
S : NonUnitalStarSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
x : A
⊢ Eq.{w + 1} (α := B) ((↑(((codRestrict f S hf : NonUnitalStarAlgHom.{u, v, w} R A ↥S) : (a : A) → ↥S) x) : B) : B)
    ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
f : F
S : NonUnitalStarSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
⊢ Function.Injective.{v + 1, w + 1} (α := A) (β := ↥S) (⇑(codRestrict f S hf) : (a : A) → ↥S) ↔
    Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
⟨fun H _x _y hxy => H <| Subtype.ext hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩

Premises used: congr_arg, Iff.intro, Subtype.val, Subtype.ext
-- 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
ϕ ψ : F
x : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
⊢ star x ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubalgebra.toNonUnitalSubsemiring (NonUnitalAlgHom.equalizer ϕ ψ))))

Tactic:
simp [map_star, hx]

Premises used: StarHomClass.map_star
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : 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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
φ ψ : F
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (equalizer φ ψ) x ↔
    Eq.{w + 1} (α := B) ((φ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : NonUnitalSemiring 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
g : B → A
f : F
h : Function.LeftInverse g (⇑f : (a : A) → B)
x : ↥(NonUnitalStarAlgHom.range f)
x' : A
hx' : (f : (a : A) → B) x' = (↑x : B)
rw : Eq.{w + 1} (α := B) ((f : (a : A) → B) (g ((f : (a : A) → B) x')) : B) ((f : (a : A) → B) x' : B)
rw₁ rw₂ : Eq.{w + 1} (α := B) ((f : (a : A) → B) x' : B) ((f : (a : A) → B) x' : B)
⊢ (f : (a : A) → B) (g (↑x : B)) = (↑x : B)

Tactic:
rw [← hx', h x']
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
g : B → A
f : F
h : Function.LeftInverse g (⇑f : (a : A) → B)
x : A
⊢ Eq.{w + 1} (α := B)
    ((↑(((ofLeftInverse' h : StarAlgEquiv.{u, v, w} R A ↥(NonUnitalStarAlgHom.range f)) :
              (a : A) → ↥(NonUnitalStarAlgHom.range f))
            x) :
        B) :
      B)
    ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
g : B → A
f : F
h : Function.LeftInverse g (⇑f : (a : A) → B)
x : ↥(NonUnitalStarAlgHom.range f)
⊢ (symm (ofLeftInverse' h) : (a : ↥(NonUnitalStarAlgHom.range f)) → A) x = g (↑x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : Star A
inst_4 : NonUnitalSemiring B
inst_5 : Module R B
inst_6 : Star B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
f : F
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
x : A
⊢ Eq.{w + 1} (α := B)
    ((↑(((ofInjective' f hf : StarAlgEquiv.{u, v, w} R A ↥(NonUnitalStarAlgHom.range f)) :
              (a : A) → ↥(NonUnitalStarAlgHom.range f))
            x) :
        B) :
      B)
    ((f : (a : A) → B) x : B)

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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
S : NonUnitalSubalgebra R A
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x + y ∈ star S.carrier

Tactic:
simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier]
        using (star_add x y).symm ▸ add_mem hx hy

Premises used: NonUnitalSubalgebra.mem_carrier, Set.mem_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 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
S : NonUnitalSubalgebra R A
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x * y ∈ star S.carrier

Tactic:
simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier]
        using (star_mul x y).symm ▸ mul_mem hy hx

Premises used: NonUnitalSubalgebra.mem_carrier, Set.mem_star