awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
⊢ (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.obj U ≅
    (Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf).obj U
have app : (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop U))) = U
Tactic: refine asIso (f.c.app (op (opensFunctor f |>.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso ?_)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop U))) = U
have app : ∀ (U : Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry) : TopCat) : Type u_1)),
  (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U
Tactic: induction U with | op U => ?_
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U
have app : ∀ (carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry) : TopCat) : Type u_1))
  (is_open' : IsOpen carrier),
  (Opens.map f.base).op.obj
      (op
        ((opensFunctor f).obj
          (unop
            (op
              { carrier := carrier, is_open' := is_open' :
                Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry) : TopCat) : Type u_1) })))) =
    op { carrier := carrier, is_open' := is_open' }
Tactic: cases U
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
is_open' : IsOpen carrier
⊢ (Opens.map f.base).op.obj
      (op
        ((opensFunctor f).obj
          (unop
            (op
              { carrier := carrier, is_open' := is_open' :
                Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) })))) =
    op { carrier := carrier, is_open' := is_open' }
have app : op
    {
      carrier :=
        (⇑(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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
          (↑((opensFunctor f).obj
                { carrier := carrier, is_open' := is_open' :
                  Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry) : TopCat) : Type u_1) }) :
            Set (↑(↑Y : TopCat) : Type u_1)),
      is_open' := sorry : Opens (↑(↑X : TopCat) : Type u_1) } =
  op { carrier := carrier, is_open' := is_open' }
Tactic: dsimp only [IsOpenMap.functor, Functor.op, Opens.map]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
is_open' : IsOpen carrier
⊢ op
      {
        carrier :=
          (⇑(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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
            (↑((opensFunctor f).obj
                  { carrier := carrier, is_open' := is_open' :
                    Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) }) :
              Set (↑(↑Y : TopCat) : Type u_1)),
        is_open' := ⋯ : Opens (↑(↑X : TopCat) : Type u_1) } =
    op { carrier := carrier, is_open' := is_open' }
have app : (⇑(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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
    (↑((opensFunctor f).obj
          { carrier := carrier, is_open' := is_open' :
            Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry) : TopCat) : Type u_1) }) :
      Set (↑(↑Y : TopCat) : Type u_1)) =
  carrier
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
is_open' : IsOpen carrier
⊢ (⇑(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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
      (↑((opensFunctor f).obj
            { carrier := carrier, is_open' := is_open' :
              Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) }) :
        Set (↑(↑Y : TopCat) : Type u_1)) =
    carrier
have app : (↑{ carrier := carrier, is_open' := is_open' :
        Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry) : TopCat) : Type u_1) } :
    Set (↑(↑X : TopCat) : Type u_1)) =
  carrier
Tactic: erw [Set.preimage_image_eq _ H.base_open.injective]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.map i ≫
      Iso.hom (asIso (f.c.app (op ((opensFunctor f).obj (unop V)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)) =
    Iso.hom (asIso (f.c.app (op ((opensFunctor f).obj (unop U)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf).map i
have naturality : Eq (α :=
  Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ⟶
    X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
  (Y.presheaf.map (Quiver.Hom.op (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) sorry) i.unop)) ≫
    f.c.app (op ((opensFunctor f).obj (unop V))) ≫ X.presheaf.map (eqToHom sorry))
  ((f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom sorry)) ≫
    X.presheaf.map ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ Eq (α :=
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (Y.presheaf.map (Quiver.Hom.op (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) ⋯) i.unop)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V))) ≫ X.presheaf.map (eqToHom ⋯))
    ((f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom ⋯)) ≫
      X.presheaf.map ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op)
have naturality : Eq (α :=
  Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ⟶
    X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
  (f.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ≫
      X.presheaf.map
          (Quiver.Hom.op
            ((Opens.map f.base).map (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) sorry) i.unop))) ≫
        X.presheaf.map (eqToHom sorry) :
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
  (f.c.app (op ((opensFunctor f).obj (unop U))) ≫
      X.presheaf.map (eqToHom sorry) ≫ X.presheaf.map ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op :
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
Tactic: simp only [NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_obj,
        TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op, Category.assoc]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ Eq (α :=
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (f.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ≫
        X.presheaf.map
            (Quiver.Hom.op
              ((Opens.map f.base).map (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) ⋯) i.unop))) ≫
          X.presheaf.map (eqToHom ⋯) :
      Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
        X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (f.c.app (op ((opensFunctor f).obj (unop U))) ≫
        X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op :
      Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
        X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
have naturality : Eq (α :=
  Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ⟶
    X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
  (f.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ≫
      X.presheaf.map
        (Quiver.Hom.op
            ((Opens.map f.base).map (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) sorry) i.unop)) ≫
          eqToHom sorry) :
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
  (f.c.app (op ((opensFunctor f).obj (unop U))) ≫
      X.presheaf.map (eqToHom sorry ≫ ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op) :
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
Tactic: rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
      (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
      (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y) =
    f
have refine : ∀ (x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ),
  ((CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
              (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
              (Y.ofRestrict sorry : Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry ⟶ Y)).c ≫
          Functor.whiskerRight (eqToHom sorry) X.presheaf).app
      x =
    f.c.app x
Tactic: refine PresheafedSpace.Hom.ext _ _ rfl <| NatTrans.ext <| funext fun x => ?_
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ ((CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
              (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
              (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)).c ≫
          Functor.whiskerRight (eqToHom ⋯) X.presheaf).app
      x =
    f.c.app x
have simp : ((CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
            (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
            (Y.ofRestrict sorry : Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry ⟶ Y)).c ≫
        𝟙
          ((Opens.map
                (CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
                    (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
                    (Y.ofRestrict sorry : Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry ⟶ Y)).base).op ⋙
            X.presheaf)).app
    x =
  f.c.app x
Tactic: simp only [eqToHom_refl,
    Functor.whiskerRight_id']
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ ((CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
              (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
              (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)).c ≫
          𝟙
            ((Opens.map
                  (CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
                      (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
                      (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)).base).op ⋙
              X.presheaf)).app
      x =
    f.c.app x
have erw : f.c.app x ≫
    X.presheaf.map
      (CategoryStruct.comp (Y :=
        (Opens.map f.base).op.obj
          (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) sorry)) ((Opens.map f.base).op.obj x)))
        ((Opens.map f.base).op.map
            (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction sorry)) (unop x))) :
          (Opens.map f.base).op.obj x ⟶
            (Opens.map f.base).op.obj
              (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) sorry)) ((Opens.map f.base).op.obj x)))
        (Iso.hom (eqToIso sorry) :
          (Opens.map f.base).op.obj
              (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict sorry))) (unop x)))))) ⟶
            op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict sorry))) (unop x)))) =
  f.c.app x
