R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ (x ∈ ⨆ (i : ι), S i) ↔ ∃ i, x ∈ S i
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
let U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup)
    (Subsemigroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
    (⨆ i, (S i).toAddSubmonoid)
    (AddSubmonoid.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
H : (⨆ (i : ι), S i) ≤ U
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i

case H
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ (⨆ (i : ι), S i) ≤ U
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
suffices H : (⨆ i, S i) ≤ U
case H
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ (⨆ (i : ι), S i) ≤ U
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
H : (⨆ (i : ι), S i) ≤ U
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i

case H
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ (⨆ (i : ι), S i) ≤ U
simpa using @H x
no goals
case H
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.274576
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ (⨆ (i : ι), S i) ≤ U
exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