awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NonUnitalStarSubalgebra R A
⊢ Eq (α := ↥S →ₙₐ[R] ↥S) (NonUnitalAlgHomClass.toNonUnitalAlgHom (inclusion ⋯)) (NonUnitalAlgHom.id R ↥S)

Tactic:
NonUnitalAlgHom.ext fun _x => Subtype.ext rfl

Premises used: rfl, Subtype.ext, NonUnitalAlgHom.ext
-- 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
x : A
hx : x ∈ S
⊢ (inclusion h : (a : ↥S) → ↥T) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) x hx) = Subtype.mk (p := fun (x : A) ↦ x ∈ T) x ⋯

Tactic:
rfl

Premises used: Set.Mem, rfl
-- 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
x : ↥T
m : (↑x : A) ∈ S
⊢ (inclusion h : (a : ↥S) → ↥T) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑x : A) m) = x

Tactic:
Subtype.ext rfl

Premises used: rfl, Subtype.ext
-- 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 U : NonUnitalStarSubalgebra R A
hst : S ≤ T
htu : T ≤ U
x : ↥S
⊢ Eq (α := ↥U) ((inclusion htu : (a : ↥T) → ↥U) ((inclusion hst : (a : ↥S) → ↥T) x) : ↥U)
    ((inclusion ⋯ : (a : ↥S) → ↥U) x : ↥U)

Tactic:
Subtype.ext rfl

Premises used: rfl, Subtype.ext
-- 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
s : ↥S
⊢ (↑((inclusion h : (a : ↥S) → ↥T) s) : A) = (↑s : A)

Tactic:
rfl

Premises used: Set.Mem, 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
inst_10 : StarRing R
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 : Set A
⊢ Eq (α := NonUnitalStarSubalgebra R B) (map f (adjoin R s)) (adjoin R ((⇑f : (a : A) → B) '' s))

Tactic:
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) NonUnitalStarAlgebra.gi.gc
    NonUnitalStarAlgebra.gi.gc fun _t => rfl

Premises used: GaloisConnection.l_comm_of_u_comm, Set.image_preimage, NonUnitalStarSubalgebra.gc_map_comap, NonUnitalStarAlgebra.gi, rfl, GaloisInsertion.gc
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
inst_10 : StarRing R
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
x : A
⊢ Eq (α := NonUnitalStarSubalgebra R B) (map f (adjoin R {x})) (adjoin R (singleton (α := B) ((f : (a : A) → B) x : B)))

Tactic:
simp [NonUnitalStarAlgHom.map_adjoin]

Premises used: NonUnitalStarAlgHom.map_adjoin
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B_1 : Type w
C_1 : Type w'
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B_1
inst_5 : StarRing B_1
inst_6 : Module R B_1
inst_7 : FunLike F A B_1
inst_8 : NonUnitalAlgHomClass F R A B_1
inst_9 : StarHomClass F A B_1
S : NonUnitalStarSubalgebra R A
inst_10 : StarRing R
inst_11 : IsScalarTower R A A
inst_12 : SMulCommClass R A A
inst_13 : StarModule R A
inst_14 : IsScalarTower R B_1 B_1
inst_15 : SMulCommClass R B_1 B_1
inst_16 : StarModule R B_1
inst_17 : Subsingleton A
B C : NonUnitalStarSubalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C

Tactic:
simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]

Premises used: ZeroMemClass.zero_mem, Subsingleton.elim, OfNat.ofNat
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
inst_10 : StarRing R
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
inst_17 : Subsingleton.{v + 1} (NonUnitalStarSubalgebra R A)
⊢ Subsingleton (A →⋆ₙₐ[R] B)

Tactic:
⟨fun f g => NonUnitalStarAlgHom.ext fun a =>
    have : a ∈ (⊥ : NonUnitalStarSubalgebra R A) :=
      Subsingleton.elim (⊤ : NonUnitalStarSubalgebra R A) ⊥ ▸ mem_top
    (mem_bot.mp this).symm ▸ (map_zero f).trans (map_zero g).symm⟩

