awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
e_unop :
  Eq (α := Set (↑(↑s.pt : TopCat) : Type u_1))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) s.snd.base) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
      (↑(⋯.functor.obj (unop U)) : Set (↑(↑Y : TopCat) : Type u_1)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (Y := (↑(pullbackConeOfLeft f g).pt : TopCat)) (pullback.lift s.fst.base s.snd.base ⋯)) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)) ⁻¹'
      (↑(unop U) : Set (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)))
⊢ op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) s.snd.base) :
              (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
            (↑(⋯.functor.obj (unop U)) : Set (↑(↑Y : TopCat) : Type u_1)),
        is_open' := ⋯ : Opens (↑(↑s.pt : TopCat) : Type u_1) } =
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) (Y := (↑(pullbackConeOfLeft f g).pt : TopCat))
                  (pullback.lift s.fst.base s.snd.base ⋯)) :
              (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)) ⁻¹'
            (↑(unop U) : Set (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)),
        is_open' := ⋯ }

Tactic:
congr 2
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
⊢ CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
      (limit.π (cospan f.base g.base) WalkingCospan.right) =
    s.snd.base

Tactic:
have : _ = s.snd.base := limit.lift_π s' WalkingCospan.right
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this :
  CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
      (limit.π (cospan f.base g.base) WalkingCospan.right) =
    s.snd.base
rw :
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
            (limit.π (cospan f.base g.base) WalkingCospan.right))) :
      (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
    (↑(⋯.functor.obj (unop U)) : Set (↑(↑Y : TopCat) : Type u_1))
| (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          s.snd.base) :
      (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
    (↑(⋯.functor.obj (unop U)) : Set (↑(↑Y : TopCat) : Type u_1))

Tactic:
rw [← this]
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this :
  CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
      (limit.π (cospan f.base g.base) WalkingCospan.right) =
    s.snd.base
dsimp :
  Set.preimage (β := (↑(↑Y : TopCat) : Type u_1))
    (Function.comp (β := (↑(limit (cospan f.base g.base)) : Type u_1))
      (⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) :
        (a : (↑(limit (cospan f.base g.base)) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
      (⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯)) :
            C((↑(↑s.pt : TopCat) : Type u_1), (↑(limit (cospan f.base g.base)) : Type u_1))) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(limit (cospan f.base g.base)) : Type u_1)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
      (↑(unop U) : Set (↑(pullback f.base g.base) : Type u_1)))
| (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
            (limit.π (cospan f.base g.base) WalkingCospan.right))) :
      (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
    (↑(⋯.functor.obj (unop U)) : Set (↑(↑Y : TopCat) : Type u_1))

Tactic:
dsimp [s']
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this :
  CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
      (limit.π (cospan f.base g.base) WalkingCospan.right) =
    s.snd.base
rw :
  Set.preimage (β := (↑(limit (cospan f.base g.base)) : Type u_1))
    (⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯)) :
          C((↑(↑s.pt : TopCat) : Type u_1), (↑(limit (cospan f.base g.base)) : Type u_1))) :
      (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(limit (cospan f.base g.base)) : Type u_1))
    (Set.preimage (β := (↑(↑Y : TopCat) : Type u_1))
      (⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) :
        (a : (↑(limit (cospan f.base g.base)) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
          (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
        (↑(unop U) : Set (↑(pullback f.base g.base) : Type u_1))))
| Set.preimage (β := (↑(↑Y : TopCat) : Type u_1))
    (Function.comp (β := (↑(limit (cospan f.base g.base)) : Type u_1))
      (⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) :
        (a : (↑(limit (cospan f.base g.base)) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
      (⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯)) :
            C((↑(↑s.pt : TopCat) : Type u_1), (↑(limit (cospan f.base g.base)) : Type u_1))) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(limit (cospan f.base g.base)) : Type u_1)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
      (↑(unop U) : Set (↑(pullback f.base g.base) : Type u_1)))

Tactic:
rw [Function.comp_def, ← Set.preimage_preimage]

Premises used: Set.preimage_preimage, Function.comp_def
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this :
  CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
      (limit.π (cospan f.base g.base) WalkingCospan.right) =
    s.snd.base
rw :
  Set.preimage (β := (↑(limit (cospan f.base g.base)) : Type u_1))
    (⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯)) :
          C((↑(↑s.pt : TopCat) : Type u_1), (↑(limit (cospan f.base g.base)) : Type u_1))) :
      (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(limit (cospan f.base g.base)) : Type u_1))
    (Set.preimage (β := (↑(↑Y : TopCat) : Type u_1))
      (⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) :
        (a : (↑(limit (cospan f.base g.base)) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
          (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
        (↑(unop U) : Set (↑(pullback f.base g.base) : Type u_1))))
| (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          s.snd.base) :
      (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
    (↑(⋯.functor.obj (unop U)) : Set (↑(↑Y : TopCat) : Type u_1))

Tactic:
rw [← this]
                  dsimp [s']
                  rw [Function.comp_def, ← Set.preimage_preimage]

Premises used: Set.preimage_preimage, Function.comp_def
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this :
  CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
      (limit.π (cospan f.base g.base) WalkingCospan.right) =
    s.snd.base
e_unop :
  Eq (α := Set (↑(↑s.pt : TopCat) : Type u_1))
    (Set.preimage (β := (↑(limit (cospan f.base g.base)) : Type u_1))
      (⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯)) :
            C((↑(↑s.pt : TopCat) : Type u_1), (↑(limit (cospan f.base g.base)) : Type u_1))) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(limit (cospan f.base g.base)) : Type u_1))
      (Set.preimage (β := (↑(↑Y : TopCat) : Type u_1))
        (⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) :
          (a : (↑(limit (cospan f.base g.base)) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
            (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
          (↑(unop U) : Set (↑(pullback f.base g.base) : Type u_1)))))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (Y := (↑(pullbackConeOfLeft f g).pt : TopCat)) (pullback.lift s.fst.base s.snd.base ⋯)) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)) ⁻¹'
      (↑(unop U) : Set (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)))
