R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) S
i : ι := Nonempty.some (_ : Nonempty ι)
⊢ ∃ i, 0 ∈ S i
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) S
i : ι := Nonempty.some (_ : Nonempty ι)
⊢ 0 ∈
    {
          toSubsemigroup :=
            { carrier := ⋃ (i : ι), ↑(S i),
              mul_mem' :=
                (_ : ∀ {a b : A}, (a ∈ ⋃ (i : ι), ↑(S i)) → (b ∈ ⋃ (i : ι), ↑(S i)) → a * b ∈ ⋃ (i : ι), ↑(S i)) },
          one_mem' :=
            (_ :
              1 ∈
                { carrier := ⋃ (i : ι), ↑(S i),
                    mul_mem' :=
                      (_ :
                        ∀ {a b : A},
                          (a ∈ ⋃ (i : ι), ↑(S i)) →
                            (b ∈ ⋃ (i : ι), ↑(S i)) → a * b ∈ ⋃ (i : ι), ↑(S i)) }.carrier) }.toSubsemigroup.carrier
simp only [Set.mem_iUnion, SetLike.mem_coe]
no goals
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) S
i : ι := Nonempty.some (_ : Nonempty ι)
⊢ ∃ i, 0 ∈ S i
exact ⟨i, zero_mem _⟩
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) S
i : ι := Nonempty.some (_ : Nonempty ι)
⊢ ∃ i, 1 ∈ S i
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) S
i : ι := Nonempty.some (_ : Nonempty ι)
⊢ 1 ∈
    { carrier := ⋃ (i : ι), ↑(S i),
        mul_mem' :=
          (_ : ∀ {a b : A}, (a ∈ ⋃ (i : ι), ↑(S i)) → (b ∈ ⋃ (i : ι), ↑(S i)) → a * b ∈ ⋃ (i : ι), ↑(S i)) }.carrier
simp only [Set.mem_iUnion, SetLike.mem_coe]
no goals
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) S
i : ι := Nonempty.some (_ : Nonempty ι)
⊢ ∃ i, 1 ∈ S i
exact ⟨i, one_mem _⟩