Premises used: NonUnitalStarAlgebra.mem_bot, NonUnitalStarAlgebra.mem_top, Eq.rec, map_zero, Bot.bot, Subsingleton.intro, Iff.mp, Subsingleton.elim, Top.top, Eq.symm, Eq.trans, NonUnitalStarAlgHom.ext
-- 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 : NonUnitalStarSubalgebra R A
⊢ NonUnitalStarAlgHom.range (F := ↥S →⋆ₙₐ[R] A) (NonUnitalStarSubalgebraClass.subtype S) = S

Tactic:
ext <| Set.ext_iff.1 <|
    (NonUnitalStarAlgHom.coe_range (NonUnitalStarSubalgebraClass.subtype S)).trans Subtype.range_val

Premises used: NonUnitalStarSubalgebraClass.subtype, NonUnitalStarSubalgebra.ext, Subtype.range_val, Iff.mp, Set.ext_iff, Eq.trans, NonUnitalStarAlgHom.coe_range
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
S : NonUnitalStarSubalgebra R A
S₁ : NonUnitalStarSubalgebra R B
⊢ (↑(S.prod S₁) : Set (A × B)) = (↑S : Set A) ×ˢ (↑S₁ : Set B)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
S : NonUnitalStarSubalgebra R A
S₁ : NonUnitalStarSubalgebra R B
⊢ (S.prod S₁).toNonUnitalSubalgebra = S.prod S₁.toNonUnitalSubalgebra

Tactic:
rfl

Premises used: NonUnitalSubalgebra.prod, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
S : NonUnitalStarSubalgebra R A
S₁ : NonUnitalStarSubalgebra R B
x : A × B
⊢ x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁

Tactic:
Set.mem_prod

Premises used: Set.Mem, setOf, Set.prod, Set.mem_prod
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
S T : NonUnitalStarSubalgebra R A
S₁ T₁ : NonUnitalStarSubalgebra R B
⊢ S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁

Tactic:
Set.prod_mono

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : IsScalarTower R B B
inst_12 : SMulCommClass R B B
inst_13 : StarModule R B
h :
  ∀ (x : A × B),
    Membership.mem (γ := NonUnitalStarSubalgebra R (A × B)) (prod ⊤ ⊤) x ↔
      Membership.mem (γ := NonUnitalStarSubalgebra R (A × B)) ⊤ x
⊢ Eq (α := NonUnitalStarSubalgebra R (A × B)) (prod ⊤ ⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : IsScalarTower R B B
inst_12 : SMulCommClass R B B
inst_13 : StarModule R B
x : A × B
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R (A × B)) (prod ⊤ ⊤) x ↔
    Membership.mem (γ := NonUnitalStarSubalgebra R (A × B)) ⊤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : IsScalarTower R B B
inst_12 : SMulCommClass R B B
inst_13 : StarModule R B
S T : NonUnitalStarSubalgebra R A
S₁ T₁ : NonUnitalStarSubalgebra R B
⊢ S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)

Tactic:
SetLike.coe_injective Set.prod_inter_prod

Premises used: SetLike.coe_injective, Set.prod_inter_prod
-- 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
ι : Type u_1
inst_4 : StarRing R
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : Nonempty ι
S : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) S
⊢ (↑(iSup S) : Set A) = ⋃ (i : ι), (↑(S i) : Set A)

Tactic:
let K : NonUnitalStarSubalgebra R A :=
    { __ := NonUnitalSubalgebra.copy _ _ (NonUnitalSubalgebra.coe_iSup_of_directed dir).symm
      star_mem' := fun hx ↦
        let ⟨i, hi⟩ := Set.mem_iUnion.1 hx
        Set.mem_iUnion.2 ⟨i, star_mem (s := S i) hi⟩ }
  have : iSup S = K := le_antisymm (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set A)) i)
    (Set.iUnion_subset fun _ ↦ le_iSup S _)
  this.symm ▸ rfl

