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_1 s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
h : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
right : m ≫ (pullbackConeOfLeft f g).snd = pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd
⊢ m = pullbackConeOfLeftLift f g s

Tactic:
rw [← cancel_mono (pullbackConeOfLeft f g).snd]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft, CategoryTheory.Limits.PullbackCone.snd
-- 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_1 s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
h : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m ≫ (pullbackConeOfLeft f g).snd = pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd

Tactic:
h₂.trans (pullbackConeOfLeftLift_snd f g s).symm

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, Eq.symm, Eq.trans
-- 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_1 s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
h : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m ≫ (pullbackConeOfLeft f g).snd = pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd

Tactic:
exact h₂.trans (pullbackConeOfLeftLift_snd f g s).symm

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, Eq.symm, Eq.trans
-- 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
⊢ HasPullback f g

Tactic:
⟨⟨⟨_, pullbackConeOfLeftIsLimit f g⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit, CategoryTheory.Limits.LimitCone.mk
-- 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
⊢ HasPullback g f

Tactic:
hasPullback_symmetry f g

Premises used: CategoryTheory.Limits.hasPullback_symmetry
-- 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
rw :
  IsOpenImmersion (X := pullback f g)
    (Iso.hom (limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }) ≫
      { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) }.cone.π.app
        WalkingCospan.right)
⊢ IsOpenImmersion (X := pullback f g) (limit.π (cospan f g) WalkingCospan.right)

Tactic:
rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]

Premises used: CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.limit.isoLimitCone_hom_π, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit, CategoryTheory.Limits.LimitCone.mk
-- 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
⊢ IsOpenImmersion (X := pullback f g)
    (Iso.hom (limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }) ≫
      { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) }.cone.π.app
        WalkingCospan.right)

Tactic:
infer_instance
-- 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
rw : IsOpenImmersion (X := pullback g f) (Iso.hom (pullbackSymmetry g f) ≫ pullback.snd f g)
⊢ IsOpenImmersion (X := pullback g f) (pullback.fst g f)

Tactic:
rw [← pullbackSymmetry_hom_comp_snd]

Premises used: CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd
-- 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
⊢ IsOpenImmersion (X := pullback g f) (Iso.hom (pullbackSymmetry g f) ≫ pullback.snd f g)

Tactic:
infer_instance
-- 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
inst_1 : IsOpenImmersion g
rw : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.left ≫ f)
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)

Tactic:
rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]

Premises used: CategoryTheory.Limits.WalkingCospan.Hom.inl, CategoryTheory.Limits.cospan_map_inl, CategoryTheory.Limits.cospan, CategoryTheory.Limits.limit.w
-- 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
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.left ≫ f)

Tactic:
infer_instance
-- 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
apply :
  IsLimit
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      (Functor.mapCone (forget C) (pullbackConeOfLeft f g)))
⊢ IsLimit (F := cospan f g ⋙ forget C) (Functor.mapCone (forget C) (pullbackConeOfLeft f g))

Tactic:
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan _) _).toFun

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, Equiv.toFun, CategoryTheory.Limits.diagramIsoCospan
-- 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 :
  limit.cone (cospan f.base g.base) ≅
    (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      (Functor.mapCone (forget C) (pullbackConeOfLeft f g))
⊢ IsLimit
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      (Functor.mapCone (forget C) (pullbackConeOfLeft f g)))

Tactic:
refine (IsLimit.equivIsoLimit ?_).toFun (limit.isLimit (cospan f.base g.base))

Premises used: Equiv.toFun, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.IsLimit.equivIsoLimit, CategoryTheory.Limits.cospan, AlgebraicGeometry.PresheafedSpace.Hom.base
-- 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
φ :
  (limit.cone (cospan f.base g.base)).pt ≅
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
        (Functor.mapCone (forget C) (pullbackConeOfLeft f g))).pt
w :
  autoParam
    (∀ (j : WalkingCospan),
      (limit.cone (cospan f.base g.base)).π.app j =
        Iso.hom (Iso.refl (limit.cone (cospan f.base g.base)).pt) ≫
          ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
                  (Functor.mapCone (forget C) (pullbackConeOfLeft f g))).π.app
            j)
    Cone.ext._auto_1
⊢ limit.cone (cospan f.base g.base) ≅
    (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      (Functor.mapCone (forget C) (pullbackConeOfLeft f g))

Tactic:
fapply Cone.ext

Premises used: CategoryTheory.Limits.Cone.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
⊢ (limit.cone (cospan f.base g.base)).pt ≅
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
        (Functor.mapCone (forget C) (pullbackConeOfLeft f g))).pt

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- 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
w :
  ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      𝟙 (Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) j) ≫
        NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) j ≫
          (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j
⊢ autoParam
    (∀ (j : WalkingCospan),
      (limit.cone (cospan f.base g.base)).π.app j =
        Iso.hom (Iso.refl (limit.cone (cospan f.base g.base)).pt) ≫
          ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
                  (Functor.mapCone (forget C) (pullbackConeOfLeft f g))).π.app
            j)
    Cone.ext._auto_1

Tactic:
change ∀ j, _ = 𝟙 _ ≫ _ ≫ _
-- 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
w :
  Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
      (cospan f.base g.base).obj none)
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) none ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
        (cospan f.base g.base).obj none)
    ((limit.cone (cospan f.base g.base)).π.app none :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
        (cospan f.base g.base).obj none)
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
      (cospan f.base g.base).obj none)
    ((limit.cone (cospan f.base g.base)).π.app none)
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) none ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none)

