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 Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
    (PresheafedSpace.forget CommRingCat)
have inst : cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
    ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr) ≅
  cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
Tactic: apply +allowSynthFailures preservesLimit_of_iso_diagram
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst_1 : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst :
  cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr) ≅
    cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
⊢ PreservesLimit (cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
    (PresheafedSpace.forget CommRingCat)
have inst₁ : PreservesLimit
  (cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
    ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr))
  (PresheafedSpace.forget CommRingCat)
Tactic: apply +allowSynthFailures preservesLimit_of_iso_diagram
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst_1 : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst :
  cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr) ≅
    cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
inst₁ :
  PreservesLimit
    (cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr))
    (PresheafedSpace.forget CommRingCat)
⊢ PreservesLimit (cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
    (PresheafedSpace.forget CommRingCat)
have inst₂ : WalkingCospan ⥤ PresheafedSpace CommRingCat
Tactic: apply +allowSynthFailures preservesLimit_of_iso_diagram
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit
    (cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr))
    (PresheafedSpace.forget CommRingCat)
have inst : PreservesLimit (C := PresheafedSpace CommRingCat) (cospan f.toHom g.toHom) (PresheafedSpace.forget CommRingCat)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
⊢ IsIso (X := pullback f g) (pullback.snd f g)
have inst : IsIso (X := forgetToSheafedSpace.obj (pullback f g)) (forgetToSheafedSpace.map (pullback.snd f g))
Tactic: apply +allowSynthFailures Functor.ReflectsIsomorphisms.reflects
    (F := LocallyRingedSpace.forgetToSheafedSpace)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
⊢ IsIso (X := forgetToSheafedSpace.obj (pullback f g)) (forgetToSheafedSpace.map (pullback.snd f g))
have inst : IsIso (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (pullback f g)))
  (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map (pullback.snd f g)))
Tactic: apply +allowSynthFailures Functor.ReflectsIsomorphisms.reflects
    (F := SheafedSpace.forgetToPresheafedSpace)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
⊢ IsIso (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (pullback f g)))
    (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map (pullback.snd f g)))
have inst : IsIso (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (pullback f g)))
  (CategoryStruct.comp (Y :=
    pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
      ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))
    (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g))
    (pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
      ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g)))
Tactic: erw [← PreservesPullback.iso_hom_snd
      (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H'
have rw : l ≫ f = lift f g H' ≫ f
Tactic: rw [← cancel_mono f, hl, lift_fac]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
l : Y ⟶ X
hl : l ≫ f = g
rw : l ≫ f = lift f g H' ≫ f
⊢ l = lift f g H'
have rw₁ : g = lift f g H' ≫ f
Tactic: rw [← cancel_mono f, hl, lift_fac]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
l : Y ⟶ X
hl : l ≫ f = g
rw : l ≫ f = lift f g H' ≫ f
rw₁ : g = lift f g H' ≫ f
⊢ l = lift f g H'
have rw₂ : g = g
Tactic: rw [← cancel_mono f, hl, lift_fac]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
⊢ Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) (lift f g H').base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.preimage (β := (↑(↑Z.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
      (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))))
have this : IsIso (X := pullback f g) (pullback.snd f g)
Tactic: have := pullback_snd_isIso_of_range_subset f g H'
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
this : IsIso (X := pullback f g) (pullback.snd f g)
⊢ Eq (α := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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)
            (CategoryStruct.comp (Y := pullback f g) (inv (pullback.snd f g)) (pullback.fst f g)).base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.preimage (β := (↑(↑Z.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
      (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))))
have this₁ : Eq (α := (↑(pullback f g).toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat))
  (CategoryStruct.comp (Y :=
    pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
      ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))
    (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g))
    (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
      ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)))
  (PresheafedSpace.Hom.base (Hom.toHom (pullback.fst f g)))
