[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
p q : NonUnitalSubalgebra R A
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
q : NonUnitalSubalgebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ } =
    (fun s => s.carrier) q
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring A
smul_mem'✝¹ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝¹.carrier → c • x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, smul_mem' := smul_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toNonUnitalSubsemiring
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring A
smul_mem'✝¹ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝¹.carrier → c • x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s => s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝
[PROOFSTEP]
exact SetLike.coe_injective h
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubsemiring = T.toNonUnitalSubsemiring
x : A
⊢ x ∈ S ↔ x ∈ T
[PROOFSTEP]
rw [← mem_toNonUnitalSubsemiring, ← mem_toNonUnitalSubsemiring, h]
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S T : NonUnitalSubalgebra R A
h : toSubmodule S = toSubmodule T
x : A
⊢ x ∈ S ↔ x ∈ T
[PROOFSTEP]
rw [← mem_toSubmodule, ← mem_toSubmodule, h]
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
s : Set A
hs : s = ↑S
src✝ : NonUnitalSubsemiring A := NonUnitalSubsemiring.copy S.toNonUnitalSubsemiring s hs
r : R
a : A
ha : a ∈ s
⊢ r • a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            mul_mem' :=
              (_ :
                ∀ {a b : A},
                  a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
show r • a ∈ s
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
s : Set A
hs : s = ↑S
src✝ : NonUnitalSubsemiring A := NonUnitalSubsemiring.copy S.toNonUnitalSubsemiring s hs
r : R
a : A
ha : a ∈ s
⊢ r • a ∈ s
[PROOFSTEP]
rw [hs] at ha ⊢
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
s : Set A
hs : s = ↑S
src✝ : NonUnitalSubsemiring A := NonUnitalSubsemiring.copy S.toNonUnitalSubsemiring s hs
r : R
a : A
ha : a ∈ ↑S
⊢ r • a ∈ ↑S
[PROOFSTEP]
exact S.smul_mem' r ha
[GOAL]
F : Type v'
R' : Type u'
R✝ : Type u
A✝ : Type v
B : Type w
C : Type w'
inst✝¹⁰ : CommSemiring R✝
inst✝⁹ : NonUnitalNonAssocSemiring A✝
inst✝⁸ : Module R✝ A✝
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R✝ B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R✝ C
inst✝³ : NonUnitalAlgHomClass F R✝ A✝ B
S✝ : NonUnitalSubalgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : NonUnitalRing A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : toNonUnitalSubring S = toNonUnitalSubring T
x : A
⊢ x ∈ S ↔ x ∈ T
[PROOFSTEP]
rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S✝ S T : NonUnitalSubalgebra R A
h : (fun S => toSubmodule S) S = (fun S => toSubmodule S) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T
[PROOFSTEP]
apply SetLike.ext_iff.1 h
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S✝ S T : NonUnitalSubalgebra R A
h : (fun S => S.toNonUnitalSubsemiring) S = (fun S => S.toNonUnitalSubsemiring) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T
[PROOFSTEP]
apply SetLike.ext_iff.1 h
[GOAL]
F : Type v'
R' : Type u'
R✝ : Type u
A✝ : Type v
B : Type w
C : Type w'
inst✝¹⁰ : CommSemiring R✝
inst✝⁹ : NonUnitalNonAssocSemiring A✝
inst✝⁸ : Module R✝ A✝
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R✝ B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R✝ C
inst✝³ : NonUnitalAlgHomClass F R✝ A✝ B
S✝ : NonUnitalSubalgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : NonUnitalRing A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : (fun S => toNonUnitalSubring S) S = (fun S => toNonUnitalSubring S) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T
[PROOFSTEP]
apply SetLike.ext_iff.1 h
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S✝ : NonUnitalSubalgebra R A
f : F
S : NonUnitalSubalgebra R A
src✝ : NonUnitalSubsemiring B := NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring
r : R
b : B
hb :
  b ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            mul_mem' :=
              (_ :
                ∀ {a b : B},
                  a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ r • b ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            mul_mem' :=
              (_ :
                ∀ {a b : B},
                  a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rcases hb with ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
S✝ : NonUnitalSubalgebra R A
f : F
S : NonUnitalSubalgebra R A
src✝ : NonUnitalSubsemiring B := NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring
r : R
a : A
ha : a ∈ ↑S.toNonUnitalSubsemiring
⊢ r • ↑↑f a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            mul_mem' :=
              (_ :
                ∀ {a b : B},
                  a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
exact map_smul f r a ▸ Set.mem_image_of_mem f (S.smul_mem' r ha)
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : B
⊢ a ∈ (NonUnitalRingHom.srange ↑φ).toAddSubmonoid.toAddSubsemigroup.carrier →
    r • a ∈ (NonUnitalRingHom.srange ↑φ).toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : A
⊢ r • ↑↑φ a ∈ (NonUnitalRingHom.srange ↑φ).toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
exact ⟨r • a, map_smul φ r a⟩
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
⊢ ↑(NonUnitalAlgHom.range φ) = Set.range ↑φ
[PROOFSTEP]
ext
[GOAL]
case h
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ x✝ ∈ ↑(NonUnitalAlgHom.range φ) ↔ x✝ ∈ Set.range ↑φ
[PROOFSTEP]
rw [SetLike.mem_coe, mem_range]
[GOAL]
case h
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ (∃ x, ↑φ x = x✝) ↔ x✝ ∈ Set.range ↑φ
[PROOFSTEP]
rfl
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ↑ϕ x = ↑ψ x
hy : ↑ϕ y = ↑ψ y
⊢ x + y ∈ {a | ↑ϕ a = ↑ψ a}
[PROOFSTEP]
rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
⊢ 0 ∈
    { carrier := {a | ↑ϕ a = ↑ψ a},
        add_mem' := (_ : ∀ {x y : A}, ↑ϕ x = ↑ψ x → ↑ϕ y = ↑ψ y → x + y ∈ {a | ↑ϕ a = ↑ψ a}) }.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, map_zero, map_zero]
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ↑ϕ x = ↑ψ x
hy : ↑ϕ y = ↑ψ y
⊢ x * y ∈
    {
          toAddSubsemigroup :=
            { carrier := {a | ↑ϕ a = ↑ψ a},
              add_mem' := (_ : ∀ {x y : A}, ↑ϕ x = ↑ψ x → ↑ϕ y = ↑ψ y → x + y ∈ {a | ↑ϕ a = ↑ψ a}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {a | ↑ϕ a = ↑ψ a},
                    add_mem' :=
                      (_ :
                        ∀ {x y : A},
                          ↑ϕ x = ↑ψ x → ↑ϕ y = ↑ψ y → x + y ∈ {a | ↑ϕ a = ↑ψ a}) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]
[GOAL]
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : Module R C
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : ↑ϕ x = ↑ψ x
⊢ r • x ∈
    {
            toAddSubmonoid :=
              {
                toAddSubsemigroup :=
                  { carrier := {a | ↑ϕ a = ↑ψ a},
                    add_mem' := (_ : ∀ {x y : A}, ↑ϕ x = ↑ψ x → ↑ϕ y = ↑ψ y → x + y ∈ {a | ↑ϕ a = ↑ψ a}) },
                zero_mem' :=
                  (_ :
                    0 ∈
                      { carrier := {a | ↑ϕ a = ↑ψ a},
                          add_mem' :=
                            (_ : ∀ {x y : A}, ↑ϕ x = ↑ψ x → ↑ϕ y = ↑ψ y → x + y ∈ {a | ↑ϕ a = ↑ψ a}) }.carrier) },
            mul_mem' :=
              (_ :
                ∀ {x y : A},
                  ↑ϕ x = ↑ψ x →
                    ↑ϕ y = ↑ψ y →
                      x * y ∈
                        {
                              toAddSubsemigroup :=
                                { carrier := {a | ↑ϕ a = ↑ψ a},
                                  add_mem' :=
                                    (_ : ∀ {x y : A}, ↑ϕ x = ↑ψ x → ↑ϕ y = ↑ψ y → x + y ∈ {a | ↑ϕ a = ↑ψ a}) },
                              zero_mem' :=
                                (_ :
                                  0 ∈
                                    { carrier := {a | ↑ϕ a = ↑ψ a},
                                        add_mem' :=
                                          (_ :
                                            ∀ {x y : A},
                                              ↑ϕ x = ↑ψ x →
                                                ↑ϕ y = ↑ψ y →
                                                  x + y ∈
                                                    {a |
                                                      ↑ϕ a =
                                                        ↑ψ
                                                          a}) }.carrier) }.toAddSubsemigroup.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, map_smul, map_smul, hx]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ a * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
refine' Submodule.span_induction ha _ _ _ _
[GOAL]
case refine'_1
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x : A), x ∈ ↑(NonUnitalSubsemiring.closure s) → x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
refine' Submodule.span_induction hb _ _ _ _
[GOAL]
case refine'_1.refine'_1
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x : A),
    x ∈ ↑(NonUnitalSubsemiring.closure s) →
      ∀ (x_1 : A),
        x_1 ∈ ↑(NonUnitalSubsemiring.closure s) → x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
exact fun x (hx : x ∈ NonUnitalSubsemiring.closure s) y (hy : y ∈ NonUnitalSubsemiring.closure s) =>
  Submodule.subset_span (mul_mem hy hx)
[GOAL]
case refine'_1.refine'_2
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x : A), x ∈ ↑(NonUnitalSubsemiring.closure s) → x * 0 ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
exact fun x _hx => (mul_zero x).symm ▸ Submodule.zero_mem _
[GOAL]
case refine'_1.refine'_3
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x y : A),
    (∀ (x_1 : A),
        x_1 ∈ ↑(NonUnitalSubsemiring.closure s) → x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
      (∀ (x : A), x ∈ ↑(NonUnitalSubsemiring.closure s) → x * y ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
        ∀ (x_1 : A),
          x_1 ∈ ↑(NonUnitalSubsemiring.closure s) → x_1 * (x + y) ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
exact fun x y hx hy z hz => (mul_add z x y).symm ▸ add_mem (hx z hz) (hy z hz)
[GOAL]
case refine'_1.refine'_4
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (a : R) (x : A),
    (∀ (x_1 : A),
        x_1 ∈ ↑(NonUnitalSubsemiring.closure s) → x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
      ∀ (x_1 : A),
        x_1 ∈ ↑(NonUnitalSubsemiring.closure s) → x_1 * a • x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
exact fun r x hx y hy => (mul_smul_comm r y x).symm ▸ SMulMemClass.smul_mem r (hx y hy)
[GOAL]
case refine'_2
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ 0 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
exact (zero_mul b).symm ▸ Submodule.zero_mem _
[GOAL]
case refine'_3
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x y : A),
    x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
      y * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        (x + y) * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
exact fun x y => (add_mul x y b).symm ▸ add_mem
[GOAL]
case refine'_4
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
src✝ : Submodule R A := Submodule.span R ↑(NonUnitalSubsemiring.closure s)
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (a : R) (x : A),
    x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
      a • x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
[PROOFSTEP]
exact fun r x hx => (smul_mul_assoc r x b).symm ▸ SMulMemClass.smul_mem r hx
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
p : { x // x ∈ adjoin R s } → Prop
a : { x // x ∈ adjoin R s }
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
H0 : p 0
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
Hsmul : ∀ (r : R) (x : { x // x ∈ adjoin R s }), p x → p (r • x)
b : A
hb : b ∈ adjoin R s
⊢ p { val := b, property := hb }
[PROOFSTEP]
refine Exists.elim ?_ (fun (hb : b ∈ adjoin R s) (hc : p ⟨b, hb⟩) => hc)
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
p : { x // x ∈ adjoin R s } → Prop
a : { x // x ∈ adjoin R s }
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
H0 : p 0
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
Hsmul : ∀ (r : R) (x : { x // x ∈ adjoin R s }), p x → p (r • x)
b : A
hb : b ∈ adjoin R s
⊢ ∃ x, p { val := b, property := x }
[PROOFSTEP]
apply adjoin_induction hb
[GOAL]
case Hs
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
p : { x // x ∈ adjoin R s } → Prop
a : { x // x ∈ adjoin R s }
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
H0 : p 0
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
Hsmul : ∀ (r : R) (x : { x // x ∈ adjoin R s }), p x → p (r • x)
b : A
hb : b ∈ adjoin R s
⊢ ∀ (x : A), x ∈ s → ∃ x_1, p { val := x, property := x_1 }
[PROOFSTEP]
exact fun x hx => ⟨subset_adjoin R hx, Hs x hx⟩
[GOAL]
case Hadd
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
p : { x // x ∈ adjoin R s } → Prop
a : { x // x ∈ adjoin R s }
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
H0 : p 0
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
Hsmul : ∀ (r : R) (x : { x // x ∈ adjoin R s }), p x → p (r • x)
b : A
hb : b ∈ adjoin R s
⊢ ∀ (x y : A),
    (∃ x_1, p { val := x, property := x_1 }) →
      (∃ x, p { val := y, property := x }) → ∃ x_1, p { val := x + y, property := x_1 }
[PROOFSTEP]
exact fun x y hx hy => Exists.elim hx <| fun hx' hx => Exists.elim hy <| fun hy' hy => ⟨add_mem hx' hy', Hadd _ _ hx hy⟩
[GOAL]
case H0
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
p : { x // x ∈ adjoin R s } → Prop
a : { x // x ∈ adjoin R s }
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
H0 : p 0
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
Hsmul : ∀ (r : R) (x : { x // x ∈ adjoin R s }), p x → p (r • x)
b : A
hb : b ∈ adjoin R s
⊢ ∃ x, p { val := 0, property := x }
[PROOFSTEP]
exact ⟨_, H0⟩
[GOAL]
case Hmul
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
p : { x // x ∈ adjoin R s } → Prop
a : { x // x ∈ adjoin R s }
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
H0 : p 0
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
Hsmul : ∀ (r : R) (x : { x // x ∈ adjoin R s }), p x → p (r • x)
b : A
hb : b ∈ adjoin R s
⊢ ∀ (x y : A),
    (∃ x_1, p { val := x, property := x_1 }) →
      (∃ x, p { val := y, property := x }) → ∃ x_1, p { val := x * y, property := x_1 }
[PROOFSTEP]
exact fun x y hx hy => Exists.elim hx <| fun hx' hx => Exists.elim hy <| fun hy' hy => ⟨mul_mem hx' hy', Hmul _ _ hx hy⟩
[GOAL]
case Hsmul
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
s : Set A
p : { x // x ∈ adjoin R s } → Prop
a : { x // x ∈ adjoin R s }
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
H0 : p 0
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
Hsmul : ∀ (r : R) (x : { x // x ∈ adjoin R s }), p x → p (r • x)
b : A
hb : b ∈ adjoin R s
⊢ ∀ (r : R) (x : A), (∃ x_1, p { val := x, property := x_1 }) → ∃ x_1, p { val := r • x, property := x_1 }
[PROOFSTEP]
exact fun r x hx => Exists.elim hx <| fun hx' hx => ⟨SMulMemClass.smul_mem r hx', Hsmul r _ hx⟩
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
⊢ adjoin R ⊥ = ⊥
[PROOFSTEP]
apply GaloisConnection.l_bot
[GOAL]
case gc
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
⊢ GaloisConnection (adjoin R) ?u
case u
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
⊢ NonUnitalSubalgebra R A → Set A
[PROOFSTEP]
exact NonUnitalAlgebra.gc
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
rw [← SetLike.le_def]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S T : NonUnitalSubalgebra R A
⊢ S ≤ S ⊔ T
[PROOFSTEP]
exact le_sup_left
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
rw [← SetLike.le_def]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S T : NonUnitalSubalgebra R A
⊢ T ≤ S ⊔ T
[PROOFSTEP]
exact le_sup_right
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S : Set (NonUnitalSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ (p : NonUnitalSubalgebra R A), p ∈ S → x ∈ p
[PROOFSTEP]
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S : Set (NonUnitalSubalgebra R A)
⊢ ↑(NonUnitalSubalgebra.toSubmodule (sInf S)) = ↑(sInf (NonUnitalSubalgebra.toSubmodule '' S))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S : Set (NonUnitalSubalgebra R A)
⊢ ↑(sInf S).toNonUnitalSubsemiring = ↑(sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp [iInf]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
x : A
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(NonUnitalSubalgebra.toSubmodule (⨅ (i : ι), S i)) = ↑(⨅ (i : ι), NonUnitalSubalgebra.toSubmodule (S i))
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
x : A
⊢ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure ∅) ↔ x = 0
[PROOFSTEP]
rw [NonUnitalSubsemiring.closure_empty, NonUnitalSubsemiring.coe_bot, Submodule.span_zero_singleton, Submodule.mem_bot]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
⊢ NonUnitalSubalgebra.toSubmodule ⊥ = ⊥
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
x✝ : A
⊢ x✝ ∈ NonUnitalSubalgebra.toSubmodule ⊥ ↔ x✝ ∈ ⊥
[PROOFSTEP]
simp only [mem_bot, NonUnitalSubalgebra.mem_toSubmodule, Submodule.mem_bot]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
⊢ ↑⊥ = {0}
[PROOFSTEP]
simp [Set.ext_iff, NonUnitalAlgebra.mem_bot]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
[PROOFSTEP]
exact mem_top
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤
[PROOFSTEP]
exact ⟨fun _ => mem_top, fun _ => h x⟩
[GOAL]
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : NonUnitalAlgHomClass F R A B
f : A →ₙₐ[R] B
⊢ ↑(NonUnitalSubalgebra.map f ⊥) = ↑⊥
[PROOFSTEP]
simp [NonUnitalAlgebra.coe_bot, NonUnitalSubalgebra.coe_map]
[GOAL]
R : Type u
A : Type v
B✝ : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B✝
inst✝³ : Module R B✝
inst✝² : IsScalarTower R B✝ B✝
inst✝¹ : SMulCommClass R B✝ B✝
S : NonUnitalSubalgebra R A
inst✝ : Subsingleton A
B C : NonUnitalSubalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C
[PROOFSTEP]
simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
S₁ : NonUnitalSubalgebra R B
⊢ prod ⊤ ⊤ = ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
S₁ : NonUnitalSubalgebra R B
x✝ : A × B
⊢ x✝ ∈ prod ⊤ ⊤ ↔ x✝ ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
⊢ { x // x ∈ T } →ₙₐ[R] B
[PROOFSTEP]
subst hT
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ { x // x ∈ iSup K } →ₙₐ[R] B
[PROOFSTEP]
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)
        (↑(iSup K)) (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 _ => (· * ·))
      on_goal 3 => rw [coe_iSup_of_directed dir]
      all_goals simp
    map_add' := by
      dsimp
      apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
      on_goal 3 => rw [coe_iSup_of_directed dir]
      all_goals simp
    map_smul' := fun r => by
      dsimp
      apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x) (fun _ _ => rfl)
      on_goal 2 => rw [coe_iSup_of_directed dir]
      all_goals simp }
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i j : ι
x : A
hxi : x ∈ (fun i => ↑(K i)) i
hxj : x ∈ (fun i => ↑(K i)) j
⊢ (fun i x => ↑(f i) x) i { val := x, property := hxi } = (fun i x => ↑(f i) x) j { val := x, property := hxj }
[PROOFSTEP]
let ⟨k, hik, hjk⟩ := dir i j
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i j : ι
x : A
hxi : x ∈ (fun i => ↑(K i)) i
hxj : x ∈ (fun i => ↑(K i)) j
k : ι
hik : (fun x x_1 => x ≤ x_1) (K i) (K k)
hjk : (fun x x_1 => x ≤ x_1) (K j) (K k)
⊢ (fun i x => ↑(f i) x) i { val := x, property := hxi } = (fun i x => ↑(f i) x) j { val := x, property := hxj }
[PROOFSTEP]
simp only
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i j : ι
x : A
hxi : x ∈ (fun i => ↑(K i)) i
hxj : x ∈ (fun i => ↑(K i)) j
k : ι
hik : (fun x x_1 => x ≤ x_1) (K i) (K k)
hjk : (fun x x_1 => x ≤ x_1) (K j) (K k)
⊢ ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj }
[PROOFSTEP]
rw [hf i k hik, hf j k hjk]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i j : ι
x : A
hxi : x ∈ (fun i => ↑(K i)) i
hxj : x ∈ (fun i => ↑(K i)) j
k : ι
hik : (fun x x_1 => x ≤ x_1) (K i) (K k)
hjk : (fun x x_1 => x ≤ x_1) (K j) (K k)
⊢ ↑(NonUnitalAlgHom.comp (f k) (inclusion hik)) { val := x, property := hxi } =
    ↑(NonUnitalAlgHom.comp (f k) (inclusion hjk)) { val := x, property := hxj }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
rw [coe_iSup_of_directed dir]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ∀ (x : { x // x ∈ iSup K }),
    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
        (_ :
          ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
            (fun i x => ↑(f i) x) i { val := x, property := hxi } =
              (fun i x => ↑(f i) x) j { val := x, property := hxj })
        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
      r •
        Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
          (_ :
            ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
              (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                (fun i x => ↑(f i) x) j { val := x, property := hxj })
          ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ∀ (x : { x // x ∈ iSup K }),
    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
        (_ :
          ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
            ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
      r •
        Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
          (_ :
            ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
              ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
          ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x
[PROOFSTEP]
apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x) (fun _ _ => rfl)
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ∀ (i : ι) (x : ↑↑(K i)), ↑(f i) (r • x) = r • ↑(f i) x
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
on_goal 2 => rw [coe_iSup_of_directed dir]
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ∀ (i : ι) (x : ↑↑(K i)), ↑(f i) (r • x) = r • ↑(f i) x
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
on_goal 2 => rw [coe_iSup_of_directed dir]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
rw [coe_iSup_of_directed dir]
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ∀ (i : ι) (x : ↑↑(K i)), ↑(f i) (r • x) = r • ↑(f i) x
[PROOFSTEP]
all_goals simp
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
r : R
⊢ ∀ (i : ι) (x : ↑↑(K i)), ↑(f i) (r • x) = r • ↑(f i) x
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ MulActionHom.toFun
      {
        toFun :=
          Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
            (_ :
              ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                  (fun i x => ↑(f i) x) j { val := x, property := hxj })
            ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
        map_smul' :=
          (_ :
            ∀ (r : R) (x : { x // x ∈ iSup K }),
              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                  (_ :
                    ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                      (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                        (fun i x => ↑(f i) x) j { val := x, property := hxj })
                  ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                r •
                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                    (_ :
                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
      0 =
    0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
      (_ :
        ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
          ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) 0 =
    0
[PROOFSTEP]
exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι), ↑(f i) ((fun i => 0) i) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (x y : { x // x ∈ iSup K }),
    MulActionHom.toFun
        {
          toFun :=
            Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
              (_ :
                ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                  (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                    (fun i x => ↑(f i) x) j { val := x, property := hxj })
              ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
          map_smul' :=
            (_ :
              ∀ (r : R) (x : { x // x ∈ iSup K }),
                Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                    (_ :
                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                  r •
                    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                      (_ :
                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
        (x + y) =
      MulActionHom.toFun
          {
            toFun :=
              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                (_ :
                  ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                    (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                      (fun i x => ↑(f i) x) j { val := x, property := hxj })
                ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
            map_smul' :=
              (_ :
                ∀ (r : R) (x : { x // x ∈ iSup K }),
                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                      (_ :
                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                    r •
                      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                        (_ :
                          ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                            (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                              (fun i x => ↑(f i) x) j { val := x, property := hxj })
                        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
          x +
        MulActionHom.toFun
          {
            toFun :=
              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                (_ :
                  ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                    (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                      (fun i x => ↑(f i) x) j { val := x, property := hxj })
                ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
            map_smul' :=
              (_ :
                ∀ (r : R) (x : { x // x ∈ iSup K }),
                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                      (_ :
                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                    r •
                      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                        (_ :
                          ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                            (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                              (fun i x => ↑(f i) x) j { val := x, property := hxj })
                        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
          y
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (x y : { x // x ∈ iSup K }),
    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
        (_ :
          ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
            ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (x + y) =
      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
          (_ :
            ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
              ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
          ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x +
        Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
          (_ :
            ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
              ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
          ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) y
[PROOFSTEP]
apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
[GOAL]
case hopi
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)),
    Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) (x + y) =
      Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) x + Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) y
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), ↑(f i) (x + y) = ↑(f i) x + ↑(f i) y
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
on_goal 3 => rw [coe_iSup_of_directed dir]
[GOAL]
case hopi
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)),
    Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) (x + y) =
      Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) x + Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) y
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), ↑(f i) (x + y) = ↑(f i) x + ↑(f i) y
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
on_goal 3 => rw [coe_iSup_of_directed dir]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
rw [coe_iSup_of_directed dir]
[GOAL]
case hopi
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)),
    Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) (x + y) =
      Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) x + Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) y
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), ↑(f i) (x + y) = ↑(f i) x + ↑(f i) y
[PROOFSTEP]
all_goals simp
[GOAL]
case hopi
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)),
    Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) (x + y) =
      Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) x + Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) y
[PROOFSTEP]
simp
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), ↑(f i) (x + y) = ↑(f i) x + ↑(f i) y
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (x y : { x // x ∈ iSup K }),
    MulActionHom.toFun
        {
            toMulActionHom :=
              {
                toFun :=
                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                    (_ :
                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : { x // x ∈ iSup K }),
                      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                          (_ :
                            ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                              (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                (fun i x => ↑(f i) x) j { val := x, property := hxj })
                          ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                        r •
                          Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                            (_ :
                              ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                  (fun i x => ↑(f i) x) j { val := x, property := hxj })
                            ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) },
            map_zero' :=
              (_ :
                MulActionHom.toFun
                    {
                      toFun :=
                        Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                          (_ :
                            ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                              (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                (fun i x => ↑(f i) x) j { val := x, property := hxj })
                          ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : { x // x ∈ iSup K }),
                            Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                (_ :
                                  ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                    (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                      (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                              r •
                                Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                  (_ :
                                    ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                      (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                        (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                  ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : { x // x ∈ iSup K }),
                  MulActionHom.toFun
                      {
                        toFun :=
                          Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                            (_ :
                              ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                  (fun i x => ↑(f i) x) j { val := x, property := hxj })
                            ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : { x // x ∈ iSup K }),
                              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                  (_ :
                                    ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                      (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                        (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                  ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                r •
                                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                    (_ :
                                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                        (hxj : x ∈ (fun i => ↑(K i)) j),
                                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                      (x + y) =
                    MulActionHom.toFun
                        {
                          toFun :=
                            Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                              (_ :
                                ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                  (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                    (fun i x => ↑(f i) x) j { val := x, property := hxj })
                              ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : { x // x ∈ iSup K }),
                                Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                    (_ :
                                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                        (hxj : x ∈ (fun i => ↑(K i)) j),
                                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                  r •
                                    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                      (_ :
                                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                          (hxj : x ∈ (fun i => ↑(K i)) j),
                                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                        x +
                      MulActionHom.toFun
                        {
                          toFun :=
                            Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                              (_ :
                                ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                  (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                    (fun i x => ↑(f i) x) j { val := x, property := hxj })
                              ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : { x // x ∈ iSup K }),
                                Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                    (_ :
                                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                        (hxj : x ∈ (fun i => ↑(K i)) j),
                                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                  r •
                                    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                      (_ :
                                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                          (hxj : x ∈ (fun i => ↑(K i)) j),
                                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                        y) }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          {
              toMulActionHom :=
                {
                  toFun :=
                    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                      (_ :
                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : { x // x ∈ iSup K }),
                        Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                            (_ :
                              ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                  (fun i x => ↑(f i) x) j { val := x, property := hxj })
                            ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                          r •
                            Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                              (_ :
                                ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                  (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                    (fun i x => ↑(f i) x) j { val := x, property := hxj })
                              ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) },
              map_zero' :=
                (_ :
                  MulActionHom.toFun
                      {
                        toFun :=
                          Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                            (_ :
                              ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                  (fun i x => ↑(f i) x) j { val := x, property := hxj })
                            ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : { x // x ∈ iSup K }),
                              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                  (_ :
                                    ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                      (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                        (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                  ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                r •
                                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                    (_ :
                                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                        (hxj : x ∈ (fun i => ↑(K i)) j),
                                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : { x // x ∈ iSup K }),
                    MulActionHom.toFun
                        {
                          toFun :=
                            Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                              (_ :
                                ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                  (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                    (fun i x => ↑(f i) x) j { val := x, property := hxj })
                              ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : { x // x ∈ iSup K }),
                                Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                    (_ :
                                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                        (hxj : x ∈ (fun i => ↑(K i)) j),
                                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                  r •
                                    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                      (_ :
                                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                          (hxj : x ∈ (fun i => ↑(K i)) j),
                                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                        (x + y) =
                      MulActionHom.toFun
                          {
                            toFun :=
                              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                (_ :
                                  ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                    (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                      (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : { x // x ∈ iSup K }),
                                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                      (_ :
                                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                          (hxj : x ∈ (fun i => ↑(K i)) j),
                                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                    r •
                                      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                        (_ :
                                          ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                            (hxj : x ∈ (fun i => ↑(K i)) j),
                                            (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                              (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                          x +
                        MulActionHom.toFun
                          {
                            toFun :=
                              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                (_ :
                                  ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                    (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                      (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : { x // x ∈ iSup K }),
                                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                      (_ :
                                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                          (hxj : x ∈ (fun i => ↑(K i)) j),
                                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                    r •
                                      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                        (_ :
                                          ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                            (hxj : x ∈ (fun i => ↑(K i)) j),
                                            (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                              (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                          y) }.toMulActionHom
          x *
        MulActionHom.toFun
          {
              toMulActionHom :=
                {
                  toFun :=
                    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                      (_ :
                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : { x // x ∈ iSup K }),
                        Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                            (_ :
                              ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                  (fun i x => ↑(f i) x) j { val := x, property := hxj })
                            ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                          r •
                            Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                              (_ :
                                ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                  (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                    (fun i x => ↑(f i) x) j { val := x, property := hxj })
                              ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) },
              map_zero' :=
                (_ :
                  MulActionHom.toFun
                      {
                        toFun :=
                          Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                            (_ :
                              ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                  (fun i x => ↑(f i) x) j { val := x, property := hxj })
                            ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : { x // x ∈ iSup K }),
                              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                  (_ :
                                    ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                      (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                        (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                  ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                r •
                                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                    (_ :
                                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                        (hxj : x ∈ (fun i => ↑(K i)) j),
                                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : { x // x ∈ iSup K }),
                    MulActionHom.toFun
                        {
                          toFun :=
                            Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                              (_ :
                                ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                  (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                    (fun i x => ↑(f i) x) j { val := x, property := hxj })
                              ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : { x // x ∈ iSup K }),
                                Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                    (_ :
                                      ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                        (hxj : x ∈ (fun i => ↑(K i)) j),
                                        (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                          (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                    ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                  r •
                                    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                      (_ :
                                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                          (hxj : x ∈ (fun i => ↑(K i)) j),
                                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                        (x + y) =
                      MulActionHom.toFun
                          {
                            toFun :=
                              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                (_ :
                                  ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                    (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                      (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : { x // x ∈ iSup K }),
                                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                      (_ :
                                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                          (hxj : x ∈ (fun i => ↑(K i)) j),
                                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                    r •
                                      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                        (_ :
                                          ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                            (hxj : x ∈ (fun i => ↑(K i)) j),
                                            (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                              (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                          x +
                        MulActionHom.toFun
                          {
                            toFun :=
                              Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                (_ :
                                  ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
                                    (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                      (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)),
                            map_smul' :=
                              (_ :
                                ∀ (r : R) (x : { x // x ∈ iSup K }),
                                  Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                      (_ :
                                        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                          (hxj : x ∈ (fun i => ↑(K i)) j),
                                          (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                            (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (r • x) =
                                    r •
                                      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
                                        (_ :
                                          ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i)
                                            (hxj : x ∈ (fun i => ↑(K i)) j),
                                            (fun i x => ↑(f i) x) i { val := x, property := hxi } =
                                              (fun i x => ↑(f i) x) j { val := x, property := hxj })
                                        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x) }
                          y) }.toMulActionHom
          y
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (x y : { x // x ∈ iSup K }),
    Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
        (_ :
          ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
            ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
        ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (x * y) =
      Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
          (_ :
            ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
              ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
          ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x *
        Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
          (_ :
            ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)),
              ↑(f i) { val := x, property := hxi } = ↑(f j) { val := x, property := hxj })
          ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) y
[PROOFSTEP]
apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
[GOAL]
case hopi
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)),
    Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) (x * y) =
      Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) x * Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) y
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), ↑(f i) (x * y) = ↑(f i) x * ↑(f i) y
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
on_goal 3 => rw [coe_iSup_of_directed dir]
[GOAL]
case hopi
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)),
    Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) (x * y) =
      Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) x * Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) y
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), ↑(f i) (x * y) = ↑(f i) x * ↑(f i) y
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
on_goal 3 => rw [coe_iSup_of_directed dir]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)
[PROOFSTEP]
rw [coe_iSup_of_directed dir]
[GOAL]
case hopi
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)),
    Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) (x * y) =
      Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) x * Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) y
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), ↑(f i) (x * y) = ↑(f i) x * ↑(f i) y
[PROOFSTEP]
all_goals simp
[GOAL]
case hopi
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)),
    Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) (x * y) =
      Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) x * Set.inclusion (_ : ↑(K i) ⊆ ↑(iSup K)) y
[PROOFSTEP]
simp
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
⊢ ∀ (i : ι) (x y : ↑↑(K i)), ↑(f i) (x * y) = ↑(f i) x * ↑(f i) y
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : { x // x ∈ K i }
h : K i ≤ T
⊢ ↑(iSupLift K dir f hf T hT) (↑(inclusion h) x) = ↑(f i) x
[PROOFSTEP]
subst T
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i : ι
x : { x // x ∈ K i }
h : K i ≤ iSup K
⊢ ↑(iSupLift K dir f hf (iSup K) (_ : iSup K = iSup K)) (↑(inclusion h) x) = ↑(f i) x
[PROOFSTEP]
dsimp [iSupLift]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i : ι
x : { x // x ∈ K i }
h : K i ≤ iSup K
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
      (_ :
        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
          (fun i x => ↑(f i) x) i { val := x, property := hxi } = (fun i x => ↑(f i) x) j { val := x, property := hxj })
      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) (↑(inclusion h) x) =
    ↑(f i) x
[PROOFSTEP]
apply Set.iUnionLift_inclusion
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i : ι
x : { x // x ∈ K i }
h : K i ≤ iSup K
⊢ ↑(K i) ⊆ ↑(iSup K)
[PROOFSTEP]
exact h
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
⊢ NonUnitalAlgHom.comp (iSupLift K dir f hf T hT) (inclusion h) = f i
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : { x // x ∈ K i }
⊢ ↑(NonUnitalAlgHom.comp (iSupLift K dir f hf T hT) (inclusion h)) x✝ = ↑(f i) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : { x // x ∈ K i }
hx : ↑x ∈ T
⊢ ↑(iSupLift K dir f hf T hT) { val := ↑x, property := hx } = ↑(f i) x
[PROOFSTEP]
subst hT
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i : ι
x : { x // x ∈ K i }
hx : ↑x ∈ iSup K
⊢ ↑(iSupLift K dir f hf (iSup K) (_ : iSup K = iSup K)) { val := ↑x, property := hx } = ↑(f i) x
[PROOFSTEP]
dsimp [iSupLift]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i : ι
x : { x // x ∈ K i }
hx : ↑x ∈ iSup K
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
      (_ :
        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
          (fun i x => ↑(f i) x) i { val := x, property := hxi } = (fun i x => ↑(f i) x) j { val := x, property := hxj })
      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) { val := ↑x, property := hx } =
    ↑(f i) x
[PROOFSTEP]
apply Set.iUnionLift_mk
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : { x // x ∈ T }
hx : ↑x ∈ K i
⊢ ↑(iSupLift K dir f hf T hT) x = ↑(f i) { val := ↑x, property := hx }
[PROOFSTEP]
subst hT
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i : ι
x : { x // x ∈ iSup K }
hx : ↑x ∈ K i
⊢ ↑(iSupLift K dir f hf (iSup K) (_ : iSup K = iSup K)) x = ↑(f i) { val := ↑x, property := hx }
[PROOFSTEP]
dsimp [iSupLift]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
S : NonUnitalSubalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = NonUnitalAlgHom.comp (f j) (inclusion h)
i : ι
x : { x // x ∈ iSup K }
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
      (_ :
        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
          (fun i x => ↑(f i) x) i { val := x, property := hxi } = (fun i x => ↑(f i) x) j { val := x, property := hxj })
      ↑(iSup K) (_ : ↑(iSup K) ⊆ ⋃ (i : ι), ↑(K i)) x =
    ↑(f i) { val := ↑x, property := hx }
[PROOFSTEP]
apply Set.iUnionLift_of_mem
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
⊢ r • a ∈ Set.center A
[PROOFSTEP]
simp [Set.mem_center_iff, mul_smul_comm, smul_mul_assoc, (Set.mem_center_iff A).mp ha]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
r : R
a : A
ha : a ∈ Set.centralizer s
x : A
hx : x ∈ s
⊢ x * r • a = r • a * x
[PROOFSTEP]
rw [mul_smul_comm, smul_mul_assoc, ha x hx]
