case h
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
x : K
⊢ x ∈ ↑(sInf (toSubring '' S)) ↔ x ∈ ⋂ (s : Subfield K) (_ : s ∈ S), ↑s
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
⊢ ↑(sInf (toSubring '' S)) = ⋂ (s : Subfield K) (_ : s ∈ S), ↑s
ext x
case h
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
x : K
⊢ (∀ (i : Subring K), x ∈ ⋂ (_ : i ∈ toSubring '' S), ↑i) ↔ ∀ (i : Subfield K), x ∈ ⋂ (_ : i ∈ S), ↑i
case h
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
x : K
⊢ x ∈ ↑(sInf (toSubring '' S)) ↔ x ∈ ⋂ (s : Subfield K) (_ : s ∈ S), ↑s
rw [Subring.coe_sInf, Set.mem_iInter, Set.mem_iInter]
no goals
case h
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
x : K
⊢ (∀ (i : Subring K), x ∈ ⋂ (_ : i ∈ toSubring '' S), ↑i) ↔ ∀ (i : Subfield K), x ∈ ⋂ (_ : i ∈ S), ↑i
exact
  ⟨fun h s s' ⟨s_mem, s'_eq⟩ => h s.toSubring _ ⟨⟨s, s_mem, rfl⟩, s'_eq⟩,
    fun h s s' ⟨⟨s'', s''_mem, s_eq⟩, (s'_eq : ↑s = s')⟩ =>
    h s'' _ ⟨s''_mem, by simp [← s_eq, ← s'_eq]⟩⟩
no goals
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
S : Set (Subfield K)
x : K
h : ∀ (i : Subfield K), x ∈ ⋂ (_ : i ∈ S), ↑i
s : Subring K
s' : Set K
x✝ : s' ∈ Set.range fun h => ↑s
s'' : Subfield K
s''_mem : s'' ∈ S
s_eq : s''.toSubring = s
s'_eq : ↑s = s'
⊢ (fun h => ↑s'') s''_mem = s'
simp [← s_eq, ← s'_eq]