⊢ Eq (α := Set (↑(↑s.pt : TopCat) : Type u_1))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) s.snd.base) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
      (↑(⋯.functor.obj (unop U)) : Set (↑(↑Y : TopCat) : Type u_1)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (Y := (↑(pullbackConeOfLeft f g).pt : TopCat)) (pullback.lift s.fst.base s.snd.base ⋯)) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)) ⁻¹'
      (↑(unop U) : Set (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)))

Tactic:
conv_lhs =>
                  rw [← this]
                  dsimp [s']
                  rw [Function.comp_def, ← Set.preimage_preimage]

Premises used: Set.preimage_preimage, Function.comp_def
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this :
  CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
      (limit.π (cospan f.base g.base) WalkingCospan.right) =
    s.snd.base
e_unop :
  Eq (α := Set (↑(↑s.pt : TopCat) : Type u_1))
    ((⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯)) :
            C((↑(↑s.pt : TopCat) : Type u_1), (↑(limit (cospan f.base g.base)) : Type u_1))) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(limit (cospan f.base g.base)) : Type u_1)) ⁻¹'
      (↑(unop U) : Set (↑(pullback f.base g.base) : Type u_1)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (Y := (↑(pullbackConeOfLeft f g).pt : TopCat)) (pullback.lift s.fst.base s.snd.base ⋯)) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)) ⁻¹'
      (↑(unop U) : Set (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)))
⊢ Eq (α := Set (↑(↑s.pt : TopCat) : Type u_1))
    (Set.preimage (β := (↑(limit (cospan f.base g.base)) : Type u_1))
      (⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯)) :
            C((↑(↑s.pt : TopCat) : Type u_1), (↑(limit (cospan f.base g.base)) : Type u_1))) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(limit (cospan f.base g.base)) : Type u_1))
      (Set.preimage (β := (↑(↑Y : TopCat) : Type u_1))
        (⇑(TopCat.Hom.hom (limit.π (cospan f.base g.base) WalkingCospan.right)) :
          (a : (↑(limit (cospan f.base g.base)) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
            (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
          (↑(unop U) : Set (↑(pullback f.base g.base) : Type u_1)))))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (Y := (↑(pullbackConeOfLeft f g).pt : TopCat)) (pullback.lift s.fst.base s.snd.base ⋯)) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)) ⁻¹'
      (↑(unop U) : Set (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)))

