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

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

Premises used: Set.iUnionLift_unary, NonUnitalStarSubalgebra.coe_iSup_of_directed, 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 : 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 : (↑(↑(K i) : Set A) : Type v)),
    Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) (star x) : B) (star ((f i : (a : ↥(K i)) → B) x) : B)

Tactic:
simp [map_star]

Premises used: StarHomClass.map_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 : 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 : (↑(↑(K i) : Set A) : Type v)),
    Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) (star x) : B) (star ((f i : (a : ↥(K i)) → B) x) : B)

Tactic:
all_goals simp [map_star]

Premises used: StarHomClass.map_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 : 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)
⊢ NonUnitalStarAlgHom.{u, v, w} R (↥(iSup K)) B

Tactic:
exact
    { toFun :=
        Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
          (fun i j x hxi hxj => by
            let ⟨k, hik, hjk⟩ := dir i j
            simp only
            rw [hf i k hik, hf j k hjk]
            rfl)
          _ (by rw [coe_iSup_of_directed dir])
      map_zero' := by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]
        exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
      map_mul' := by
        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]
        apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
        all_goals simp
      map_add' := by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]
        apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
        all_goals simp
      map_smul' := fun r => by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]
        apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x)
          (fun _ _ => rfl)
        all_goals simp
      map_star' := by
        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]
        apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => star x)
          (fun _ _ => rfl)
        all_goals simp [map_star] }
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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
i : ι
x : ↥(K i)
h : K i ≤ T
subst :
  ∀ (h : K i ≤ iSup K),
    Eq.{w + 1} (α := B)
      ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) ((inclusion h : (a : ↥(K i)) → ↥(iSup K)) x : ↥(iSup K)) :
        B)
      ((f i : (a : ↥(K i)) → B) x : B)
⊢ Eq.{w + 1} (α := B) ((iSupLift K dir f hf T hT : (a : ↥T) → B) ((inclusion h : (a : ↥(K i)) → ↥T) x : ↥T) : B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
subst T
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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 : ↥(K i)
h : K i ≤ iSup K
dsimp :
  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) ⋯ ((inclusion h : (a : ↥(K i)) → ↥(iSup K)) x) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)
⊢ Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) ((inclusion h : (a : ↥(K i)) → ↥(iSup K)) x : ↥(iSup K)) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
dsimp [iSupLift]

Premises used: NonUnitalStarSubalgebra.iSupLift
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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 : ↥(K i)
h : K i ≤ iSup K
h₁ : (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)
⊢ 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) ⋯ ((inclusion h : (a : ↥(K i)) → ↥(iSup K)) x) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
apply Set.iUnionLift_inclusion

Premises used: Set.iUnionLift_inclusion
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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 : ↥(K i)
h : K i ≤ iSup K
⊢ (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)

Tactic:
h

Premises used: Set.Subset
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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 : ↥(K i)
h : K i ≤ iSup K
⊢ (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)

Tactic:
exact h
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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
i : ι
h : K i ≤ T
h₁ :
  ∀ (x : ↥(K i)),
    Eq.{w + 1} (α := B) (((iSupLift K dir f hf T hT).comp (inclusion h) : (a : ↥(K i)) → B) x : B)
      ((f i : (a : ↥(K i)) → B) x : B)
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i

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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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
i : ι
h : K i ≤ T
x : ↥(K i)
⊢ Eq.{w + 1} (α := B) (((iSupLift K dir f hf T hT).comp (inclusion h) : (a : ↥(K i)) → B) x : B)
    ((f i : (a : ↥(K i)) → B) x : B)

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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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
i : ι
x : ↥(K i)
hx : (↑x : A) ∈ T
subst :
  ∀ (hx : (↑x : A) ∈ iSup K),
    Eq.{w + 1} (α := B)
      ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
        B)
      ((f i : (a : ↥(K i)) → B) x : B)
⊢ Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf T hT : (a : ↥T) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ T) (↑x : A) hx) : B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
subst hT
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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 : ↥(K i)
hx : (↑x : A) ∈ iSup K
dsimp :
  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) ⋯ (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)
⊢ Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
dsimp [iSupLift]