Premises used: Iff.mpr, Set.iUnion_subset, iSup, Set.mem_iUnion, AddSubsemigroup.carrier, Membership.mem, Eq.rec, StarMemClass.star_mem, le_iSup, AddSubmonoid.toAddSubsemigroup, NonUnitalSubalgebra.copy, NonUnitalSubalgebra.coe_iSup_of_directed, le_antisymm, NonUnitalSubsemiring.toAddSubmonoid, SetLike.coe, NonUnitalStarSubalgebra.mk, NonUnitalSubalgebra.toNonUnitalSubsemiring, Exists.intro, Iff.mp, iSup_le, NonUnitalStarSubalgebra.toNonUnitalSubalgebra, Eq.symm, Set.iUnion, _private.0.NonUnitalStarSubalgebra.coe_iSup_of_directed.match_1, rfl, Star.star
-- 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
ι : Type u_1
inst_4 : StarRing R
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : Nonempty ι
S : ι → NonUnitalStarSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative.{v} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{v} ↥(⨆ (i : ι), S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, NonUnitalSubsemiring.coe_iSup_of_directed dir,
    coe_iSup_of_directed dir] using NonUnitalSubsemiring.isMulCommutative_iSup dir

Premises used: NonUnitalSubsemiring.isMulCommutative_iSup, NonUnitalSubsemiring.coe_iSup_of_directed, SetLike.mem_coe, NonUnitalStarSubalgebra.coe_iSup_of_directed, isMulCommutative_iff
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S_1 : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
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
inst_17 : Nonempty ι
inst_18 : Preorder ι
inst_19 : IsDirectedOrder ι
S : OrderHom.{u_1, v} ι (NonUnitalStarSubalgebra R A)
hS : ∀ (i : ι), IsMulCommutative.{v} ↥((S : (a : ι) → NonUnitalStarSubalgebra R A) i : NonUnitalStarSubalgebra R A)
⊢ IsMulCommutative.{v} ↥(⨆ (i : ι), (S : (a : ι) → NonUnitalStarSubalgebra R A) i)

Tactic:
isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, NonUnitalStarSubalgebra.isMulCommutative_iSup, Monotone.directed_le
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
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
inst_17 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
subst : NonUnitalStarAlgHom.{u, v, w} R (↥(iSup K)) B
⊢ NonUnitalStarAlgHom.{u, v, w} R (↥T) B

Tactic:
subst hT
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
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
inst_17 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
let :
  ∀ (k : ι) (hik : K i ≤ K k) (hjk : K j ≤ K k),
    Eq.{w + 1} (α := B)
      ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
      ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))
⊢ Eq.{w + 1} (α := B)
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))

Tactic:
let ⟨k, hik, hjk⟩ := dir i j
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
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
inst_17 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
k : ι
hik : (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) (K j) (K k)
simp :
  Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)
⊢ Eq.{w + 1} (α := B)
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))

Tactic:
simp only
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
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
inst_17 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
k : ι
hik : (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) (K j) (K k)
rw :
  Eq.{w + 1} (α := B)
    (((f k).comp (inclusion hik) : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    (((f k).comp (inclusion hjk) : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)
⊢ Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)

Tactic:
rw [hf i k hik, hf j k hjk]
-- 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 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
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
inst_17 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
k : ι
hik : (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) (K j) (K k)
⊢ Eq.{w + 1} (α := B)
    (((f k).comp (inclusion hik) : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    (((f k).comp (inclusion hjk) : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)

Tactic:
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 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : NonUnitalSemiring B
inst_5 : StarRing B
inst_6 : Module R B
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst_10 : StarRing R
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
inst_17 : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalStarSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalStarAlgHom.{u, v, w} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
rw rw₁ : Subset.{v} (α := Set A) (⋃ (i : ι), (↑(K i) : Set A)) (⋃ (i : ι), (↑(K i) : Set A))
⊢ (↑(iSup K) : Set A) ⊆ ⋃ (i : ι), (↑(K i) : Set A)

Tactic:
rw [coe_iSup_of_directed dir]

Premises used: NonUnitalStarSubalgebra.coe_iSup_of_directed