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
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ IsIso (X := limit (D.diagramOverOpen U)) (D.diagramOverOpenπ U i)
have h : D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U)) ∧
  Eq (α :=
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
Tactic: use D.ιInvAppπEqMap U ≫ D.ιInvApp U
-- 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 : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U)) ∧
    Eq (α :=
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
      ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
          (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
      (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
          (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
have h : D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))
Tactic: constructor
-- 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 : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
h : D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U)) ∧
    Eq (α :=
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
      ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
          (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
      (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
          (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
have h₁ : Eq (α :=
  (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
  ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
  (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
Tactic: constructor
-- 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 : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α :=
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
have h : Eq (α :=
  (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
  (D.ιInvAppπEqMap U ≫ (D.U i).presheaf.map (eqToHom sorry) :
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
  (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
Tactic: rw [Category.assoc, (D.ιInvApp_π _).choose_spec]
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j) //
    l ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst ∧
      l ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)},
          m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst →
            m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = l }
have refine_1 : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_1 : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j) //
    l ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst ∧
      l ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)},
          m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst →
            m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = l }
have refine_2 : lift (D.f i j) s.fst sorry ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_1 : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
refine_2 : lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j) //
    l ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst ∧
      l ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)},
          m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst →
            m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = l }
have refine_3 : lift (D.f i j) s.fst sorry ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_1 : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
refine_2 : lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst
refine_3 : lift (D.f i j) s.fst ⋯ ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j) //
    l ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst ∧
      l ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)},
          m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst →
            m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = l }
have refine_4 : ∀ {m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)},
  m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst →
    m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = lift (D.f i j) s.fst sorry
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
have refine_1 : Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
  (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          s.fst.base) :
      (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
  (Set.range (ι := (↑(↑(Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone 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.vPullbackCone i j).pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
Tactic: refine PresheafedSpace.IsOpenImmersion.lift (D.f i j) s.fst ?_
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.range (ι :=
      (↑(↑(Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone 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.vPullbackCone i j).pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
have refine_1 : Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
  (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          s.fst.base) :
      (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
  (Set.preimage (β := (↑D.toTopGlueData.glued : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι i)) :
      (a : (↑(D.toTopGlueData.U i) : Type v)) → (↑D.toTopGlueData.glued : Type v))
    (Set.range (ι := (↑(D.toTopGlueData.U j) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι j)) :
        (a : (↑(D.toTopGlueData.U j) : Type v)) → (↑D.toTopGlueData.glued : Type v))))
Tactic: erw [← D.toTopGlueData.preimage_range j i]
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)
have rw : Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
  (s.fst.base ≫
      CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι i))
        (Iso.hom (D.gluedIso (forget C))) :
    (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
  (s.snd.base ≫
      CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι j))
        (Iso.hom (D.gluedIso (forget C))) :
    (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
Tactic: rw [← 𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _, ←
          𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _]
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.fst.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι i))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.snd.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι j))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
have this : Eq (α := (↑s.pt : TopCat) ⟶ (↑D.glued : TopCat)) (Hom.base (s.fst ≫ D.ι i)) (Hom.base (s.snd ≫ D.ι j))
Tactic: have := congr_arg PresheafedSpace.Hom.base s.condition
-- 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
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this : Eq (α := (↑s.pt : TopCat) ⟶ (↑D.glued : TopCat)) (Hom.base (s.fst ≫ D.ι i)) (Hom.base (s.snd ≫ D.ι j))
⊢ Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.fst.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι i))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.snd.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι j))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
have this₁ : Eq (α := (↑s.pt : TopCat) ⟶ (↑D.glued : TopCat)) (s.fst.base ≫ Hom.base (D.ι i)) (s.snd.base ≫ Hom.base (D.ι j))
Tactic: rw [comp_base, comp_base] 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
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this : Eq (α := (↑s.pt : TopCat) ⟶ (↑D.glued : TopCat)) (s.fst.base ≫ Hom.base (D.ι i)) (s.snd.base ≫ Hom.base (D.ι j))
⊢ Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.fst.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι i))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.snd.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι j))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
have this₁ : ∀ {Z : TopCat.{v}} (h : (↑D.glued : TopCat) ⟶ Z), s.fst.base ≫ Hom.base (D.ι i) ≫ h = s.snd.base ≫ Hom.base (D.ι j) ≫ h
Tactic: replace this := reassoc_of% 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
inst_1 : HasLimits.{v, u} C
i j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.preimage (β := (↑D.toTopGlueData.glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι i)) :
        (a : (↑(D.toTopGlueData.U i) : Type v)) → (↑D.toTopGlueData.glued : Type v))
      (Set.range (ι := (↑(D.toTopGlueData.U j) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι j)) :
          (a : (↑(D.toTopGlueData.U j) : Type v)) → (↑D.toTopGlueData.glued : Type v))))
