awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s t : Set A
H : s ⊆ t
⊢ LE.le (α := StarSubalgebra R A) (adjoin R s) (adjoin R t)

Tactic:
StarAlgebra.gc.monotone_l H

Premises used: StarAlgebra.gc, GaloisConnection.monotone_l
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : StarSubalgebra 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, StarAlgebra.subset_adjoin, le_antisymm, SetLike.coe, StarAlgebra.adjoin_le
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
rw :
  Eq (α := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (s ∪ star s)) : Submodule R A)
    (span R (↑(Submonoid.closure (s ∪ star s)) : Set A) : Submodule R A)
rw₁ rw₂ :
  Eq (α := Submodule R A) (span R (↑(Submonoid.closure (s ∪ star s)) : Set A))
    (span R (↑(Submonoid.closure (s ∪ star s)) : Set A))
⊢ Eq (α := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (StarSubalgebra.toSubalgebra (adjoin R s)) :
      Submodule R A)
    (span R (↑(Submonoid.closure (s ∪ star s)) : Set A) : Submodule R A)

Tactic:
rw [adjoin_toSubalgebra, Algebra.adjoin_eq_span]

Premises used: Algebra.adjoin_eq_span, StarAlgebra.adjoin_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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : NonUnitalStarSubalgebra R A
rw : span R (↑(Submonoid.closure ((↑s : Set A) ∪ star (↑s : Set A))) : Set A) = R ∙ 1 ⊔ s.toSubmodule
rw₁ : span R ({1} ∪ (↑(Subsemigroup.closure ((↑s : Set A) ∪ star (↑s : Set A))) : Set A)) = R ∙ 1 ⊔ s.toSubmodule
rw₂ : R ∙ 1 ⊔ span R (↑(Subsemigroup.closure ((↑s : Set A) ∪ star (↑s : Set A))) : Set A) = R ∙ 1 ⊔ s.toSubmodule
rw₃ :
  R ∙ 1 ⊔
      NonUnitalSubalgebra.toSubmodule
        (NonUnitalStarSubalgebra.toNonUnitalSubalgebra (NonUnitalStarAlgebra.adjoin R (↑s : Set A))) =
    R ∙ 1 ⊔ s.toSubmodule
rw₄ rw₅ : R ∙ 1 ⊔ s.toSubmodule = R ∙ 1 ⊔ s.toSubmodule
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A)
      (StarSubalgebra.toSubalgebra (adjoin R (↑s : Set A))) =
    R ∙ 1 ⊔ s.toSubmodule

Tactic:
rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union,
    ← NonUnitalStarAlgebra.adjoin_eq_span, NonUnitalStarAlgebra.adjoin_eq]

Premises used: Submonoid.closure_eq_one_union, NonUnitalStarAlgebra.adjoin_eq_span, Submodule.span_union, NonUnitalStarAlgebra.adjoin_eq, StarAlgebra.adjoin_eq_span
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : Subalgebra R A
⊢ Eq (α := StarSubalgebra R A) S.starClosure (adjoin R (↑S : Set A))

Tactic:
le_antisymm (Subalgebra.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, Subalgebra.starClosure_le_iff, StarAlgebra.subset_adjoin, le_antisymm, SetLike.coe, StarAlgebra.adjoin_le
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
⊢ p a ha

Tactic:
Algebra.adjoin_induction (fun x hx ↦ ?_) algebraMap add mul ha

Premises used: Algebra.adjoin_induction
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
refine : ∀ (x : A) (hx : x ∈ s ∪ Star.star s), p x ⋯
⊢ p a ha

Tactic:
refine Algebra.adjoin_induction (fun x hx ↦ ?_) algebraMap add mul 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
x : A
hx : x ∈ s ∪ Star.star s
⊢ x ∈ s ∨ Star.star x ∈ s

Tactic:
push _ ∈ _ at hx
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : x ∈ s ∨ Star.star x ∈ s
inl : ∀ (hx : x ∈ s), p x ⋯
inr : ∀ (hx : Star.star x ∈ s), p x ⋯
⊢ p x ⋯

Tactic:
obtain (hx | hx) := hx
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : x ∈ s
⊢ p x ⋯

Tactic:
mem x hx
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : x ∈ s
⊢ p x ⋯

Tactic:
exact mem x hx
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ Star.star x ∈ s ∪ Star.star s

Tactic:
simpa using Or.inl hx

Premises used: Or.inl
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p : (x : A) → Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x), p x hx → p (Star.star x) ⋯
a : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
x : A
hx_1 : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ p x ⋯

Tactic:
simpa using star _ (Algebra.subset_adjoin (by simpa using Or.inl hx)) (mem _ hx)

Premises used: Algebra.subset_adjoin
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
x : A
h : x ∈ s
⊢ p x z ⋯ ⋯

Tactic:
mem_mem _ _ h hz
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
x : A
h : x ∈ s
⊢ p x z ⋯ ⋯

Tactic:
exact mem_mem _ _ h hz
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
r : R
⊢ p ((algebraMap R A : (a : R) → A) r) z ⋯ ⋯

Tactic:
algebraMap_left _ _ hz
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
r : R
⊢ p ((algebraMap R A : (a : R) → A) r) z ⋯ ⋯

Tactic:
exact algebraMap_left _ _ hz
-- 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 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
x y : A
hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y
h₁ : p x z hx ⋯
h₂ : p y z hy ⋯
⊢ p (x * y) z ⋯ ⋯

Tactic:
mul_left _ _ _ _ _ _ h₁ h₂