Premises used: NonUnitalStarSubalgebra.iSupLift
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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 : ↥(K i)
hx : (↑x : 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) ⋯ (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
apply Set.iUnionLift_mk

Premises used: Set.iUnionLift_mk
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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
i : ι
x : ↥T
hx : (↑x : A) ∈ K i
subst :
  ∀ (x : ↥(iSup K)) (hx : (↑x : A) ∈ K i),
    Eq.{w + 1} (α := B) ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) x : B)
      ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
⊢ Eq.{w + 1} (α := B) ((iSupLift K dir f hf T hT : (a : ↥T) → B) x : B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)

Tactic:
subst hT
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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 : ↥(iSup K)
hx : (↑x : A) ∈ K i
dsimp :
  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) ⋯ x :
      B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
⊢ Eq.{w + 1} (α := B) ((iSupLift K dir f hf (iSup K) ⋯ : (a : ↥(iSup K)) → B) x : B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)

Tactic:
dsimp [iSupLift]

Premises used: NonUnitalStarSubalgebra.iSupLift
-- 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
ι : Type u_1
inst_7 : StarRing R
inst_8 : IsScalarTower R A A
inst_9 : SMulCommClass R A A
inst_10 : StarModule R A
inst_11 : 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 : ↥(iSup K)
hx : (↑x : A) ∈ K i
⊢ 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) ⋯ x :
      B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)

Tactic:
apply Set.iUnionLift_of_mem

Premises used: Set.iUnionLift_of_mem
-- 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
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
⊢ (↑(center R A) : Set A) = Set.center A

Tactic:
rfl

Premises used: setOf, Set.center, 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
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
⊢ Eq (α := NonUnitalSubalgebra R A) (toNonUnitalSubalgebra (center R A)) (NonUnitalSubalgebra.center R A)

Tactic:
rfl

Premises used: NonUnitalSubalgebra.center, rfl
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : StarRing R
inst_2 : NonUnitalCommSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
⊢ Eq (α := NonUnitalStarSubalgebra R A) (center R A) ⊤

Tactic:
SetLike.coe_injective (Set.center_eq_univ A)

Premises used: Set.center_eq_univ, SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : StarRing A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
a : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (center R A) a ↔ ∀ (b : A), b * a = a * b

Tactic:
Subsemigroup.mem_center_iff

Premises used: Set.Mem, setOf, Subsemigroup.mem_center_iff, Set.center
-- 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
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
⊢ (↑(centralizer R s) : Set A) = (s ∪ star s).centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, 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
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
z : A
simp : (∀ x ∈ s, x * z = z * x) → ((∀ x ∈ star s, x * z = z * x) ↔ ∀ (x : A) (x_1 : x ∈ s), star x * z = z * star x)
⊢ (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Tactic:
simp only [Set.mem_union, or_imp, forall_and, and_congr_right_iff]

Premises used: Set.mem_union, or_imp, and_congr_right_iff, forall_and
-- 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
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
z : A
⊢ (∀ x ∈ s, x * z = z * x) → ((∀ x ∈ star s, x * z = z * x) ↔ ∀ (x : A) (x_1 : x ∈ s), star x * z = z * star x)

Tactic:
fun _ =>
    ⟨fun hz a ha => hz _ (Set.star_mem_star.mpr ha), fun hz a ha => star_star a ▸ hz _ ha⟩

Premises used: Iff.mpr, star_star, Eq.rec, Iff.intro, Set.star_mem_star, 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
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s : Set A
z : A
⊢ (∀ x ∈ s, x * z = z * x) → ((∀ x ∈ star s, x * z = z * x) ↔ ∀ (x : A) (x_1 : x ∈ s), star x * z = z * star x)

Tactic:
exact fun _ =>
    ⟨fun hz a ha => hz _ (Set.star_mem_star.mpr ha), fun hz a ha => star_star a ▸ hz _ ha⟩
-- 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
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
s t : Set A
h : s ⊆ t
⊢ LE.le (α := NonUnitalStarSubalgebra R A) (centralizer R t) (centralizer R s)

Tactic:
Set.centralizer_subset (Set.union_subset_union h <| Set.preimage_mono h)

Premises used: Set.union_subset_union, Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset, Set.preimage_mono