awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : PullbackCone f g
x : Opens (↑(↑X : TopCat) : Type u_1)
this :
  Eq (α :=
    Z.presheaf.obj (op ((opensFunctor f).obj x)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (s.snd ≫ g).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)))
    ((f.c.app (op ((opensFunctor f).obj x)) ≫ s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x)))) ≫
      inv (s.pt.presheaf.map (eqToHom ⋯)))
    (g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have this₁ : ∀ {Z_1 : C}
  (h :
    (Functor.obj (TopCat.Presheaf.pushforward C (s.snd ≫ g).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶
      Z_1),
  f.c.app (op ((opensFunctor f).obj x)) ≫
      s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom sorry)) ≫ h =
    g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
Tactic: replace this := reassoc_of% 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 : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens (↑(↑X : TopCat) : Type u_1)
this :
  ∀ {Z_1 : C}
    (h :
      (Functor.obj (TopCat.Presheaf.pushforward C (s.snd ≫ g).base) s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶
        Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: erw [← this, hf.invApp_app_assoc, s.fst.c.naturality_assoc]
-- 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
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd
have refine_1 : (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).base = s.snd.base
Tactic: refine PresheafedSpace.Hom.ext _ _ ?_ <| 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 Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
refine_1 : (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).base = s.snd.base
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd
have refine_2 : ∀ (x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ),
  NatTrans.app
      ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ Functor.whiskerRight (eqToHom sorry) s.pt.presheaf)
      x =
    s.snd.c.app x
Tactic: refine PresheafedSpace.Hom.ext _ _ ?_ <| 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 Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ NatTrans.app
      ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf)
      x =
    s.snd.c.app x
have refine_2 : ((pullbackConeOfLeft f g).snd.c.app x ≫
      s.snd.c.app (sorry.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
        s.pt.presheaf.map (eqToHom sorry)) ≫
    NatTrans.app (Functor.whiskerRight (eqToHom sorry) s.pt.presheaf) x =
  s.snd.c.app x
Tactic: change (_ ≫ _ ≫ _) ≫ _ = _
-- 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ ((pullbackConeOfLeft f g).snd.c.app x ≫
        s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
          s.pt.presheaf.map (eqToHom ⋯)) ≫
      NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x
have refine_2 : (pullbackConeOfLeft f g).snd.c.app x ≫
    s.snd.c.app (sorry.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
      s.pt.presheaf.map (eqToHom sorry) ≫ NatTrans.app (Functor.whiskerRight (eqToHom sorry) s.pt.presheaf) x =
  s.snd.c.app x
Tactic: simp_rw [Category.assoc]
-- 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ (pullbackConeOfLeft f g).snd.c.app x ≫
      s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).snd.base).op.obj x)) ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x
have refine_2 : s.snd.c.app x ≫
    (Functor.obj (TopCat.Presheaf.pushforward C s.snd.base) s.pt.presheaf).map
        (Quiver.Hom.op (sorry.adjunction.counit.app (unop x))) ≫
      s.pt.presheaf.map (eqToHom sorry) ≫ NatTrans.app (Functor.whiskerRight (eqToHom sorry) s.pt.presheaf) x =
  s.snd.c.app x
Tactic: erw [s.snd.c.naturality_assoc]
-- 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ s.snd.c.app x ≫
      (Functor.obj (TopCat.Presheaf.pushforward C s.snd.base) s.pt.presheaf).map
          (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
        s.pt.presheaf.map (eqToHom ⋯) ≫ NatTrans.app (Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf) x =
    s.snd.c.app x
have refine_2 : s.snd.c.app x ≫
    s.pt.presheaf.map
      ((Opens.map s.snd.base).op.map (Quiver.Hom.op (sorry.adjunction.counit.app (unop x))) ≫
        eqToHom sorry ≫ NatTrans.app (eqToHom sorry) x) =
  s.snd.c.app x
Tactic: erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]
-- 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
          eqToHom ⋯ ≫ NatTrans.app (eqToHom ⋯) x) =
    s.snd.c.app x