Tactic: erw [Category.comp_id, comp_c_app, f.c.naturality_assoc, ← X.presheaf.map_comp]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ f.c.app x ≫
      X.presheaf.map
        (CategoryStruct.comp (Y :=
          (Opens.map f.base).op.obj
            (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          ((Opens.map f.base).op.map
              (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) (unop x))) :
            (Opens.map f.base).op.obj x ⟶
              (Opens.map f.base).op.obj
                (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          (Iso.hom (eqToIso ⋯) :
            (Opens.map f.base).op.obj
                (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))))) ⟶
              op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))) =
    f.c.app x
have trans : f.c.app x ≫
    X.presheaf.map
      (CategoryStruct.comp (Y :=
        (Opens.map f.base).op.obj
          (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) sorry)) ((Opens.map f.base).op.obj x)))
        ((Opens.map f.base).op.map
            (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction sorry)) (unop x))) :
          (Opens.map f.base).op.obj x ⟶
            (Opens.map f.base).op.obj
              (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) sorry)) ((Opens.map f.base).op.obj x)))
        (Iso.hom (eqToIso sorry) :
          (Opens.map f.base).op.obj
              (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict sorry))) (unop x)))))) ⟶
            op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict sorry))) (unop x)))) =
  f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x))
Tactic: trans f.c.app x ≫ X.presheaf.map (𝟙 _)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
trans :
  f.c.app x ≫
      X.presheaf.map
        (CategoryStruct.comp (Y :=
          (Opens.map f.base).op.obj
            (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          ((Opens.map f.base).op.map
              (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) (unop x))) :
            (Opens.map f.base).op.obj x ⟶
              (Opens.map f.base).op.obj
                (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          (Iso.hom (eqToIso ⋯) :
            (Opens.map f.base).op.obj
                (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))))) ⟶
              op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))) =
    f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x))
⊢ f.c.app x ≫
      X.presheaf.map
        (CategoryStruct.comp (Y :=
          (Opens.map f.base).op.obj
            (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          ((Opens.map f.base).op.map
              (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) (unop x))) :
            (Opens.map f.base).op.obj x ⟶
              (Opens.map f.base).op.obj
                (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          (Iso.hom (eqToIso ⋯) :
            (Opens.map f.base).op.obj
                (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))))) ⟶
              op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))) =
    f.c.app x
have trans₁ : f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x)) = f.c.app x
Tactic: trans f.c.app x ≫ X.presheaf.map (𝟙 _)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Eq (α := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
    (Iso.inv (isoRestrict f) ≫ f : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
    (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
have rw : f =
  CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
    (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
    (Y.ofRestrict sorry : Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry ⟶ Y)
Tactic: rw [Iso.inv_comp_eq, isoRestrict_hom_ofRestrict]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
rw :
  f =
    CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
      (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
      (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
⊢ Eq (α := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
    (Iso.inv (isoRestrict f) ≫ f : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
    (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
have rw₁ : f = f
Tactic: rw [Iso.inv_comp_eq, isoRestrict_hom_ofRestrict]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Mono f
have rw : Mono
  (CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
    (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry)
    (Y.ofRestrict sorry : Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry ⟶ Y))
Tactic: rw [← H.isoRestrict_hom_ofRestrict]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
V : Opens (↑(↑Y : TopCat) : Type u_1)
U : Opens (↑(↑X : TopCat) : Type u_1)
h : V = (opensFunctor f).obj U
⊢ IsIso (X := Y.presheaf.obj (op V)) (f.c.app (op V))
have subst : IsIso (X := Y.presheaf.obj (op ((opensFunctor f).obj U))) (f.c.app (op ((opensFunctor f).obj U)))
Tactic: subst h
Cleared hypotheses: V, h
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
⊢ IsIso (X := Z.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := (f ≫ g).base) ⋯) U)))
    ((f ≫ g).c.app (op (Functor.obj (IsOpenEmbedding.functor (f := (f ≫ g).base) ⋯) U)))
have generalize_proofs : ∀
  (h :
    IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))),
  IsIso (X := Z.presheaf.obj (op (h.functor.obj U))) ((f ≫ g).c.app (op (h.functor.obj U)))
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
⊢ IsIso (X := Z.presheaf.obj (op (h.functor.obj U))) ((f ≫ g).c.app (op (h.functor.obj U)))
have dsimp : IsIso (X := Z.presheaf.obj (op (h.functor.obj U)))
  (g.c.app (op (h.functor.obj U)) ≫ f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
Tactic: dsimp only [AlgebraicGeometry.PresheafedSpace.comp_c_app, unop_op, Functor.op, comp_base,
      Opens.map_comp_obj]