-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
h₁_1 : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) x : ↥(D.obj i))
h₂ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
      ↥(D.map k.hom ⁻¹ᵁ U))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
          ↥(D.map k.hom ⁻¹ᵁ U)) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
rwa :
  ∀ (h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f ≫ k.hom)) x : ↥(D.obj i)))
    (h₂ :
      Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
          ↥(D.map k.hom ⁻¹ᵁ U)))
    (e :
      Eq (α := ↥(D.obj k.left))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (X := (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base
                  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
              (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
            (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
              ↥(D.map k.hom ⁻¹ᵁ U)) :
          ↥(D.obj k.left))
        ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))),
    x ∈ D.map j.hom ⁻¹ᵁ U
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
have rwa₁ : ∀ (h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map j.hom) x : ↥(D.obj i)))
  (h₂ :
    Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
      (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
        ↥(D.map k.hom ⁻¹ᵁ U)))
  (e :
    Eq (α := ↥(D.obj k.left))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
            (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
          (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁_1 :
            ↥(D.map k.hom ⁻¹ᵁ U)) :
        ↥(D.obj k.left))
      ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))),
  x ∈ D.map j.hom ⁻¹ᵁ U
Tactic: rwa [← D.map_comp, Over.w f] at h₁
Cleared hypotheses: h₁, h₂, e