awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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 :
  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' := ⋯ : 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' := ⋯ }
⊢ (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))))))

Tactic:
dsimp only [Functor.op, Opens.map, IsOpenMap.functor, unop_op, Opens.coe_mk]

Premises used: CategoryTheory.Functor.op, TopologicalSpace.Opens.coe_mk, IsOpenMap.functor, Opposite.unop_op, TopologicalSpace.Opens.map
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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)
⊢ 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
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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)
⊢ 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

Premises used: CategoryTheory.IsIso.inv_comp_eq
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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)
⊢ 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
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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 :
  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
⊢ Eq.{v + 1} (α := C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v), (↑(↑(D.V (i, k)) : TopCat) : Type v)))
    ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
      (Hom.base (pullback.snd (D.f i j) (D.f i k))))
    ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
      (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 (TopCat.Hom.hom ·) this
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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.{v + 1} (α := C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v), (↑(↑(D.V (i, k)) : TopCat) : Type v)))
    ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
      (Hom.base (pullback.snd (D.f i j) (D.f i k))))
    ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
      (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).base)
⊢ Eq.{v + 1} (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    ((fun (x : C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v), (↑(↑(D.V (i, k)) : TopCat) : Type v))) ↦
        x.toFun)
      ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
        (Hom.base (pullback.snd (D.f i j) (D.f i k)))))
    ((fun (x : C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v), (↑(↑(D.V (i, k)) : TopCat) : Type v))) ↦
        x.toFun)
      ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
        (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 (ContinuousMap.toFun ·) this
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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))))
⊢ Function.Injective (α := (↑(↑(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)
          (D.t k i).base) :
      (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))

Tactic:
Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩

Premises used: CategoryTheory.GlueData.t, Function.HasLeftInverse.injective, CategoryTheory.ConcreteCategory.hom, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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 :
  ∀ (x : (↑(↑(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 i k).base :
          (a : (↑(↑(D.V (i, k)) : 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).base :
              (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
            x :
          (↑(↑(D.V (i, k)) : TopCat) : Type v)) =
      x
⊢ Function.Injective (α := (↑(↑(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)
          (D.t k i).base) :
      (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))

Tactic:
refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩

Premises used: CategoryTheory.GlueData.t, Function.HasLeftInverse.injective, CategoryTheory.ConcreteCategory.hom, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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 : (↑(↑(D.V (k, i)) : 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).base ≫ (D.t i k).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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 ≫ D.t i k).base :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
w₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Hom.base (𝟙 (D.V (k, i)))) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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.V (k, i)) : TopCat)) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
w₄ w₅ : x = x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t i k).base :
        (a : (↑(↑(D.V (i, k)) : 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).base :
            (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
          x :
        (↑(↑(D.V (i, k)) : TopCat) : Type v)) =
    x

Tactic:
rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.GlueData.t_inv, AlgebraicGeometry.PresheafedSpace.id_base, AlgebraicGeometry.PresheafedSpace.comp_base, CategoryTheory.ConcreteCategory.id_apply, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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 (α := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(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)) ''
        (↑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))))

Tactic:
congr_arg (_ '' ·) ?_

Premises used: congr_arg, Set.image
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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 (α := Set (↑(↑(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)) ''
      (↑U : Set (↑(↑(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)) ⁻¹'
      (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)))

Tactic:
congr_fun ?_ _

Premises used: congr_fun
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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 :
  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)))
⊢ Eq (α := Set (↑(↑(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)) ''
      (↑U : Set (↑(↑(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)) ⁻¹'
      (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)))

Tactic:
refine congr_fun ?_ _

Premises used: congr_fun
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
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)))

Tactic:
Set.image_eq_preimage_of_inverse ?_ ?_

Premises used: Set.image_eq_preimage_of_inverse