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
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)))
    (g.c.app (op (h.functor.obj U)) ≫ f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
have x : IsIso (X := Z.presheaf.obj (op (h.functor.obj U))) (g.c.app (op (h.functor.obj U)))
Tactic: apply IsIso.comp_isIso'
-- 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))
x : IsIso (X := Z.presheaf.obj (op (h.functor.obj U))) (g.c.app (op (h.functor.obj U)))
⊢ 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))))
have x₁ : IsIso (X := (Functor.obj (TopCat.Presheaf.pushforward C g.base) Y.presheaf).obj (op (h.functor.obj U)))
  (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
Tactic: apply IsIso.comp_isIso'
-- 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))
⊢ h.functor.obj U = (opensFunctor g).obj ((opensFunctor f).obj U)
have h₁ : ∀ (x : (↑(↑Z : TopCat) : Type u_1)),
  x ∈ (↑(h.functor.obj U) : Set (↑(↑Z : TopCat) : Type u_1)) ↔
    x ∈ (↑((opensFunctor g).obj ((opensFunctor f).obj U)) : Set (↑(↑Z : TopCat) : Type u_1))
Tactic: ext
-- 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 := (Functor.obj (TopCat.Presheaf.pushforward C g.base) Y.presheaf).obj (op (h.functor.obj U)))
    (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
have x : (Opens.map g.base).obj (h.functor.obj U) = (opensFunctor f).obj U
Tactic: apply c_iso' f 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
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))
⊢ (Opens.map g.base).obj (h.functor.obj U) = (opensFunctor f).obj U
have x : (↑((Opens.map g.base).obj (h.functor.obj U)) : Set (↑(↑Y : TopCat) : Type u_1)) =
  (↑((opensFunctor f).obj U) : Set (↑(↑Y : TopCat) : Type u_1))
Tactic: ext1
-- 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))
⊢ (↑((Opens.map g.base).obj (h.functor.obj U)) : Set (↑(↑Y : TopCat) : Type u_1)) =
    (↑((opensFunctor f).obj U) : Set (↑(↑Y : TopCat) : Type u_1))
