-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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
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 ⋯).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 }
⊢ { 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 }

Tactic:
subst h