awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
r : R
dsimp :
  ∀ (x : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (r • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) r : R)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)
⊢ ∀ (x : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
        (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (r • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) r : R)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)

Tactic:
dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]

Premises used: SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, NonUnitalStarSubalgebra.inclusion_mk, Eq.ndrec, Function.comp_apply, eq_mpr_eq_cast, id_eq
-- 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)
r : R
h :
  ∀ (i : ι) (x : (↑(↑(K i) : Set A) : Type v)),
    (f i : (a : ↥(K i)) → B) (r • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) r : R) ((f i : (a : ↥(K i)) → B) x : B)
⊢ ∀ (x : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (r • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) r : R)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)

Tactic:
apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x)
          (fun _ _ => rfl)

Premises used: Set.iUnionLift_unary, NonUnitalStarSubalgebra.coe_iSup_of_directed, HSMul.hSMul
-- 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)
r : R
⊢ ∀ (i : ι) (x : (↑(↑(K i) : Set A) : Type v)),
    (f i : (a : ↥(K i)) → B) (r • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) r : R) ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
simp
-- 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)
r : R
⊢ ∀ (i : ι) (x : (↑(↑(K i) : Set A) : Type v)),
    (f i : (a : ↥(K i)) → B) (r • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) r : R) ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
all_goals simp
-- 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 : ι), Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) ((fun (i : ι) ↦ (0 : ↥(K i))) i) : B) (0 : B)

Tactic:
simp
-- 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)
⊢ Eq.{w + 1} (α := B)
    (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
      (↑(iSup K) : Set A) ⋯ 0)
    0

Tactic:
exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)

Premises used: Set.iUnionLift_const, 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
ι : 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)
dsimp :
  ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (x + y) =
      HAdd.hAdd (α := B)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ y)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
        (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (x + y) =
      HAdd.hAdd (α := B)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ y)

Tactic:
dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]

Premises used: SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, NonUnitalStarSubalgebra.inclusion_mk, Eq.ndrec, Function.comp_apply, eq_mpr_eq_cast, id_eq
-- 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)
hopi :
  ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
    Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ (x + y) =
      HAdd.hAdd (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ x)
        (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ y)
h :
  ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
    (f i : (a : ↥(K i)) → B) (x + y) =
      HAdd.hAdd (α := B) (β := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) y : B)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (x + y) =
      HAdd.hAdd (α := B)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ y)

Tactic:
apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))

Premises used: HAdd.hAdd, NonUnitalStarSubalgebra.coe_iSup_of_directed, Set.iUnionLift_binary
-- 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 : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
    Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ (x + y) =
      HAdd.hAdd (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ x)
        (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ y)

Tactic:
simp
-- 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 : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
    (f i : (a : ↥(K i)) → B) (x + y) =
      HAdd.hAdd (α := B) (β := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) y : B)

Tactic:
simp
-- 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)
dsimp :
  ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (x * y) =
      HMul.hMul (α := B)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ y)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
        (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (x * y) =
      HMul.hMul (α := B)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ y)

Tactic:
dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast, ZeroMemClass.coe_zero,
          AddSubmonoid.mk_add_mk, Set.inclusion_mk]

Premises used: SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, NonUnitalStarSubalgebra.inclusion_mk, AddSubmonoid.mk_add_mk, ZeroMemClass.coe_zero, Eq.ndrec, Function.comp_apply, eq_mpr_eq_cast, Set.inclusion_mk, id_eq
-- 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)
hopi :
  ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
    Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ (x * y) =
      HMul.hMul (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ x)
        (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ y)
h :
  ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
    (f i : (a : ↥(K i)) → B) (x * y) =
      HMul.hMul (α := B) (β := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) y : B)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (x * y) =
      HMul.hMul (α := B)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ y)

Tactic:
apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))

Premises used: HMul.hMul, NonUnitalStarSubalgebra.coe_iSup_of_directed, Set.iUnionLift_binary
-- 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 : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
    Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ (x * y) =
      HMul.hMul (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ x)
        (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ y)

Tactic:
simp
-- 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 : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
    (f i : (a : ↥(K i)) → B) (x * y) =
      HMul.hMul (α := B) (β := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) y : B)

Tactic:
simp
-- 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)
dsimp :
  ∀ (a : ↥(iSup K)),
    Eq.{w + 1} (α := B)
      (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (star a))
      (star
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ a))
⊢ ∀ (a : ↥(iSup K)),
    Eq.{w + 1} (α := B)
      (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
        (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (star a))
      (star
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ a))

Tactic:
dsimp only [SetLike.coe_sort_coe, NonUnitalStarAlgHom.comp_apply, inclusion_mk, Eq.ndrec,
          id_eq, eq_mpr_eq_cast, ZeroMemClass.coe_zero, AddSubmonoid.mk_add_mk, Set.inclusion_mk,
          MulMemClass.mk_mul_mk, NonUnitalAlgHom.toDistribMulActionHom_eq_coe,
          DistribMulActionHom.toFun_eq_coe, NonUnitalAlgHom.coe_to_distribMulActionHom,
          NonUnitalAlgHom.coe_mk]

Premises used: SetLike.coe_sort_coe, NonUnitalAlgHom.toDistribMulActionHom_eq_coe, NonUnitalStarAlgHom.comp_apply, NonUnitalStarSubalgebra.inclusion_mk, AddSubmonoid.mk_add_mk, ZeroMemClass.coe_zero, Eq.ndrec, MulMemClass.mk_mul_mk, DistribMulActionHom.toFun_eq_coe, NonUnitalAlgHom.coe_mk, eq_mpr_eq_cast, Set.inclusion_mk, id_eq, NonUnitalAlgHom.coe_to_distribMulActionHom