have trans : s.snd.c.app x ≫
    s.pt.presheaf.map
      ((Opens.map s.snd.base).op.map (Quiver.Hom.op (sorry.adjunction.counit.app (unop x))) ≫
        eqToHom sorry ≫ NatTrans.app (eqToHom sorry) x) =
  s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x))
Tactic: trans s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 _)
-- 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
trans :
  s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
          eqToHom ⋯ ≫ NatTrans.app (eqToHom ⋯) x) =
    s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x))
⊢ s.snd.c.app x ≫
      s.pt.presheaf.map
        ((Opens.map s.snd.base).op.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop x))) ≫
          eqToHom ⋯ ≫ NatTrans.app (eqToHom ⋯) x) =
    s.snd.c.app x
have trans₁ : s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x)) = s.snd.c.app x
Tactic: trans s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 _)
-- 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
⊢ IsLimit (pullbackConeOfLeft f g)
have create : (s : PullbackCone f g) →
  { l : s.pt ⟶ (pullbackConeOfLeft f g).pt //
    l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
      l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
          m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }
Tactic: apply PullbackCone.isLimitAux'
-- 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_1 s : PullbackCone f g
⊢ { l : s.pt ⟶ (pullbackConeOfLeft f g).pt //
    l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
      l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
          m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }
have property : pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
  pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
    ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
      m ≫ (pullbackConeOfLeft f g).fst = s.fst →
        m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
Tactic: use pullbackConeOfLeftLift f g s
-- 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_1 s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
    pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
        m ≫ (pullbackConeOfLeft f g).fst = s.fst →
          m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
have right : pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
  ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
    m ≫ (pullbackConeOfLeft f g).fst = s.fst →
      m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
Tactic: use pullbackConeOfLeftLift_fst f g s
-- 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_1 s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
    ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
      m ≫ (pullbackConeOfLeft f g).fst = s.fst →
        m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
have right : ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
  m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
Tactic: use pullbackConeOfLeftLift_snd f g s
-- 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_1 s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
h : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m = pullbackConeOfLeftLift f g s
have right : m ≫ (pullbackConeOfLeft f g).snd = pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd
Tactic: rw [← cancel_mono (pullbackConeOfLeft f g).snd]
-- 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
⊢ IsOpenImmersion (X := pullback f g) (limit.π (cospan f g) WalkingCospan.right)
have rw : IsOpenImmersion (X := pullback f g)
  (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
s : PullbackCone f g
⊢ IsOpenImmersion (X := pullback g f) (pullback.fst g f)
have rw : IsOpenImmersion (X := pullback g f) (Iso.hom (pullbackSymmetry g f) ≫ pullback.snd f g)
Tactic: rw [← pullbackSymmetry_hom_comp_snd]
-- 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
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)
have rw : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.left ≫ f)
Tactic: rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]
-- 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
⊢ IsLimit (F := cospan f g ⋙ forget C) (Functor.mapCone (forget C) (pullbackConeOfLeft f g))
have apply : IsLimit
  ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
    (Functor.mapCone (forget C) (pullbackConeOfLeft f g)))
Tactic: apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan _) _).toFun
-- 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
⊢ IsLimit
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      (Functor.mapCone (forget C) (pullbackConeOfLeft f g)))
have refine : limit.cone (cospan f.base g.base) ≅
  (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
    (Functor.mapCone (forget C) (pullbackConeOfLeft f g))
Tactic: refine (IsLimit.equivIsoLimit ?_).toFun (limit.isLimit (cospan f.base g.base))
-- 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
⊢ limit.cone (cospan f.base g.base) ≅
    (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      (Functor.mapCone (forget C) (pullbackConeOfLeft f g))
have φ : (limit.cone (cospan f.base g.base)).pt ≅
  ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      (Functor.mapCone (forget C) (pullbackConeOfLeft f g))).pt
Tactic: fapply Cone.ext
-- 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
φ :
  (limit.cone (cospan f.base g.base)).pt ≅
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
        (Functor.mapCone (forget C) (pullbackConeOfLeft f g))).pt
