awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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
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)
⊢ ∀ (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)

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

Premises used: Set.iUnionLift_unary, NonUnitalSubalgebra.coe_iSup_of_directed, HSMul.hSMul
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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
⊢ ∀ (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:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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
⊢ ∀ (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:
all_goals simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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 : ι), Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) ((fun (i : ι) ↦ (0 : ↥(K i))) i) : B) (0 : B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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)
⊢ 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.Algebra.NonUnitalSubalgebra
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)
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
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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)
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: NonUnitalSubalgebra.coe_iSup_of_directed, HAdd.hAdd, Set.iUnionLift_binary
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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 : ι) (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.Algebra.NonUnitalSubalgebra
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 : ι) (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.Algebra.NonUnitalSubalgebra
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)
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
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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)
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, NonUnitalSubalgebra.coe_iSup_of_directed, Set.iUnionLift_binary
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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 : ι) (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.Algebra.NonUnitalSubalgebra
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 : ι) (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.Algebra.NonUnitalSubalgebra
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)
⊢ NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id 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
          exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
        map_mul' := by
          dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
          all_goals simp
        map_add' := by
          dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
          all_goals simp
        map_smul' := fun r => by
          dsimp
          apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x)
            (fun _ _ => rfl)
          all_goals simp }
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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
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.Algebra.NonUnitalSubalgebra
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
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: NonUnitalSubalgebra.iSupLift
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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
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.Algebra.NonUnitalSubalgebra
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
⊢ (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)

Tactic:
h

Premises used: Set.Subset
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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
⊢ (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)

Tactic:
exact h
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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
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.Algebra.NonUnitalSubalgebra
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
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 only [NonUnitalAlgHom.comp_apply, iSupLift_inclusion]

Premises used: NonUnitalSubalgebra.iSupLift_inclusion, NonUnitalAlgHom.comp_apply
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
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
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