K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
⊢ (x ∈ ⨆ (i : ι), S i) ↔ ∃ i, x ∈ S i
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
⊢ x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
suffices x ∈ closure (⋃ i, (S i : Set K)) → ∃ i, x ∈ S i by
  simpa only [closure_iUnion, closure_eq]
case refine'_1
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∃ i, 1 ∈ S i

case refine'_2
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : K), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x + y ∈ S i

case refine'_3
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x : K), (∃ i, x ∈ S i) → ∃ i, -x ∈ S i

case refine'_4
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x : K), (∃ i, x ∈ S i) → ∃ i, x⁻¹ ∈ S i

case refine'_5
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : K), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
⊢ x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
refine' fun hx => closure_induction hx (fun x => Set.mem_iUnion.mp) _ _ _ _ _
no goals
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
this : x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
⊢ (x ∈ ⨆ (i : ι), S i) → ∃ i, x ∈ S i
simpa only [closure_iUnion, closure_eq]
no goals
case refine'_1
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∃ i, 1 ∈ S i
exact hι.elim fun i => ⟨i, (S i).one_mem⟩
case refine'_2.intro.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : K
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x + y ∈ S i
case refine'_2
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : K), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x + y ∈ S i
rintro x y ⟨i, hi⟩ ⟨j, hj⟩
case refine'_2.intro.intro.intro.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : K
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hki : S i ≤ S k
hkj : S j ≤ S k
⊢ ∃ i, x + y ∈ S i
case refine'_2.intro.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : K
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x + y ∈ S i
obtain ⟨k, hki, hkj⟩ := hS i j
no goals
case refine'_2.intro.intro.intro.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : K
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hki : S i ≤ S k
hkj : S j ≤ S k
⊢ ∃ i, x + y ∈ S i
exact ⟨k, (S k).add_mem (hki hi) (hkj hj)⟩
case refine'_3.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x : K
i : ι
hi : x ∈ S i
⊢ ∃ i, -x ∈ S i
case refine'_3
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x : K), (∃ i, x ∈ S i) → ∃ i, -x ∈ S i
rintro x ⟨i, hi⟩
no goals
case refine'_3.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x : K
i : ι
hi : x ∈ S i
⊢ ∃ i, -x ∈ S i
exact ⟨i, (S i).neg_mem hi⟩
case refine'_4.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x : K
i : ι
hi : x ∈ S i
⊢ ∃ i, x⁻¹ ∈ S i
case refine'_4
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x : K), (∃ i, x ∈ S i) → ∃ i, x⁻¹ ∈ S i
rintro x ⟨i, hi⟩
no goals
case refine'_4.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x : K
i : ι
hi : x ∈ S i
⊢ ∃ i, x⁻¹ ∈ S i
exact ⟨i, (S i).inv_mem hi⟩
case refine'_5.intro.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : K
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
case refine'_5
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x : K
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : K), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
rintro x y ⟨i, hi⟩ ⟨j, hj⟩
case refine'_5.intro.intro.intro.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : K
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hki : S i ≤ S k
hkj : S j ≤ S k
⊢ ∃ i, x * y ∈ S i
case refine'_5.intro.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : K
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
obtain ⟨k, hki, hkj⟩ := hS i j
no goals
case refine'_5.intro.intro.intro.intro
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : K
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : K
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hki : S i ≤ S k
hkj : S j ≤ S k
⊢ ∃ i, x * y ∈ S i
exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