-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem pullback_cone_of_left_condition : pullbackConeOfLeftFst f g ≫ f = Y.ofRestrict _ ≫ g

Proof state:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ (f.c.app (op X✝) ≫
        invApp f ((Opens.map f.base).obj X✝) ≫
          g.c.app (op (⋯.functor.obj ((Opens.map f.base).obj X✝))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
      (Y.restrict ⋯).presheaf.map ((eqToHom ⋯).app (op X✝)) =
    g.c.app (op X✝) ≫ (Y.ofRestrict ⋯).c.app (op ((Opens.map g.base).obj X✝))

Tactic:
simp only [app_invApp_assoc,
  eqToHom_app, Category.assoc, NatTrans.naturality_assoc]

Result:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ g.c.app (op X✝) ≫
      ((TopCat.Presheaf.pushforward C g.base).obj Y.presheaf).map (homOfLE ⋯).op ≫
        Y.presheaf.map (eqToHom ⋯) ≫ (Y.restrict ⋯).presheaf.map (eqToHom ⋯) =
    g.c.app (op X✝) ≫ (Y.ofRestrict ⋯).c.app (op ((Opens.map g.base).obj X✝))

Proof state:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ g.c.app (op X✝) ≫
      ((TopCat.Presheaf.pushforward C g.base).obj Y.presheaf).map (homOfLE ⋯).op ≫
        Y.presheaf.map (eqToHom ⋯) ≫ (Y.restrict ⋯).presheaf.map (eqToHom ⋯) =
    g.c.app (op X✝) ≫ (Y.ofRestrict ⋯).c.app (op ((Opens.map g.base).obj X✝))

Tactic:
erw [← Y.presheaf.map_comp, ← Y.presheaf.map_comp]

Result:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ g.c.app (op X✝) ≫
      Y.presheaf.map ((Opens.map g.base).op.map (homOfLE ⋯).op ≫ eqToHom ⋯ ≫ ⋯.functor.op.map (eqToHom ⋯)) =
    g.c.app (op X✝) ≫ (Y.ofRestrict ⋯).c.app (op ((Opens.map g.base).obj X✝))

Proof state:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ (pullbackConeOfLeftFst f g ≫ f).c.app (op X✝) ≫ (whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app (op X✝) =
    (Y.ofRestrict ⋯ ≫ g).c.app (op X✝)

Tactic:
dsimp only [comp_c_app, unop_op, whiskerRight_app, pullbackConeOfLeftFst]

Result:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ (f.c.app (op X✝) ≫
        invApp f ((Opens.map f.base).obj X✝) ≫
          g.c.app (op (⋯.functor.obj ((Opens.map f.base).obj X✝))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
      (Y.restrict ⋯).presheaf.map ((eqToHom ⋯).app (op X✝)) =
    g.c.app (op X✝) ≫ (Y.ofRestrict ⋯).c.app (op ((Opens.map g.base).obj X✝))

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
⊢ (pullbackConeOfLeftFst f g ≫ f).base = (Y.ofRestrict ⋯ ≫ g).base

Tactic:
simpa using pullback.condition

Result:
no goals

Proof state:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ g.c.app (op X✝) ≫
      Y.presheaf.map ((Opens.map g.base).op.map (homOfLE ⋯).op ≫ eqToHom ⋯ ≫ ⋯.functor.op.map (eqToHom ⋯)) =
    g.c.app (op X✝) ≫ (Y.ofRestrict ⋯).c.app (op ((Opens.map g.base).obj X✝))

Tactic:
congr 1

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
⊢ pullbackConeOfLeftFst f g ≫ f = Y.ofRestrict ⋯ ≫ g

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

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
⊢ (pullbackConeOfLeftFst f g ≫ f).base = (Y.ofRestrict ⋯ ≫ g).base

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens ↑↑Z)ᵒᵖ
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app U =
    (Y.ofRestrict ⋯ ≫ g).c.app U

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens ↑↑Z)ᵒᵖ
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app U =
    (Y.ofRestrict ⋯ ≫ g).c.app U

Tactic:
induction U using Opposite.rec'

Result:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app (op X✝) =
    (Y.ofRestrict ⋯ ≫ g).c.app (op X✝)

Proof state:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app (op X✝) =
    (Y.ofRestrict ⋯ ≫ g).c.app (op X✝)

Tactic:
rw [NatTrans.comp_app]

Result:
case refine_2.h
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
X✝ : Opens ↑↑Z
⊢ (pullbackConeOfLeftFst f g ≫ f).c.app (op X✝) ≫ (whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app (op X✝) =
    (Y.ofRestrict ⋯ ≫ g).c.app (op X✝)