⊢ limit.cone (cospan f.base g.base) ≅
    (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
      (Functor.mapCone (forget C) (pullbackConeOfLeft f g))
have w : autoParam
  (∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      Iso.hom (Iso.refl (limit.cone (cospan f.base g.base)).pt) ≫
        ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
                (Functor.mapCone (forget C) (pullbackConeOfLeft f g))).π.app
          j)
  Cone.ext._auto_1
Tactic: fapply Cone.ext
-- 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
⊢ autoParam
    (∀ (j : WalkingCospan),
      (limit.cone (cospan f.base g.base)).π.app j =
        Iso.hom (Iso.refl (limit.cone (cospan f.base g.base)).pt) ≫
          ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
                  (Functor.mapCone (forget C) (pullbackConeOfLeft f g))).π.app
            j)
    Cone.ext._auto_1
have w : ∀ (j : WalkingCospan),
  (limit.cone (cospan f.base g.base)).π.app j =
    𝟙 (Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) j) ≫
      NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) j ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j
Tactic: change ∀ j, _ = 𝟙 _ ≫ _ ≫ _
-- 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
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
      (cospan f.base g.base).obj none)
    ((limit.cone (cospan f.base g.base)).π.app none)
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) none ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none)
have w : Eq (α :=
  Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
    (cospan f.base g.base).obj none)
  (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) none ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none :
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
      (cospan f.base g.base).obj none)
  ((limit.cone (cospan f.base g.base)).π.app none :
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
      (cospan f.base g.base).obj none)
Tactic: symm
-- 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
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.left) ⟶
      (cospan f.base g.base).obj (some WalkingPair.left))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.left) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left))
have w : Eq (α :=
  Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
      (some WalkingPair.left) ⟶
    (cospan f.base g.base).obj (some WalkingPair.left))
  (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.left) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left) :
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.left) ⟶
      (cospan f.base g.base).obj (some WalkingPair.left))
  ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left) :
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.left) ⟶
      (cospan f.base g.base).obj (some WalkingPair.left))
Tactic: symm
-- 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
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.right) ⟶
      (cospan f.base g.base).obj (some WalkingPair.right))
    ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right))
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right))
have w : Eq (α :=
  Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
      (some WalkingPair.right) ⟶
    (cospan f.base g.base).obj (some WalkingPair.right))
  (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right) :
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.right) ⟶
      (cospan f.base g.base).obj (some WalkingPair.right))
  ((limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right) :
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt)
        (some WalkingPair.right) ⟶
      (cospan f.base g.base).obj (some WalkingPair.right))
Tactic: symm
-- 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
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
      (cospan f.base g.base).obj none)
    (NatTrans.app (Cone.π (Functor.mapCone (forget C) (pullbackConeOfLeft f g))) none ≫
        (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
        (cospan f.base g.base).obj none)
    ((limit.cone (cospan f.base g.base)).π.app none :
      Functor.obj (Functor.obj (Functor.const WalkingCospan) (limit.cone (cospan f.base g.base)).pt) none ⟶
        (cospan f.base g.base).obj none)
have w : ((pullbackConeOfLeft f g).fst.base ≫ f.base) ≫ Iso.hom (eqToIso sorry) = pullback.fst f.base g.base ≫ f.base
Tactic: simp only [limit.cone_x, Functor.const_obj_obj, cospan_one, Functor.comp_obj, forget_obj,
          Functor.mapCone_pt, Functor.mapCone_π_app, PullbackCone.condition_one, forget_map,
          comp_base, cospan_left, cospan_right, Functor.comp_map, cospan_map_inl, cospan_map_inr,
          diagramIsoCospan_hom_app, PullbackCone.fst_limit_cone]
-- 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)))
⊢ IsIso (X := pullback f g) (pullback.snd f g)
have this : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
Tactic: haveI := TopCat.snd_iso_of_left_embedding_range_subset hf.base_open.isEmbedding g.base H