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 : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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)))
    (Set.range (ι := (↑(↑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)) → (↑(↑Z : TopCat) : Type u_1)))
this : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
⊢ IsIso (X := (↑(pullback f g) : TopCat)) (Hom.base (limit.π (cospan f g) WalkingCospan.right))
have rw : IsIso (X := (↑(pullback f g) : TopCat))
  (Hom.base
    (Iso.hom (limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }) ≫
      { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) }.cone.π.app
        WalkingCospan.right))
Tactic: rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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)))
    (Set.range (ι := (↑(↑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)) → (↑(↑Z : TopCat) : Type u_1)))
this : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
⊢ IsIso (X := (↑(pullback f g) : TopCat))
    (Hom.base
      (Iso.hom (limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }) ≫
        { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) }.cone.π.app
          WalkingCospan.right))
have change : IsIso (X := (↑(pullback f g) : TopCat))
  (Hom.base
      (Iso.hom
        (limit.isoLimitCone
          { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) })) ≫
    pullback.snd f.base g.base)
Tactic: change IsIso (_ ≫ pullback.snd _ _)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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)))
    (Set.range (ι := (↑(↑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)) → (↑(↑Z : TopCat) : Type u_1)))
this : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
⊢ IsIso (X := pullback f g) (pullback.snd f g)
have this₁ : IsIso (X := (↑(pullback f g) : TopCat)) (Hom.base (pullback.snd f g))
Tactic: have : IsIso (pullback.snd f g).base := by
    delta pullback.snd
    rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
    change IsIso (_ ≫ pullback.snd _ _)
    infer_instance
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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)))
    (Set.range (ι := (↑(↑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)) → (↑(↑Z : 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:
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
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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)))
    (Set.range (ι := (↑(↑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)) → (↑(↑Z : 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:
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
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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)))
    (Set.range (ι := (↑(↑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)) → (↑(↑Z : 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 (goal)
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
inst_1 : IsOpenImmersion g
e :
  Eq (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑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)))
⊢ lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X
have rw : (lift g f sorry ≫ lift f g sorry) ≫ f = 𝟙 X ≫ f
Tactic: rw [← cancel_mono f]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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
inst_1 : IsOpenImmersion g
e :
  Eq (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑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)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑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)))
⊢ lift f g ⋯ ≫ lift g f ⋯ = 𝟙 Y
have rw : (lift f g sorry ≫ lift g f sorry) ≫ g = 𝟙 Y ≫ g
Tactic: rw [← cancel_mono g]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ X.presheaf.IsSheaf
have apply : (Functor.obj
    (TopCat.Presheaf.pushforward C (Hom.base (Iso.hom (Iso.symm (isoRestrict f)))) :
      TopCat.Presheaf.{u_1, v, u} C (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry) : TopCat) ⥤
        TopCat.Presheaf.{u_1, v, u} C (↑X : TopCat))
    (Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry).presheaf).IsSheaf
Tactic: apply TopCat.Presheaf.isSheaf_of_iso (sheafIsoOfIso (isoRestrict f).symm).symm
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ (Functor.obj
      (TopCat.Presheaf.pushforward C (Hom.base (Iso.hom (Iso.symm (isoRestrict f)))) :
        TopCat.Presheaf.{u_1, v, u} C (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) ⥤
          TopCat.Presheaf.{u_1, v, u} C (↑X : TopCat))
      (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf).IsSheaf
have h : (Y.restrict (U := (↑X : TopCat)) (f := f.base) sorry).presheaf.IsSheaf
Tactic: apply TopCat.Sheaf.pushforward_sheaf_of_sheaf
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
inst_1 : SheafedSpace.IsOpenImmersion f
⊢ toSheafedSpace Y f.hom = X
have mk : ∀ (toPresheafedSpace : PresheafedSpace.{v, u, u_1} C) (IsSheaf : toPresheafedSpace.presheaf.IsSheaf)
  (f : { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf : SheafedSpace.{u, v, u_1} C } ⟶ Y)
  [inst_2 : SheafedSpace.IsOpenImmersion f],
  toSheafedSpace Y f.hom = { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf }
Tactic: cases X
Cleared hypotheses: X, f, inst_1
-- 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 : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑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 = Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U)
have h : (↑U : Set (↑(↑Y : TopCat) : Type u_1)) =
  (↑(Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) ((Opens.map f.base).obj U)) :
    Set (↑(↑Y : TopCat) : Type u_1))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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 : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑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))