have this : Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i) (s.snd.base ≫ D.toTopGlueData.ι j)
Tactic: have :
        s.fst.base ≫ D.toTopGlueData.ι i =
          s.snd.base ≫ D.toTopGlueData.ι j := by
        rw [← 𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _, ←
          𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _]
        have := congr_arg PresheafedSpace.Hom.base s.condition
        rw [comp_base, comp_base] at this
        replace this := reassoc_of% this
        exact this _
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this :
  Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)
⊢ Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.preimage (β := (↑D.toTopGlueData.glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι i)) :
        (a : (↑(D.toTopGlueData.U i) : Type v)) → (↑D.toTopGlueData.glued : Type v))
      (Set.range (ι := (↑(D.toTopGlueData.U j) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι j)) :
          (a : (↑(D.toTopGlueData.U j) : Type v)) → (↑D.toTopGlueData.glued : Type v))))
have refine_1 : Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
  (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          s.fst.base) :
      (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
  (Set.preimage (β := (↑(D.mapGlueData (forget C)).glued : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι i)) :
      (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))
    (Set.range (ι := (↑(↑(D.U j) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι j)) :
        (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))))
Tactic: simp only [mapGlueData_U, forget_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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this :
  Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)
⊢ Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.preimage (β := (↑(D.mapGlueData (forget C)).glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι i)) :
        (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))
      (Set.range (ι := (↑(↑(D.U j) : TopCat) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι j)) :
          (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))))
have refine_1 : Subset (α := Set (↑(D.mapGlueData (forget C)).glued : Type v))
  (Set.image (α := (↑(↑(D.U j) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (D.mapGlueData (forget C)).glued) (D.toTopGlueData.ι j)) :
      (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))
    (Set.image (α := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.snd.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
      Set.univ))
  (Set.range (ι := (↑(↑(D.U j) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι j)) :
      (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))
Tactic: rw [← Set.image_subset_iff, ← Set.image_univ, ← Set.image_comp, Set.image_univ,
        ← TopCat.coe_comp, this, TopCat.coe_comp, ← Set.image_univ, 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ lift (D.f i j) s.fst ⋯ ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd
have refine_3 : Eq (α := s.pt ⟶ D.glued) (lift (D.f i j) s.fst sorry ≫ PullbackCone.fst (D.vPullbackCone i j) ≫ D.ι i) (s.snd ≫ D.ι j)
Tactic: rw [← cancel_mono (𝖣.ι j), Category.assoc, ← (𝖣.vPullbackCone i j).condition]
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
| s.snd ≫ D.ι j
have rw : s.fst ≫ D.ι i
Tactic: rw [← s.condition]
-- 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
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ Eq (α := s.pt ⟶ D.glued) (lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) ≫ D.ι i) (s.snd ≫ D.ι j)
have refine_3 : Eq (α := s.pt ⟶ D.glued) (lift (D.f i j) s.fst sorry ≫ PullbackCone.fst (D.vPullbackCone i j) ≫ D.ι i) (s.fst ≫ D.ι i)
Tactic: conv_rhs => rw [← s.condition]