awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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
⊢ ∀ (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)
have dsimp : ∀ (x : ↥(iSup K)),
  Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
      (↑(iSup K) : Set A) sorry (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) sorry
        (↑(iSup K) : Set A) sorry x)
Tactic: dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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
⊢ ∀ (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)
have 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)
Tactic: apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x)
          (fun _ _ => rfl)
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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)
⊢ ∀ (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)
have 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) sorry
      (↑(iSup K) : Set A) sorry (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) sorry
        (↑(iSup K) : Set A) sorry x)
      (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
        (↑(iSup K) : Set A) sorry y)
Tactic: dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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)
⊢ ∀ (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)
have hopi : ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
  Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry (x + y) =
    HAdd.hAdd (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry x)
      (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry y)
Tactic: apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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)
⊢ ∀ (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)
have 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: apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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)
⊢ ∀ (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)
have 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) sorry
      (↑(iSup K) : Set A) sorry (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) sorry
        (↑(iSup K) : Set A) sorry x)
      (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
        (↑(iSup K) : Set A) sorry 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]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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)
⊢ ∀ (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)
have hopi : ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type v)),
  Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry (x * y) =
    HMul.hMul (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry x)
      (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry y)
Tactic: apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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)
⊢ ∀ (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)
have 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: apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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)
⊢ ∀ (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))
have 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) sorry
      (↑(iSup K) : Set A) sorry (star a))
    (star
      (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
        (↑(iSup K) : Set A) sorry 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]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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)
⊢ ∀ (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))
have 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: apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => star x)
          (fun _ _ => rfl)
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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
⊢ 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)
have subst : ∀ (h : K i ≤ iSup K),
  Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf (iSup K) sorry : (a : ↥(iSup K)) → B) ((inclusion h : (a : ↥(K i)) → ↥(iSup K)) x : ↥(iSup K)) :
      B)
    ((f i : (a : ↥(K i)) → B) x : B)
Tactic: subst T
Cleared hypotheses: T, hT, h
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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
⊢ 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)
have 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) sorry
      (↑(iSup K) : Set A) sorry ((inclusion h : (a : ↥(K i)) → ↥(iSup K)) x) :
    B)
  ((f i : (a : ↥(K i)) → B) x : B)
Tactic: dsimp [iSupLift]
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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
⊢ 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)
have h₁ : (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)
Tactic: apply Set.iUnionLift_inclusion
-- Lean 4 proof step from Mathlib.Algebra.Star.NonUnitalSubalgebra (goal)
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
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i
have 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)
Tactic: ext