awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
S : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)
eq₁ :
  Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, j)) : TopCat))
    (CategoryStruct.comp (Y :=
        pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k)))
        (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
        (pullback.fst (CategoryTheory.Functor.map (forget C) (D.f i j))
          (CategoryTheory.Functor.map (forget C) (D.f i k))) :
      Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, j)))
    (Hom.base (pullback.fst (D.f i j) (D.f i k)))
⊢ Eq (α := Set (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.fst (D.f i j) (D.f i k)))) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : TopCat) : Type v)) ⁻¹'
        S))
    (Set.preimage (β := (↑(↑(D.U i) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i k).base) :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.f i j).base) :
          (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ''
        S))
have eq₂ : Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, k)) : TopCat))
  (CategoryStruct.comp (Y :=
      pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
        (CategoryTheory.Functor.map (forget C) (D.f i k)))
      (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
      (pullback.snd (CategoryTheory.Functor.map (forget C) (D.f i j))
        (CategoryTheory.Functor.map (forget C) (D.f i k))) :
    Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, k)))
  (Hom.base (pullback.snd (D.f i j) (D.f i k)))
Tactic: have eq₂ : _ = (π₂ i, j, k).base := PreservesPullback.iso_hom_snd (forget C) _ _
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
⊢ op
      (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
        (IsOpenMap.functor (f := Hom.base (pullback.snd (D.f i j) (D.f i k))) ⋯)
        (unop
          (op
            ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                  Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                    Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
              (unop (op U)))))) =
    (Opens.map (D.f i k).base).op.obj (op (Functor.obj (IsOpenMap.functor (f := (D.f i j).base) ⋯) U))
have dsimp : op
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
            (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
          (↑{
                carrier :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                          (Hom.base (pullback.fst (D.f i j) (D.f i k)))) :
                      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                        (↑(↑(D.V (i, j)) : TopCat) : Type v)) ⁻¹'
                    (↑U : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)),
                is_open' := sorry : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) } :
            Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)),
      is_open' := sorry } =
  op
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (D.f i k).base) :
            (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
          (↑{
                carrier :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (D.f i j).base) :
                      (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ''
                    (↑U : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)),
                is_open' := sorry : Opens (↑(↑(D.U i) : TopCat) : Type v) } :
            Set (↑(↑(D.U i) : TopCat) : Type v)),
      is_open' := sorry : Opens (↑(↑(D.V (i, k)) : TopCat) : Type v) }
Tactic: dsimp only [Functor.op, IsOpenMap.functor, Opens.map, unop_op]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop
            (op
              ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                    Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)
have this : ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
  NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k) ≫ D.f i j)) U =
    NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k)) U ≫
      (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom sorry)
Tactic: have := PresheafedSpace.congr_app (@pullback.condition _ _ _ _ _ (D.f i j) (D.f i k) _)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop
            (op
              ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                    Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)
have rw : (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
  ((D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫ (D.V (i, j)).presheaf.map (eqToHom sorry)) ≫
    NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop
            (op
              ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                    Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom sorry)
Tactic: rw [← cancel_epi (inv ((D.f_open i j).invApp _ U)), IsIso.inv_hom_id_assoc,
    IsOpenImmersion.inv_invApp]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    ((D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯)) ≫
      NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
        invApp (pullback.snd (D.f i j) (D.f i k))
            (unop
              (op
                ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                      Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                        Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                  (unop (op U))))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)
have simp_rw : (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
  (D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
    (D.V (i, j)).presheaf.map (eqToHom sorry) ≫
      NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
        invApp (pullback.snd (D.f i j) (D.f i k))
            ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                  Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                    Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
              U) ≫
          (D.V (i, k)).presheaf.map (eqToHom sorry)
Tactic: simp_rw [Category.assoc]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
⊢ ∃ (eq :
    (Opens.map (D.t k i).base).op.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) =
      op
        (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
          (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
          (D.V (k, i)).presheaf.map (eqToHom eq) =
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))
have w : (Opens.map (D.t k i).base).op.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) =
  op
    (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      (opensFunctor (pullback.fst (D.f k i) (D.f k j))) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
w :
  (Opens.map (D.t k i).base).op.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) =
    op
      (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (opensFunctor (pullback.fst (D.f k i) (D.f k j))) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))
⊢ ∃ (eq :
    (Opens.map (D.t k i).base).op.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) =
      op
        (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
          (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
          (D.V (k, i)).presheaf.map (eqToHom eq) =
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))
have h : Eq (α :=
  (pullback (D.f i j) (D.f i k)).presheaf.obj (op U) ⟶
    (D.V (k, i)).presheaf.obj
      (op
        (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
          (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))))
  (CategoryStruct.comp (Y :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))
    (invApp (pullback.snd (D.f i j) (D.f i k)) U)
    ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom sorry)))
  ((D.t' k i j).c.app (op U) ≫
    invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
⊢ (Opens.map (D.t k i).base).op.obj
      (op (Functor.obj (IsOpenMap.functor (f := Hom.base (pullback.snd (D.f i j) (D.f i k))) ⋯) U)) =
    op
      (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (IsOpenMap.functor (f := Hom.base (pullback.fst (D.f k i) (D.f k j))) ⋯)
        (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))
have w : op
    {
      carrier :=
        Set.preimage (β := (↑(↑(D.V (i, k)) : TopCat) : Type v))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                TopCat.carrier) (D.t k i).base) :
            (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                  (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
              (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
            (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))),
      is_open' := sorry : Opens (↑(↑(D.V (k, i)) : TopCat) : Type v) } =
  op
    {
      carrier :=
        Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                TopCat.carrier) (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat))
                (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
            (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (D.t' k i j).base) :
              (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
                (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) ⁻¹'
            (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))),
      is_open' := sorry }
Tactic: dsimp only [Functor.op, Opens.map, IsOpenMap.functor, unop_op, Opens.coe_mk]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
⊢ Eq (α := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
    (Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t' k i j).base) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) ⁻¹'
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
have this : pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k)
Tactic: have := (𝖣.t_fac k i j).symm
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this : pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k)
⊢ Eq (α := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
    (Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t' k i j).base) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) ⁻¹'
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
have this₁ : inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = pullback.snd (D.f i j) (D.f i k)
Tactic: rw [← IsIso.inv_comp_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this : inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = pullback.snd (D.f i j) (D.f i k)
⊢ Eq (α := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
    (Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t' k i j).base) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) ⁻¹'
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
have this₁ : Hom.base (pullback.snd (D.f i j) (D.f i k)) = (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).base
Tactic: replace this := (congr_arg ((PresheafedSpace.Hom.base ·)) this).symm
Cleared hypotheses: this