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
x : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
refine_2 :
  ∀ (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))
⊢ NatTrans.app
      ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf)
      x =
    s.fst.c.app x

Tactic:
induction x with | op x => ?_

Premises used: Opposite.op
-- 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)
refine_2 :
  Eq (α := X.presheaf.obj (op x) ⟶ ((Opens.map s.fst.base).op ⋙ s.pt.presheaf).obj (op x))
    (CategoryStruct.comp (Y :=
      (Functor.obj (TopCat.Presheaf.pushforward C (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base)
            s.pt.presheaf).obj
        (op x))
      (CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj (unop (op x))))) (invApp f (unop (op x)))
            (g.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop (op x)))) ≫
              Y.presheaf.map (eqToHom ⋯)) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯) :
        X.presheaf.obj (op x) ⟶
          (Functor.obj
                (TopCat.Presheaf.pushforward C (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base)
                s.pt.presheaf).obj
            (op x))
      (NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) (op x) :
        (Functor.obj (TopCat.Presheaf.pushforward C (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base)
                s.pt.presheaf).obj
            (op x) ⟶
          ((Opens.map s.fst.base).op ⋙ s.pt.presheaf).obj (op x)))
    (s.fst.c.app (op x))
⊢ 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:
change ((_ ≫ _) ≫ _ ≫ _) ≫ _ = _

Premises used: CategoryTheory.CategoryStruct.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
x : Opens (↑(↑X : TopCat) : Type u_1)
refine_2 :
  CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj x))) (invApp f x)
      (g.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) x)) ≫
        CategoryStruct.comp (Y :=
          (Functor.obj (TopCat.Presheaf.pushforward C (pullbackConeOfLeft f g).fst.base)
                (pullbackConeOfLeft f g).pt.presheaf).obj
            (op x))
          (Y.presheaf.map (eqToHom ⋯) :
            Y.presheaf.obj ((Opens.map g.base).op.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) x))) ⟶
              Y.presheaf.obj
                (⋯.functor.op.obj (Functor.obj (Functor.op (Opens.map (pullback.fst f.base g.base))) (op x))))
          (s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
              s.pt.presheaf.map (eqToHom ⋯) ≫ NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) (op x) :
            (Functor.obj (TopCat.Presheaf.pushforward C (pullbackConeOfLeft f g).fst.base)
                    (pullbackConeOfLeft f g).pt.presheaf).obj
                (op x) ⟶
              ((Opens.map s.fst.base).op ⋙ s.pt.presheaf).obj (op x))) =
    s.fst.c.app (op x)
⊢ Eq (α := X.presheaf.obj (op x) ⟶ ((Opens.map s.fst.base).op ⋙ s.pt.presheaf).obj (op x))
    (CategoryStruct.comp (Y :=
      (Functor.obj (TopCat.Presheaf.pushforward C (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base)
            s.pt.presheaf).obj
        (op x))
      (CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj (unop (op x))))) (invApp f (unop (op x)))
            (g.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop (op x)))) ≫
              Y.presheaf.map (eqToHom ⋯)) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯) :
        X.presheaf.obj (op x) ⟶
          (Functor.obj
                (TopCat.Presheaf.pushforward C (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base)
                s.pt.presheaf).obj
            (op x))
      (NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) (op x) :
        (Functor.obj (TopCat.Presheaf.pushforward C (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base)
                s.pt.presheaf).obj
            (op x) ⟶
          ((Opens.map s.fst.base).op ⋙ s.pt.presheaf).obj (op x)))
    (s.fst.c.app (op x))

Tactic:
simp_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
x : Opens (↑(↑X : TopCat) : Type u_1)
refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj x))) (invApp f x)
      (g.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) x)) ≫
        CategoryStruct.comp (Y :=
          (Functor.obj (TopCat.Presheaf.pushforward C (pullbackConeOfLeft f g).fst.base)
                (pullbackConeOfLeft f g).pt.presheaf).obj
            (op x))
          (Y.presheaf.map (eqToHom ⋯) :
            Y.presheaf.obj ((Opens.map g.base).op.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) x))) ⟶
              Y.presheaf.obj
                (⋯.functor.op.obj (Functor.obj (Functor.op (Opens.map (pullback.fst f.base g.base))) (op x))))
          (s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
              s.pt.presheaf.map (eqToHom ⋯) ≫ NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) (op x) :
            (Functor.obj (TopCat.Presheaf.pushforward C (pullbackConeOfLeft f g).fst.base)
                    (pullbackConeOfLeft f g).pt.presheaf).obj
                (op x) ⟶
              ((Opens.map s.fst.base).op ⋙ s.pt.presheaf).obj (op x))) =
    s.fst.c.app (op x)

Tactic:
erw [← 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
x : Opens (↑(↑X : TopCat) : Type u_1)
refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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
x : Opens (↑(↑X : TopCat) : Type u_1)
⊢ Eq (α :=
    Z.presheaf.obj (op ((opensFunctor f).obj x)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (s.fst ≫ f).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)))
    ((s.fst ≫ f).c.app (op ((opensFunctor f).obj x)))
    ((s.snd ≫ g).c.app (op ((opensFunctor f).obj x)) ≫ s.pt.presheaf.map (eqToHom ⋯))