Tactic:
rw [Set.preimage_image_eq _
                    (TopCat.snd_isOpenEmbedding_of_left hf.base_open g.base).injective]

Premises used: TopCat.snd_isOpenEmbedding_of_left, Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.preimage_image_eq, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this :
  CategoryStruct.comp (Y := limit (cospan f.base g.base)) (limit.lift (cospan f.base g.base) s')
      (limit.π (cospan f.base g.base) WalkingCospan.right) =
    s.snd.base
⊢ Eq (α := Set (↑(↑s.pt : TopCat) : Type u_1))
    ((⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯)) :
            C((↑(↑s.pt : TopCat) : Type u_1), (↑(limit (cospan f.base g.base)) : Type u_1))) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(limit (cospan f.base g.base)) : Type u_1)) ⁻¹'
      (↑(unop U) : Set (↑(pullback f.base g.base) : Type u_1)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (Y := (↑(pullbackConeOfLeft f g).pt : TopCat)) (pullback.lift s.fst.base s.snd.base ⋯)) :
        (a : (↑(↑s.pt : TopCat) : Type u_1)) → (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)) ⁻¹'
      (↑(unop U) : Set (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1)))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
erw :
  s.snd.c.app (⋯.functor.op.obj U) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C s.snd.base) s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      CategoryTheory.Functor.map
        (Functor.obj (TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)) s.pt.presheaf) i
⊢ (pullbackConeOfLeft f g).pt.presheaf.map i ≫ s.snd.c.app (⋯.functor.op.obj V) ≫ s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      CategoryTheory.Functor.map
        (Functor.obj (TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)) s.pt.presheaf) i

Tactic:
erw [s.snd.c.naturality_assoc]

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.Limits.PullbackCone.snd, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
rw :
  s.snd.c.app (⋯.functor.op.obj U) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C s.snd.base) s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯) ≫
        CategoryTheory.Functor.map
          (Functor.obj (TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)) s.pt.presheaf) i
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C s.snd.base) s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      CategoryTheory.Functor.map
        (Functor.obj (TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)) s.pt.presheaf) i

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
erw :
  s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map ((Opens.map s.snd.base).op.map (⋯.functor.op.map i) ≫ eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map
        (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.op (Opens.map (pullback.lift s.fst.base s.snd.base ⋯))) i)
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C s.snd.base) s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯) ≫
        CategoryTheory.Functor.map
          (Functor.obj (TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)) s.pt.presheaf) i

Tactic:
erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]

Premises used: CategoryTheory.Limits.Cone.pt, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens (↑(↑(pullbackConeOfLeft f g).pt : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map ((Opens.map s.snd.base).op.map (⋯.functor.op.map i) ≫ eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map
        (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.op (Opens.map (pullback.lift s.fst.base s.snd.base ⋯))) i)

Tactic:
congr 1
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst

Tactic:
PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun x => ?_

Premises used: CategoryTheory.NatTrans.ext, funext, AlgebraicGeometry.PresheafedSpace.Hom.ext
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
refine_1 : (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base = s.fst.base
refine_2 :
  ∀ (x : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ),
    NatTrans.app
        ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫
          Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf)
        x =
      s.fst.c.app x
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst

Tactic:
refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun x => ?_

Premises used: CategoryTheory.NatTrans.ext, funext, AlgebraicGeometry.PresheafedSpace.Hom.ext
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ CategoryStruct.comp (Y := pullback f.base g.base) (pullback.lift s.fst.base s.snd.base ⋯)
      (pullback.fst f.base g.base) =
    s.fst.base

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens (↑(↑X : TopCat) : Type u_1)
⊢ Eq (α := X.presheaf.obj (op x) ⟶ ((Opens.map s.fst.base).op ⋙ s.pt.presheaf).obj (op x))
    (NatTrans.app
      ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf)
      (op x))
    (s.fst.c.app (op x))

Tactic:
?_