awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (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))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
⊢ Eq (α :=
    (x : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
      Set (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    (Set.image
      (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)))
    (Set.preimage
      (⇑(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)))
have w : Function.LeftInverse (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) (β :=
  (↑(↑(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)
        (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))
  (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
      (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
Tactic: refine Set.image_eq_preimage_of_inverse ?_ ?_
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (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))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
w :
  Function.LeftInverse (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) (β :=
    (↑(↑(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)
          (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))
    (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
⊢ Eq (α :=
    (x : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
      Set (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    (Set.image
      (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)))
    (Set.preimage
      (⇑(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)))
have w₁ : Function.RightInverse (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) (β :=
  (↑(↑(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)
        (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))
  (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
      (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
Tactic: refine Set.image_eq_preimage_of_inverse ?_ ?_
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (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))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(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)
          (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))
      ((TopCat.Hom.hom (inv (D.t' k i j)).base :
            (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
              (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          x :
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) =
    x
have w : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        ((inv (D.t' k i j)).base ≫ (D.t' k i j).base) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base,
        ConcreteCategory.id_apply]
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (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))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
w :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          ((inv (D.t' k i j)).base ≫ (D.t' k i j).base) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
      x =
    x
⊢ (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))
      ((TopCat.Hom.hom (inv (D.t' k i j)).base :
            (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
              (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          x :
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) =
    x
have w₁ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        (inv (D.t' k i j) ≫ D.t' k i j).base :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base,
        ConcreteCategory.id_apply]
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (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))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
w :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          ((inv (D.t' k i j)).base ≫ (D.t' k i j).base) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
      x =
    x
w₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (inv (D.t' k i j) ≫ D.t' k i j).base :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
      x =
    x
⊢ (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))
      ((TopCat.Hom.hom (inv (D.t' k i j)).base :
            (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
              (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          x :
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) =
    x
have w₂ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        (Hom.base (𝟙 (pullback (D.f i j) (D.f i k)))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base,
        ConcreteCategory.id_apply]
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (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))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)
⊢ (TopCat.Hom.hom (inv (D.t' k i j)).base :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(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)
              (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))
          x :
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) =
    x
have w : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        ((D.t' k i j).base ≫ (inv (D.t' k i j)).base) :
      (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.hom_inv_id, id_base,
        ConcreteCategory.id_apply]
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (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))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)
w :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          ((D.t' k i j).base ≫ (inv (D.t' k i j)).base) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      x =
    x
⊢ (TopCat.Hom.hom (inv (D.t' k i j)).base :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(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)
              (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))
          x :
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) =
    x
have w₁ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        (D.t' k i j ≫ inv (D.t' k i j)).base :
      (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.hom_inv_id, id_base,
        ConcreteCategory.id_apply]
-- 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)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (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))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (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))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)
w :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          ((D.t' k i j).base ≫ (inv (D.t' k i j)).base) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      x =
    x
w₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t' k i j ≫ inv (D.t' k i j)).base :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      x =
    x
⊢ (TopCat.Hom.hom (inv (D.t' k i j)).base :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(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)
              (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))
          x :
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) =
    x
have w₂ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        (Hom.base (𝟙 (pullback (D.f k i) (D.f k j)))) :
      (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.hom_inv_id, id_base,
        ConcreteCategory.id_apply]
-- 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 (α :=
    (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 ⋯)))
    ((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 (α :=
  (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) 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))))))))
  ((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))
  (NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k)))
      (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
    (D.t' k i j).c.app
        (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k)))))
          (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C (D.t' k i j).base) (pullback (D.f k i) (D.f k j)).presheaf).map
          (eqToHom sorry) ≫
        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: rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc,
      (D.t' k i j).c.naturality_assoc]