⊢ IsIso (X := Y.presheaf.obj (op U)) (f.c.app (op U))
have this : U = Functor.obj (IsOpenEmbedding.functor (f := f.base) sorry) ((Opens.map f.base).obj U)
Tactic: have : U = H.base_open.functor.obj ((Opens.map f.base).obj U) := by
    ext1
    exact (Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
have change : HasLimit
  (cospan (X := Functor.obj forget X) (CategoryTheory.Functor.map forget f) (CategoryTheory.Functor.map forget g))
Tactic: change HasLimit (cospan ((forget).map f) ((forget).map g))
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan f g ⋙ forget)
have this : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
Tactic: have : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl)
      ((cospan f g ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map f) ((forget).map g))
    infer_instance
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))
have change : HasLimit
  (cospan (X := Functor.obj forget Y) (CategoryTheory.Functor.map forget g) (CategoryTheory.Functor.map forget f))
Tactic: change HasLimit (cospan ((forget).map g) ((forget).map f))
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan g f ⋙ forget)
have this : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))
Tactic: have : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl)
      ((cospan g f ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map g) ((forget).map f))
    infer_instance
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    (PresheafedSpace.forget C)
have dsimp : PreservesLimit (cospan f.hom g.hom) (PresheafedSpace.forget C)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g ⋙ forget) (PresheafedSpace.forget C)
have this : PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
  (PresheafedSpace.forget C)
Tactic: have : PreservesLimit
        (cospan ((cospan f g ⋙ forget).map Hom.inl)
          ((cospan f g ⋙ forget).map Hom.inr)) (PresheafedSpace.forget C) := by
        dsimp
        infer_instance
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace) (InducedCategory.Hom.hom (pullback.snd f g))
have this : Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
  (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
    (Iso.hom (preservesLimitIso forget (cospan f g)) :
      Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
    (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
  (InducedCategory.Hom.hom (pullback.snd f g))
Tactic: have : _ = (pullback.snd f g).hom := preservesLimitIso_hom_π forget (cospan f g) right
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace) (InducedCategory.Hom.hom (pullback.snd f g))
have rw : PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
  (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
    (Iso.hom (preservesLimitIso forget (cospan f g)) :
      Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
    (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
have this₁ : Eq (α :=
  limit (cospan f g ⋙ forget) ⟶
    (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)).obj right)
  (CategoryStruct.comp (Y := limit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)))
    (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))))
    (limit.π (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)) right))
  (limit.π (cospan f g ⋙ forget) right ≫ (diagramIsoCospan (cospan f g ⋙ forget)).hom.app right)
Tactic: have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan f g ⋙ forget)) right
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
this :
  Eq (α := limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget)))) (limit.π (cospan f.hom g.hom) right))
    (limit.π (cospan f g ⋙ forget) right ≫ 𝟙 Y.toPresheafedSpace)
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
have this₁ : Eq (α := limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace)
  (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
    (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget)))) (limit.π (cospan f.hom g.hom) right))
  (limit.π (cospan f g ⋙ forget) right)
Tactic: rw [Category.comp_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
this :
  Eq (α := limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget)))) (limit.π (cospan f.hom g.hom) right))
    (limit.π (cospan f g ⋙ forget) right)
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
have rw : PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
  (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
    (Iso.hom (preservesLimitIso forget (cospan f g)) :
      Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
    (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
        (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget)))) (limit.π (cospan f.hom g.hom) right) :
      limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace) (InducedCategory.Hom.hom (pullback.fst g f))
have this : Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
  (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
    (Iso.hom (preservesLimitIso forget (cospan g f)) :
      Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
    (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
  (InducedCategory.Hom.hom (pullback.fst g f))
Tactic: have : _ = (pullback.fst g f).hom := preservesLimitIso_hom_π forget (cospan g f) left