Tactic:
symm
-- 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
w :
  Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.left) ⟶
      (cospan f.base g.base).obj (some WalkingPair.left))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.left) ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.left) ⟶
        (cospan f.base g.base).obj (some WalkingPair.left))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.left) ⟶
        (cospan f.base g.base).obj (some WalkingPair.left))
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.left) ⟶
      (cospan f.base g.base).obj (some WalkingPair.left))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.left) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left))

Tactic:
symm
-- 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
w :
  Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.right) ⟶
      (cospan f.base g.base).obj (some WalkingPair.right))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.right) ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.right) ⟶
        (cospan f.base g.base).obj (some WalkingPair.right))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.right) ⟶
        (cospan f.base g.base).obj (some WalkingPair.right))
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.right) ⟶
      (cospan f.base g.base).obj (some WalkingPair.right))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right))

Tactic:
symm
-- 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
w : ((pullbackConeOfLeft f g).fst.base ≫ f.base) ≫ Iso.hom (eqToIso ⋯) = pullback.fst f.base g.base ≫ f.base
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
      (cospan f.base g.base).obj none)
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) none ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
        (cospan f.base g.base).obj none)
    ((limit.cone (cospan f.base g.base)).π.app none :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
        (cospan f.base g.base).obj none)

Tactic:
simp only [limit.cone_x, Functor.const_obj_obj, cospan_one, Functor.comp_obj, forget_obj,
          Functor.mapCone_pt, Functor.mapCone_π_app, PullbackCone.condition_one, forget_map,
          comp_base, cospan_left, cospan_right, Functor.comp_map, cospan_map_inl, cospan_map_inr,
          diagramIsoCospan_hom_app, PullbackCone.fst_limit_cone]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.diagramIsoCospan_hom_app, CategoryTheory.Limits.cospan_left, CategoryTheory.Limits.cospan_map_inr, AlgebraicGeometry.PresheafedSpace.forget_obj, CategoryTheory.Limits.cospan_map_inl, AlgebraicGeometry.PresheafedSpace.forget_map, CategoryTheory.Limits.limit.cone_x, CategoryTheory.Functor.mapCone_pt, CategoryTheory.Limits.cospan_right, CategoryTheory.Functor.mapCone_π_app, AlgebraicGeometry.PresheafedSpace.comp_base, CategoryTheory.Limits.PullbackCone.condition_one, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.comp_map, CategoryTheory.Limits.cospan_one, CategoryTheory.Limits.PullbackCone.fst_limit_cone
-- 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
⊢ ((pullbackConeOfLeft f g).fst.base ≫ f.base) ≫ Iso.hom (eqToIso ⋯) = pullback.fst f.base g.base ≫ f.base

Tactic:
tauto
-- 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
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.left) ⟶
      (cospan f.base g.base).obj (some WalkingPair.left))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.left) ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.left) ⟶
        (cospan f.base g.base).obj (some WalkingPair.left))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.left) ⟶
        (cospan f.base g.base).obj (some WalkingPair.left))

Tactic:
Category.comp_id _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Category.comp_id
-- 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
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.left) ⟶
      (cospan f.base g.base).obj (some WalkingPair.left))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.left) ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.left) ⟶
        (cospan f.base g.base).obj (some WalkingPair.left))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.left) ⟶
        (cospan f.base g.base).obj (some WalkingPair.left))

Tactic:
exact Category.comp_id _

Premises used: CategoryTheory.Category.comp_id
-- 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
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.right) ⟶
      (cospan f.base g.base).obj (some WalkingPair.right))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.right) ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.right) ⟶
        (cospan f.base g.base).obj (some WalkingPair.right))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.right) ⟶
        (cospan f.base g.base).obj (some WalkingPair.right))

Tactic:
Category.comp_id _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Category.comp_id
-- 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
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.right) ⟶
      (cospan f.base g.base).obj (some WalkingPair.right))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.right) ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.right) ⟶
        (cospan f.base g.base).obj (some WalkingPair.right))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right) :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
          (some WalkingPair.right) ⟶
        (cospan f.base g.base).obj (some WalkingPair.right))

Tactic:
exact Category.comp_id _

Premises used: CategoryTheory.Category.comp_id
-- 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
⊢ PreservesLimit (cospan g f) (forget C)

Tactic:
preservesPullback_symmetry (forget C) f g

Premises used: CategoryTheory.Limits.preservesPullback_symmetry, AlgebraicGeometry.PresheafedSpace.forget
-- 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
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X : 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) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
⊢ IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)

Tactic:
haveI := TopCat.snd_iso_of_left_embedding_range_subset hf.base_open.isEmbedding g.base H
-- 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
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X : 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) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
this : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
rw :
  IsIso (X := (↑(pullback f g) : TopCat))
    (Hom.base
      (Iso.hom (limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }) ≫
        { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) }.cone.π.app
          WalkingCospan.right))
⊢ IsIso (X := (↑(pullback f g) : TopCat)) (Hom.base (limit.π (cospan f g) WalkingCospan.right))

Tactic:
rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]

Premises used: CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.limit.isoLimitCone_hom_π, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit, CategoryTheory.Limits.LimitCone.mk