Tactic:
have := congr_app s.condition (op (opensFunctor f |>.obj x))
-- 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)
this :
  Eq (α :=
    Z.presheaf.obj (op ((opensFunctor f).obj x)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (s.fst ≫ f).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)))
    (f.c.app (op ((opensFunctor f).obj x)) ≫ s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))))
    ((g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x)))) ≫
      s.pt.presheaf.map (eqToHom ⋯))
⊢ Eq (α :=
    Z.presheaf.obj (op ((opensFunctor f).obj x)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (s.snd ≫ g).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)))
    ((f.c.app (op ((opensFunctor f).obj x)) ≫ s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x)))) ≫
      inv (s.pt.presheaf.map (eqToHom ⋯)))
    (g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))))

Tactic:
rw [← IsIso.comp_inv_eq] at this

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- 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)
this :
  Eq (α :=
    Z.presheaf.obj (op ((opensFunctor f).obj x)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (s.snd ≫ g).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)))
    ((f.c.app (op ((opensFunctor f).obj x)) ≫ s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x)))) ≫
      inv (s.pt.presheaf.map (eqToHom ⋯)))
    (g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))))
⊢ ∀ {Z_1 : C}
    (h :
      (Functor.obj (TopCat.Presheaf.pushforward C (s.snd ≫ g).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶
        Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h

Tactic:
replace this := reassoc_of% 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
x : Opens (↑(↑X : TopCat) : Type u_1)
this :
  ∀ {Z_1 : C}
    (h :
      (Functor.obj (TopCat.Presheaf.pushforward C (s.snd ≫ g).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶
        Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
erw [← this, hf.invApp_app_assoc, s.fst.c.naturality_assoc]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, CategoryTheory.Limits.PullbackCone.fst, AlgebraicGeometry.PresheafedSpace.Hom.c, 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
x : Opens (↑(↑X : TopCat) : Type u_1)
this :
  ∀ {Z_1 : C}
    (h :
      (Functor.obj (TopCat.Presheaf.pushforward C (s.snd ≫ g).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶
        Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [eqToHom_map]

Premises used: CategoryTheory.eqToHom_map
-- 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).snd = s.snd

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).snd).base = s.snd.base
refine_2 :
  ∀ (x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ),
    NatTrans.app
        ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫
          Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf)
        x =
      s.snd.c.app x
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd

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.snd f.base g.base) =
    s.snd.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 (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
refine_2 :
  ((pullbackConeOfLeft f g).snd.c.app x ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
          s.pt.presheaf.map (eqToHom ⋯)) ≫
      NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x
⊢ NatTrans.app
      ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf)
      x =
    s.snd.c.app x

Tactic:
change (_ ≫ _ ≫ _) ≫ _ = _

Premises used: CategoryTheory.CategoryStruct.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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
refine_2 :
  (pullbackConeOfLeft f g).snd.c.app x ≫
      s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x
⊢ ((pullbackConeOfLeft f g).snd.c.app x ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
          s.pt.presheaf.map (eqToHom ⋯)) ≫
      NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x

Tactic:
simp_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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
refine_2 :
  s.snd.c.app x ≫
      (Functor.obj (TopCat.Presheaf.pushforward C s.snd.base) s.pt.presheaf).map
          (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x
⊢ (pullbackConeOfLeft f g).snd.c.app x ≫
      s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x

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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
refine_2 :
  s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
          eqToHom ⋯ ≫ NatTrans.app (eqToHom ⋯) x) =
    s.snd.c.app x
⊢ s.snd.c.app x ≫
      (Functor.obj (TopCat.Presheaf.pushforward C s.snd.base) s.pt.presheaf).map
          (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x

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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
trans :
  s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
          eqToHom ⋯ ≫ NatTrans.app (eqToHom ⋯) x) =
    s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x))
trans₁ : s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x)) = s.snd.c.app x
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
          eqToHom ⋯ ≫ NatTrans.app (eqToHom ⋯) x) =
    s.snd.c.app x

Tactic:
trans s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.Cone.pt, CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.Limits.PullbackCone.snd, CategoryTheory.NatTrans.app
-- 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 (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
          eqToHom ⋯ ≫ NatTrans.app (eqToHom ⋯) x) =
    s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x))

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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x)) = s.snd.c.app x

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
⊢ IsOpenImmersion (Y.ofRestrict ⋯)

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
create :
  (s : PullbackCone f g) →
    { l : s.pt ⟶ (pullbackConeOfLeft f g).pt //
      l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
        l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
            m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }
⊢ IsLimit (pullbackConeOfLeft f g)

Tactic:
apply PullbackCone.isLimitAux'

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux'
-- 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
property :
  pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
    pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
        m ≫ (pullbackConeOfLeft f g).fst = s.fst →
          m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
⊢ { l : s.pt ⟶ (pullbackConeOfLeft f g).pt //
    l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
      l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
          m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }

Tactic:
use pullbackConeOfLeftLift f g s

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift
-- 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
right :
  pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
    ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
      m ≫ (pullbackConeOfLeft f g).fst = s.fst →
        m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
    pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
        m ≫ (pullbackConeOfLeft f g).fst = s.fst →
          m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s

Tactic:
use pullbackConeOfLeftLift_fst f g s

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst
-- 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
right :
  ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
    m ≫ (pullbackConeOfLeft f g).fst = s.fst →
      m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
    ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
      m ≫ (pullbackConeOfLeft f g).fst = s.fst →
        m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s

Tactic:
use pullbackConeOfLeftLift_snd f g s

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_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
right :
  m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
⊢ m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s

Tactic:
_