awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ (i : I), IsAffine.{u} (D.obj i)
i : I
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop (D.map f)) :
            (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
          s :
        (↑Γ(D.obj j, ⊤) : Type u))
      (0 : (↑Γ(D.obj j, ⊤) : Type u))
have this : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))
Tactic: have : ∀ i, IsAffine (D.op.obj i).unop := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst_3 : CompactSpace.{u} ↥(D.obj i)
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
x : ↥(D.obj i)
⊢ ∃ (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ : x ∈ U) (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (D.map f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) s U ⋯ :
            ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              ((D.obj i).presheaf.obj (Opposite.op U))) :
        (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
have obtain : ∀ (U : TopologicalSpace.Opens ↥(D.obj i)) (hU : IsAffineOpen U) (hxU : x ∈ (↑U : Set ↥(D.obj i))),
  ∃ (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ : x ∈ U) (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (D.map f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) s U sorry :
            ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              ((D.obj i).presheaf.obj (Opposite.op U))) :
        (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
Tactic: obtain ⟨_, ⟨U, hU : IsAffineOpen U, rfl⟩, hxU, -⟩ :=
      (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst_3 : CompactSpace.{u} ↥(D.obj i)
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ (↑U : Set ↥(D.obj i))
⊢ ∃ (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ : x ∈ U) (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (D.map f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) s U ⋯ :
            ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              ((D.obj i).presheaf.obj (Opposite.op U))) :
        (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
have this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
Tactic: have (j : Over i) : IsAffine ((opensDiagram D i U).obj j) := hU.preimage (D.map _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst_3 : CompactSpace.{u} ↥(D.obj i)
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ (↑U : Set ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hj :
  Eq (α := (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensDiagram D i U).map f)) :
          (a : (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
            (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ((Over.forget i ⋙ D).obj (Over.mk (𝟙 i)), ⊤))
                (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i)))) :
              (a : (↑Γ((Over.forget i ⋙ D).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
                (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u))
            s :
          (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) :
      (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
    (0 : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
⊢ Eq (α := (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (D.map j.hom) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) s U ⋯ :
          ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            ((D.obj i).presheaf.obj (Opposite.op U))) :
      (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
have hf : Over.Hom.left f = j.hom
Tactic: have hf : f.left = j.hom := by simpa using Over.w f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst_3 : CompactSpace.{u} ↥(D.obj i)
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
U : (x : ↥(D.obj i)) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : (x : ↥(D.obj i)) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H :
  ∀ (x : ↥(D.obj i)),
    Eq (α := (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj i, U x)) (Scheme.Hom.app (D.map (f x)) (U x)) :
            (a : (↑Γ(D.obj i, U x) : Type u)) → (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) s (U x) ⋯ :
            ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              ((D.obj i).presheaf.obj (Opposite.op (U x)))) :
        (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
      (0 : (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop (D.map f)) :
            (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
          s :
        (↑Γ(D.obj j, ⊤) : Type u))
      (0 : (↑Γ(D.obj j, ⊤) : Type u))
have obtain : ∀ (t : Finset ↥(D.obj i)) (ht : Eq.{u + 1} (α := Set ↥(D.obj i)) (⋃ x ∈ t, (↑(U x) : Set ↥(D.obj i))) ⊤),
  ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop (D.map f)) :
            (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
          s :
        (↑Γ(D.obj j, ⊤) : Type u))
      (0 : (↑Γ(D.obj j, ⊤) : Type u))
Tactic: obtain ⟨t, ht⟩ := CompactSpace.elim_nhds_subcover (U ·) (fun x ↦ (U x).2.mem_nhds (hxU x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (D.map f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
have this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
Tactic: have : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i))) :=
    isCompact_iff_compactSpace.mp (by simpa)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (D.map f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
have H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
Tactic: have H : (D.map (𝟙 _) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U := by simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
⊢ Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj (Over.mk (𝟙 i)), ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤))
            (Scheme.Hom.appTop ((opensCone D c i U).π.app (Over.mk (𝟙 i)))) :
          (a : (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj (Over.mk (𝟙 i)), ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(D.obj i, U)) (Y := Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤))
                ((D.obj i).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
            s :
          (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u)) :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj (Over.mk (𝟙 i)), ⊤) : Type u))
    ((CommRingCat.Hom.hom (c.pt.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))) : Type u)) →
            (↑(c.pt.presheaf.obj (Opposite.op ((c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
              (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u)) :
      (↑(c.pt.presheaf.obj (Opposite.op ((c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
have dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp [Scheme.Opens.toScheme_presheaf_obj]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  Eq (α := (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier)
            (Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) ⋯)) :
          (a : (↑Γ((↑(D.map (𝟙 i) ⁻¹ᵁ U) : Scheme), ⊤) : Type u)) → (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(D.obj i, U)) (Y := Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤))
                ((D.obj i).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
            s :
          (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u)) :
      (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
    (0 : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (D.map f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
have refine : Eq (α := (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.app (D.map (Over.Hom.left f)) U) :
        (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
      s :
    (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
  (0 : (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
Tactic: refine ⟨j.left, f.left, ?_⟩