R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring 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✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring 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✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
let U : Subring R :=
  Subring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup)
    (Submonoid.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
    (AddSubgroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ (⨆ (i : ι), S i) ≤ U
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
suffices (⨆ i, S i) ≤ U by intro h; simpa using (this h)
no goals
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
⊢ (⨆ (i : ι), S i) ≤ U
exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : (⨆ (i : ι), S i) ≤ U
h : x ∈ ⨆ (i : ι), S i
⊢ ∃ i, x ∈ S i
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : (⨆ (i : ι), S i) ≤ U
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
intro h
no goals
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : Subring R :=
  Subring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), (S i).toSubmonoid) (⨆ (i : ι), toAddSubgroup (S i))
    (_ : ↑(⨆ (i : ι), (S i).toSubmonoid) = ⋃ (i : ι), ↑(S i).toSubmonoid)
    (_ : ↑(⨆ (i : ι), toAddSubgroup (S i)) = ⋃ (i : ι), ↑(toAddSubgroup (S i)))
this : (⨆ (i : ι), S i) ≤ U
h : x ∈ ⨆ (i : ι), S i
⊢ ∃ i, x ∈ S i
simpa using (this h)