-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
simp_rw :
  Membership.mem (γ := IntermediateField F E)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subfield.toSubring
              (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))),
        algebraMap_mem' := ⋯, inv_mem' := ⋯ }
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₁ :
  Membership.mem (γ := Subsemiring E)
      (Subring.toSubsemiring
          (Subfield.toSubring
            (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S))) :
        Subsemiring E)
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₂ :
  Membership.mem (γ := Subring E)
      (Subfield.toSubring (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)))
      x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₃ :
  Membership.mem (γ := Subfield E)
      (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₄ :
  (∃ (y : E),
      Membership.mem (γ := Subring E)
          (Subring.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) y ∧
        ∃ (z : E),
          Membership.mem (γ := Subring E)
              (Subring.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ S)) z ∧
            y / z = x) ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
simp_rw₅ :
  (∃ (y : E),
      Membership.mem (γ := Subring E) (Subalgebra.toSubring (Algebra.adjoin F S)) y ∧
        ∃ (z : E), Membership.mem (γ := Subring E) (Subalgebra.toSubring (Algebra.adjoin F S)) z ∧ y / z = x) ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F S) x ↔
    ∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
have simp_rw₆ : (∃ (y : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) y ∧
      ∃ (z : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) z ∧ y / z = x) ↔
  ∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) s ∧ x = r / s
Tactic: simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_comm]