-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
refine_1 :
  ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (a : A) (ha : a ∈ s),
    Membership.mem (γ := Subalgebra R ↥(adjoin R s))
      (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) a ⋯)
refine_2 :
  ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (r : R),
    Membership.mem (α := ↥(adjoin R s)) (γ := Subalgebra R ↥(adjoin R s))
      (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
          ((algebraMap R A : (a : R) → A) r) ⋯ :
        ↥(adjoin R s))
refine_3 :
  ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x x_1 : A)
    (x_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
    (x_3 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1),
    Membership.mem (γ := Subalgebra R ↥(adjoin R s))
        (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x x_2) →
      Membership.mem (γ := Subalgebra R ↥(adjoin R s))
          (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_1 x_3) →
        Membership.mem (γ := Subalgebra R ↥(adjoin R s))
          (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x + x_1) ⋯)
⊢ Eq (α := Subalgebra R ↥(adjoin R s))
    (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s)) ⊤
have refine_4 : ∀ (x : ↥(adjoin R s)) (x : A) (hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x x_1 : A)
  (x_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x)
  (x_3 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x_1),
  Membership.mem (γ := Subalgebra R ↥(adjoin R s))
      (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x x_2) →
    Membership.mem (γ := Subalgebra R ↥(adjoin R s))
        (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) x_1 x_3) →
      Membership.mem (γ := Subalgebra R ↥(adjoin R s))
        (adjoin R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R s) x) (x * x_1) sorry)
Tactic: refine eq_top_iff.2 fun ⟨x, hx⟩ ↦
      adjoin_induction (fun a ha ↦ ?_) (fun r ↦ ?_) (fun _ _ _ _ ↦ ?_) (fun _ _ _ _ ↦ ?_) hx