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 s).toSubring ↔ x ∈ ⨅ (t : Subfield K) (_ : t ∈ s), t.toSubring
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s : Set (Subfield K)
⊢ (sInf s).toSubring = ⨅ (t : Subfield K) (_ : t ∈ s), t.toSubring
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
⊢ (∀ (p : Subfield K), p ∈ s → x ∈ p) ↔ x ∈ ⨅ (t : Subfield K) (_ : t ∈ s), t.toSubring
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 s).toSubring ↔ x ∈ ⨅ (t : Subfield K) (_ : t ∈ s), t.toSubring
rw [mem_toSubring, mem_sInf]
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
⊢ (∀ (p : Subfield K), p ∈ s → x ∈ p) ↔ ∀ (p : Subring K), (p ∈ Set.range fun t => ⨅ (_ : t ∈ s), t.toSubring) → x ∈ p
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
⊢ (∀ (p : Subfield K), p ∈ s → x ∈ p) ↔ x ∈ ⨅ (t : Subfield K) (_ : t ∈ s), t.toSubring
erw [Subring.mem_sInf]
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
⊢ (∀ (p : Subfield K), p ∈ s → x ∈ p) ↔ ∀ (p : Subring K), (p ∈ Set.range fun t => ⨅ (_ : t ∈ s), t.toSubring) → x ∈ p
exact
  ⟨fun h p ⟨p', hp⟩ => hp ▸ Subring.mem_sInf.mpr fun p ⟨hp', hp⟩ => hp ▸ h _ hp', fun h p hp =>
    h p.toSubring
      ⟨p,
        Subring.ext fun x =>
          ⟨fun hx => Subring.mem_sInf.mp hx _ ⟨hp, rfl⟩, fun hx =>
            Subring.mem_sInf.mpr fun p' ⟨_, p'_eq⟩ => p'_eq ▸ hx⟩⟩⟩