-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
i : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (i (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s : Set ↥X
hs : s = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
j : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen_1 :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (j U) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (j (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
t : Set ↥X
ht : t = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(j U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
h :
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
        X.IdealSheafData }.ideal =
    { ideal := j, map_ideal_basicOpen := map_ideal_basicOpen_1, supportSet := t,
        supportSet_eq_iInter_zeroLocus := ht }.ideal
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
      X.IdealSheafData } =
    { ideal := j, map_ideal_basicOpen := map_ideal_basicOpen_1, supportSet := t, supportSet_eq_iInter_zeroLocus := ht }
have subst : ∀
  (map_ideal_basicOpen_2 :
    ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op))
            ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                  supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
              U) :
          Ideal (↑Γ(X, X.basicOpen f) : Type u))
        ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs }.ideal
            (X.affineBasicOpen f) :
          Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)))
  (ht :
    t =
      ⋂ (U : (↑X.affineOpens : Type u)),
        X.zeroLocus
          (↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                    supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
                U) :
            Set (↑Γ(X, (↑U : X.Opens)) : Type u))),
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
      X.IdealSheafData } =
    {
      ideal :=
        { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
            supportSet_eq_iInter_zeroLocus := hs }.ideal,
      map_ideal_basicOpen := map_ideal_basicOpen_2, supportSet := t, supportSet_eq_iInter_zeroLocus := ht }
Tactic: subst h
Cleared hypotheses: j, map_ideal_basicOpen_1, ht, h