awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) (K j) (K k)
⊢ 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)
have 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)
Tactic: rw [hf i k hik, hf j k hjk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ (↑(iSup K) : Set A) ⊆ ⋃ (i : ι), (↑(K i) : Set A)
have rw : Subset.{v} (α := Set A) (⋃ (i : ι), (↑(K i) : Set A)) (⋃ (i : ι), (↑(K i) : Set A))
Tactic: rw [coe_iSup_of_directed dir]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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 (β := B) 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
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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 (β := B) 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 (β := B) 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.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra 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.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra 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
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : (↑x : A) ∈ T
⊢ 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)
have subst : ∀ (hx : (↑x : A) ∈ iSup K),
  Eq.{w + 1} (α := B)
    ((iSupLift K dir f hf (iSup K) sorry : (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: subst hT
Cleared hypotheses: T, hT, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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)
    ((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)
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 (Subtype.mk (p := fun (x : A) ↦ x ∈ iSup K) (↑x : A) hx) :
    B)
  ((f i : (a : ↥(K i)) → B) x : B)
Tactic: dsimp [iSupLift]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : (↑x : A) ∈ K i
⊢ 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)
have subst : ∀ (x : ↥(iSup K)) (hx : (↑x : A) ∈ K i),
  Eq.{w + 1} (α := B) ((iSupLift K dir f hf (iSup K) sorry : (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: subst hT
Cleared hypotheses: T, hT, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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) ((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)
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 x :
    B)
  ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
Tactic: dsimp [iSupLift]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
⊢ Commute (r • a) b
have rw : r • a * b = b * r • a
Tactic: rw [commute_iff_eq, mul_smul_comm, smul_mul_assoc, ha.comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
rw : r • a * b = b * r • a
⊢ Commute (r • a) b
have rw₁ : r • a * b = r • (b * a)
Tactic: rw [commute_iff_eq, mul_smul_comm, smul_mul_assoc, ha.comm]