Tactic: have : _ = (pullback.fst f g).base :=
    PreservesPullback.iso_hom_fst
      (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ CategoryStruct.comp (Y := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
      (Iso.hom (isoRestrict f) :
        X ⟶ Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
      (Y.ofRestrict ⋯ : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯ ⟶ Y) =
    f
have a : forgetToSheafedSpace.map
    (CategoryStruct.comp (Y := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) sorry)
      (Iso.hom (isoRestrict f) :
        X ⟶ Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) sorry)
      (Y.ofRestrict sorry : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) sorry ⟶ Y)) =
  forgetToSheafedSpace.map f
Tactic: apply LocallyRingedSpace.forgetToSheafedSpace.map_injective
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑X.toTopCat : Type u_1)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U
have this : Set.preimage (β := (↑(↑Y.toPresheafedSpace : 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) (Hom.toShHom f).hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : 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) (Hom.toShHom f).hom.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ''
      U.carrier) =
  U.carrier
Tactic: have := Set.preimage_image_eq U.1 H.base_open.injective
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑X.toTopCat : Type u_1)
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))
have this : Set.preimage (β := (↑(↑Y.toPresheafedSpace : 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) (Hom.toShHom f).hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : 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) (Hom.toShHom f).hom.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ''
      U.carrier) =
  U.carrier
Tactic: have := Set.preimage_image_eq U.1 H.base_open.injective
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst : Epi f.base
⊢ IsIso f
have rw : IsIso (forgetToSheafedSpace.map f)
Tactic: rw [← isIso_iff_of_reflects_iso _ LocallyRingedSpace.forgetToSheafedSpace]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst : Epi f.base
⊢ IsIso (forgetToSheafedSpace.map f)
have this : Epi (forgetToSheafedSpace.map f).hom.base
Tactic: have : Epi (forgetToSheafedSpace.map f).hom.base := by assumption
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
⊢ IsOpenEmbedding (X := (↑(↑(D.U i) : TopCat) : Type v)) (Y := (↑(↑D.glued : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑D.glued : TopCat)) (Hom.base (D.ι i))) :
      (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
have rw : IsOpenEmbedding (X := (↑(↑(D.U i) : TopCat) : Type v)) (Y := (↑(↑D.glued : TopCat) : Type v))
  (Function.comp (β := (↑(D.mapGlueData (forget C)).glued : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
            (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ Functor.obj (forget C) D.glued) :
          C((↑(D.mapGlueData (forget C)).glued : Type v), (↑(↑D.glued : TopCat) : Type v))) :
      (a : (↑(D.mapGlueData (forget C)).glued : Type v)) → (↑(↑D.glued : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι i)) :
      (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))
Tactic: rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _, TopCat.coe_comp]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
S : Set (↑(↑(D.V (i, j)) : TopCat) : Type v)
⊢ Eq (α := Set (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.fst (D.f i j) (D.f i k)))) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, j)) : TopCat) : Type v)) ⁻¹'
        S))
    (Set.preimage (β := (↑(↑(D.U i) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i k).base) :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.f i j).base) :
          (a : (↑(↑(D.V (i, j)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ''
        S))
have eq₁ : Eq (α := (↑(pullback (D.f i j) (D.f i k)) : TopCat) ⟶ (↑(D.V (i, j)) : TopCat))
  (CategoryStruct.comp (Y :=
      pullback (X := Functor.obj (forget C) (D.V (i, j))) (CategoryTheory.Functor.map (forget C) (D.f i j))
        (CategoryTheory.Functor.map (forget C) (D.f i k)))
      (Iso.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)))
      (pullback.fst (CategoryTheory.Functor.map (forget C) (D.f i j))
        (CategoryTheory.Functor.map (forget C) (D.f i k))) :
    Functor.obj (forget C) (pullback (D.f i j) (D.f i k)) ⟶ Functor.obj (forget C) (D.V (i, j)))
  (Hom.base (pullback.fst (D.f i j) (D.f i k)))
Tactic: have eq₁ : _ = (π₁ i, j, k).base := PreservesPullback.iso_hom_fst (forget C) _ _