K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s✝ t : Subfield K
f✝ f : K →+* L
s : Subfield K
y : L
⊢ (y ∈
      let src := Subring.map f s.toSubring;
      {
        toSubring :=
          { toSubsemiring := src.toSubsemiring,
            neg_mem' :=
              (_ :
                ∀ {x : L},
                  x ∈ (Subring.map f s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
                    -x ∈ (Subring.map f s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) },
        inv_mem' :=
          (_ :
            ∀ (x : L),
              x ∈
                  { toSubsemiring := (Subring.map f s.toSubring).toSubsemiring,
                            neg_mem' :=
                              (_ :
                                ∀ {x : L},
                                  x ∈ (Subring.map f s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
                                    -x ∈
                                      (Subring.map f
                                                s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
                x⁻¹ ∈
                  { toSubsemiring := (Subring.map f s.toSubring).toSubsemiring,
                            neg_mem' :=
                              (_ :
                                ∀ {x : L},
                                  x ∈ (Subring.map f s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
                                    -x ∈
                                      (Subring.map f
                                                s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }) ↔
    ∃ x, x ∈ s ∧ ↑f x = y
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s✝ t : Subfield K
f✝ f : K →+* L
s : Subfield K
y : L
⊢ y ∈ map f s ↔ ∃ x, x ∈ s ∧ ↑f x = y
unfold map
no goals
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s✝ t : Subfield K
f✝ f : K →+* L
s : Subfield K
y : L
⊢ (y ∈
      let src := Subring.map f s.toSubring;
      {
        toSubring :=
          { toSubsemiring := src.toSubsemiring,
            neg_mem' :=
              (_ :
                ∀ {x : L},
                  x ∈ (Subring.map f s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
                    -x ∈ (Subring.map f s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) },
        inv_mem' :=
          (_ :
            ∀ (x : L),
              x ∈
                  { toSubsemiring := (Subring.map f s.toSubring).toSubsemiring,
                            neg_mem' :=
                              (_ :
                                ∀ {x : L},
                                  x ∈ (Subring.map f s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
                                    -x ∈
                                      (Subring.map f
                                                s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
                x⁻¹ ∈
                  { toSubsemiring := (Subring.map f s.toSubring).toSubsemiring,
                            neg_mem' :=
                              (_ :
                                ∀ {x : L},
                                  x ∈ (Subring.map f s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
                                    -x ∈
                                      (Subring.map f
                                                s.toSubring).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }) ↔
    ∃ x, x ∈ s ∧ ↑f x = y
simp only [mem_mk, Subring.mem_mk, Subring.mem_toSubsemiring, Subring.mem_map, mem_toSubring]