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)
y : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
⊢ inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) = pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
have h : pullback.fst (D.f k i) (D.f k j) = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
Tactic: rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]
-- 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)
y : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
h : pullback.fst (D.f k i) (D.f k j) = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
⊢ inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) = pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
have h₁ : Eq (α := pullback (D.f k i) (D.f k j) ⟶ D.V (k, i)) (pullback.fst (D.f k i) (D.f k j))
  (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.t i k)
Tactic: rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]
-- 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)
y : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
h : pullback.fst (D.f k i) (D.f k j) = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
h₁ :
  Eq (α := pullback (D.f k i) (D.f k j) ⟶ D.V (k, i)) (pullback.fst (D.f k i) (D.f k j))
    (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.t i k)
⊢ inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) = pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
have h₂ : Eq (α := pullback (D.f k i) (D.f k j) ⟶ D.V (k, i)) (pullback.fst (D.f k i) (D.f k j))
  (pullback.fst (D.f k i) (D.f k j) ≫ 𝟙 (D.V (k, i)))
Tactic: rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]
-- 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)
y : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
h : pullback.fst (D.f k i) (D.f k j) = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
h₁ :
  Eq (α := pullback (D.f k i) (D.f k j) ⟶ D.V (k, i)) (pullback.fst (D.f k i) (D.f k j))
    (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.t i k)
h₂ :
  Eq (α := pullback (D.f k i) (D.f k j) ⟶ D.V (k, i)) (pullback.fst (D.f k i) (D.f k j))
    (pullback.fst (D.f k i) (D.f k j) ≫ 𝟙 (D.V (k, i)))
⊢ inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) = pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
have h₃ : Eq (α := pullback (D.f k i) (D.f k j) ⟶ D.V (k, i)) (pullback.fst (D.f k i) (D.f k j))
  (pullback.fst (D.f k i) (D.f k j))
Tactic: rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]
-- 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)
⊢ 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.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))))) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯)
have e : 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: have e := (D.snd_invApp_t_app' i j k U).choose_spec
-- 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)
e :
  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)))))
⊢ 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.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))))) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯)
have e₁ : ∀ {Z : C}
  (h :
    (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))) ((Opens.map (D.t' k i j).base).1 U))) ⟶
      Z),
  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) ≫ h =
    (D.t' k i j).c.app (op U) ≫ invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U) ≫ h
Tactic: replace e := reassoc_of% e
Cleared hypotheses: e
-- 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)
e :
  ∀ {Z : C}
    (h :
      (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))) ((Opens.map (D.t' k i j).base).1 U))) ⟶
        Z),
    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 ⋯) ≫ h =
      (D.t' k i j).c.app (op U) ≫ invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U) ≫ h
⊢ 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.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))))) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯)
have rw : 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)) =
  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.V (k, i)).presheaf.map (eqToHom sorry)
Tactic: rw [← e]
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
      (Opens.map (Hom.base (D.ι j)) : Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U j) : TopCat) : Type v))
      (Functor.obj
          (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
            Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
          U :
        Opens (↑(↑D.glued : TopCat) : Type v)) =
    (opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))
have h : (↑(Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
        (Opens.map (Hom.base (D.ι j)) : Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U j) : TopCat) : Type v))
        (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
            U :
          Opens (↑(↑D.glued : TopCat) : Type v))) :
    Set (↑(↑(D.U j) : TopCat) : Type v)) =
  (↑((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))) :
    Set (↑(↑(D.U j) : TopCat) : Type v))
Tactic: ext1
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ (↑(Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
          (Opens.map (Hom.base (D.ι j)) : Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U j) : TopCat) : Type v))
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v))) :
      Set (↑(↑(D.U j) : TopCat) : Type v)) =
    (↑((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))) :
      Set (↑(↑(D.U j) : TopCat) : Type v))
have h : Eq (α := Set (↑(↑(D.U j) : TopCat) : Type v))
  (Set.preimage (β := (↑(↑D.glued : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑D.glued : TopCat)) (Hom.base (D.ι j))) :
      (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (↑D.glued : TopCat)) (Hom.base (D.ι i))) :
        (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v)) ''
      (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
  (Set.image (α := (↑(↑(D.V (j, i)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.f j i).base) :
      (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t j i).base) :
        (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
        (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))))
Tactic: dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj]
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α := Set (↑(↑(D.U j) : TopCat) : Type v))
    (Set.image (α := (↑(↑(D.V (j, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.f j i).base) : (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
      (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (D.t i j).base) :
          (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (j, 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)) ⁻¹'
          (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))))
    (Set.image (α := (↑(↑(D.V (j, i)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f j i).base) :
        (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
      (Set.preimage (β := (↑(↑(D.V (i, j)) : TopCat) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t j i).base) :
          (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
          (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))))
have h : Eq (α := Set (↑(↑(D.V (j, i)) : TopCat) : Type v))
  (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (D.t i j).base) :
      (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (j, 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)) ⁻¹'
      (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
  (Set.preimage (β := (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t j i).base) :
      (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
      (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
Tactic: refine congr_arg (_ '' ·) ?_
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α := Set (↑(↑(D.V (j, i)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t i j).base) :
        (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (j, 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)) ⁻¹'
        (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
    (Set.preimage (β := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t j i).base) :
        (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
        (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
have h : Eq (α := Set (↑(↑(D.V (i, j)) : TopCat) : Type v))
  (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (j, i)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t j i).base) :
        (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t i j).base) :
        (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (j, 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)) ⁻¹'
      (↑U : Set (↑(↑(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)) ⁻¹'
    (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))
Tactic: rw [Set.eq_preimage_iff_image_eq, ← Set.image_comp]
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
h :
  Eq (α := Set (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(D.V (j, i)) : TopCat) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t j i).base) :
          (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (D.t i j).base) :
          (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (j, 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)) ⁻¹'
        (↑U : Set (↑(↑(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)) ⁻¹'
      (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))
⊢ Eq (α := Set (↑(↑(D.V (j, i)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t i j).base) :
        (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (j, 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)) ⁻¹'
        (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
    (Set.preimage (β := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t j i).base) :
        (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
        (↑U : Set (↑(↑(D.U i) : TopCat) : Type v))))
have h₁ : Function.Bijective (α := (↑(↑(D.V (j, i)) : TopCat) : Type v)) (β := (↑(↑(D.V (i, j)) : TopCat) : Type v))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        (D.t j i).base) :
    (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : TopCat) : Type v))
Tactic: rw [Set.eq_preimage_iff_image_eq, ← Set.image_comp]
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α := Set (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(D.V (j, i)) : TopCat) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t j i).base) :
          (a : (↑(↑(D.V (j, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (D.t i j).base) :
          (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (j, 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)) ⁻¹'
        (↑U : Set (↑(↑(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)) ⁻¹'
      (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))
have h : Eq (α := Set (↑(↑(D.V (i, j)) : TopCat) : Type v))
  (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t i j ≫ D.t j i).base) :
      (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
      (↑U : Set (↑(↑(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)) ⁻¹'
    (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))
Tactic: change (D.t i j ≫ D.t j i).base '' _ = _
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α := Set (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t i j ≫ D.t j i).base) :
        (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
        (↑U : Set (↑(↑(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)) ⁻¹'
      (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))
have h : Eq (α := Set (↑(↑(D.V (i, j)) : TopCat) : Type v))
  (Set.image (α := (↑(↑(D.V (i, j)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Hom.base (𝟙 (D.V (i, j))))) :
      (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : 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)) ⁻¹'
      (↑U : Set (↑(↑(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)) ⁻¹'
    (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)))
Tactic: rw [𝖣.t_inv]