have x : Eq (α := Set (↑(↑Y : TopCat) : Type u_1))
  (Set.preimage (β := (↑(↑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) g.base) :
      (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
    (Function.comp (β := (↑(↑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))
        (⇑(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)) ''
      (↑U : Set (↑(↑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)) → (↑(↑Y : TopCat) : Type u_1)) ''
    (↑U : Set (↑(↑X : TopCat) : Type u_1)))
Tactic: dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj, comp_base, TopCat.coe_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
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))
⊢ Eq (α := Set (↑(↑Y : TopCat) : Type u_1))
    (Set.preimage (β := (↑(↑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) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
      (Function.comp (β := (↑(↑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))
          (⇑(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)) ''
        (↑U : Set (↑(↑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)) → (↑(↑Y : TopCat) : Type u_1)) ''
      (↑U : Set (↑(↑X : TopCat) : Type u_1)))
have x : Eq (α := Set (↑(↑Y : TopCat) : Type u_1))
  (Set.preimage (β := (↑(↑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) g.base) :
      (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
    (Set.image (α := (↑(↑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))
      ((⇑(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)) ''
        (↑U : Set (↑(↑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)) → (↑(↑Y : TopCat) : Type u_1)) ''
    (↑U : Set (↑(↑X : TopCat) : Type u_1)))
Tactic: rw [Set.image_comp, Set.preimage_image_eq _ hg.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 (↑(↑X : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)
have simp : (X.presheaf.map i ≫ X.presheaf.map (eqToHom sorry)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
  (X.presheaf.map (eqToHom sorry) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
    Y.presheaf.map ((opensFunctor f).op.map i)
Tactic: simp only [invApp, ← 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 (↑(↑X : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ (X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)
have rw : X.presheaf.map i ≫ X.presheaf.map (eqToHom sorry) =
  ((X.presheaf.map (eqToHom sorry) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)) ≫
    f.c.app (op ((opensFunctor f).obj (unop V)))
Tactic: rw [IsIso.comp_inv_eq]
-- 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 (↑(↑X : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))
have simp : X.presheaf.map (i ≫ eqToHom sorry) = X.presheaf.map (eqToHom sorry ≫ ((Opens.map f.base).map ((opensFunctor f).map i.unop)).op)
Tactic: simp only [Functor.op_obj, op_unop, ← X.presheaf.map_comp, Functor.op_map, Category.assoc,
    NatTrans.naturality, Quiver.Hom.unop_op, IsIso.inv_hom_id_assoc,
    TopCat.Presheaf.pushforward_obj_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
U : Opens (↑(↑X : TopCat) : Type u_1)
⊢ IsIso (Y := Y.presheaf.obj (op ((opensFunctor f).obj U))) (invApp f U)
have delta : IsIso (Y := Y.presheaf.obj (op ((opensFunctor f).obj U)))
  (X.presheaf.map (eqToHom sorry) ≫ inv (f.c.app (op ((opensFunctor f).obj U))))
Tactic: delta invApp
-- 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 (↑(↑X : TopCat) : Type u_1)
⊢ Eq (α := Y.presheaf.obj (op ((opensFunctor f).obj U)) ⟶ X.presheaf.obj (op U)) (inv (invApp f U))
    (f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯))
have rw : 𝟙 (X.presheaf.obj (op U)) =
  CategoryStruct.comp (Y := Y.presheaf.obj (op ((opensFunctor f).obj U))) (invApp f U)
    (f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom sorry))
Tactic: rw [← cancel_epi (H.invApp _ U), IsIso.hom_inv_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
U : Opens (↑(↑X : TopCat) : Type u_1)
⊢ 𝟙 (X.presheaf.obj (op U)) =
    CategoryStruct.comp (Y := Y.presheaf.obj (op ((opensFunctor f).obj U))) (invApp f U)
      (f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯))
have delta : 𝟙 (X.presheaf.obj (op U)) =
  CategoryStruct.comp (Y := Y.presheaf.obj (op ((opensFunctor f).obj U)))
    (X.presheaf.map (eqToHom sorry) ≫ inv (f.c.app (op ((opensFunctor f).obj U))))
    (f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom sorry))
Tactic: delta invApp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U))) ((Y.ofRestrict hf).c.app (op (hf.functor.obj U)))
have dsimp : IsIso (X := Y.presheaf.obj (op (hf.functor.obj U)))
  (Y.presheaf.map (Quiver.Hom.op (sorry.adjunction.counit.app (hf.functor.obj U))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
⊢ (Opens.map f).obj (hf.functor.obj U) = U
have h : (↑((Opens.map f).obj (hf.functor.obj U)) : Set (↑X : Type w)) = (↑U : Set (↑X : Type w))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U)))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
have this : (Opens.map f).obj (hf.functor.obj U) = U
Tactic: have : (Opens.map f).obj (hf.functor.obj U) = U := by
      ext1
      exact Set.preimage_image_eq _ hf.injective
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U)))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
have h : Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
Tactic: convert_to IsIso (Y.presheaf.map (𝟙 _))
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
h : Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U)))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
have h₁ : Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U)) →
  HEq (α :=
    Y.presheaf.obj (op (hf.functor.obj U)) ⟶
      Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))))
    (Y.presheaf.map (Quiver.Hom.op (sorry.adjunction.counit.app (hf.functor.obj U))))
    (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
Tactic: convert_to IsIso (Y.presheaf.map (𝟙 _))
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
h : Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
h₁ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U)) →
    HEq (α :=
      Y.presheaf.obj (op (hf.functor.obj U)) ⟶
        Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))))
      (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
      (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U)))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
have convert_2 : IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
Tactic: convert_to IsIso (Y.presheaf.map (𝟙 _))
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4 :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ HEq (α :=
    Y.presheaf.obj (op (hf.functor.obj U)) ⟶
      Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
    (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
have h : sorry.functor.obj ((Opens.map f).obj (hf.functor.obj U)) = unop (op (hf.functor.obj U))
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4 :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
h : ⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) = unop (op (hf.functor.obj U))
⊢ HEq (α :=
    Y.presheaf.obj (op (hf.functor.obj U)) ⟶
      Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
    (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
have h₁ : HEq (α := sorry.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U)
  (sorry.adjunction.counit.app (hf.functor.obj U)) (β := unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
  (𝟙 (unop (op (hf.functor.obj U))))
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4 :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ HEq (α := ⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U)
    (⋯.adjunction.counit.app (hf.functor.obj U)) (β := unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
    (𝟙 (unop (op (hf.functor.obj U))))
have h : (sorry.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U) =
  (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
Tactic: apply Subsingleton.helim
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4 :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ (⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U) =
    (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
have h : (sorry.functor.obj U ⟶ hf.functor.obj U) = (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
Tactic: rw [this]