awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
e : Iso (C := I ⥤ Scheme) (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec)
  (Functor.obj (Functor.const I) (Spec R)) :=
  NatIso.ofComponents
    (fun (x : I) ↦ Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x)) ⋯
t : Functor.obj (Functor.const Iᵒᵖ) R ⟶ D.leftOp
ha : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
⊢ Spec.map (a ≫ (coconeLeftOpOfCone (liftLimit hc)).ι.app (Opposite.op i)) =
    Spec.map (b ≫ (coconeLeftOpOfCone (liftLimit hc)).ι.app (Opposite.op j))
have simp : Spec.map ((liftLimit hc).π.app i).unop ≫ Spec.map a = Spec.map ((liftLimit hc).π.app j).unop ≫ Spec.map b
Tactic: simp only [coconeLeftOpOfCone_pt, Functor.const_obj_obj,
        Functor.leftOp_obj, coconeLeftOpOfCone_ι_app, Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
e : Iso (C := I ⥤ Scheme) (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec)
  (Functor.obj (Functor.const I) (Spec R)) :=
  NatIso.ofComponents
    (fun (x : I) ↦ Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x)) ⋯
t : Functor.obj (Functor.const Iᵒᵖ) R ⟶ D.leftOp
ha : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
have obtain : ∀ (k : Iᵒᵖ) (hik : Opposite.op i ⟶ k) (hjk : Opposite.op j ⟶ k) (H : a ≫ D.leftOp.map hik = b ≫ D.leftOp.map hjk),
  ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
Tactic: obtain ⟨k, hik, hjk, H⟩ := (HasRingHomProperty.Spec_iff.mp ‹LocallyOfFiniteType (Spec.map φ)›)
    |>.essFiniteType.exists_comp_map_eq_of_isColimit _ D.leftOp t _
    (coconeLeftOpOfCone (liftLimit hc))
    (isColimitCoconeLeftOpOfCone _ (liftedLimitIsLimit _))
    a (Spec.map_injective (by simpa using ha.symm))
    b (Spec.map_injective (by simpa using hb.symm))
    (Spec.map_injective (by
      simp only [coconeLeftOpOfCone_pt, Functor.const_obj_obj,
        Functor.leftOp_obj, coconeLeftOpOfCone_ι_app, Spec.map_comp]
      simp only [← Scheme.Spec_map, ← liftedLimitMapsToOriginal_hom_π, Category.assoc, hab]))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
⊢ ∃ (i' : I) (hii' : i' ⟶ A.i),
    Eq (α := Set ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
      ∅
have by_contra! : ∀
  (h :
    ∀ (i' : I) (hii' : i' ⟶ A.i),
      Set.Nonempty (α := ↥(D.obj i'))
        (⇑(D.map hii' ≫ pullback.lift A.a A.b sorry) ⁻¹'
          (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
⊢ False
have hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
Tactic: have hZ (i') (hii' : i' ⟶ A.i) : IsClosed (Z i' hii') :=
    (W.isOpen.isClosed_compl).preimage <| Scheme.Hom.continuous _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
⊢ False
have refine : Membership.mem (α := ↥(pullback.diagonalObj f)) (γ := Set ↥(pullback.diagonalObj f))
  (Set.range (ι := ↥X) ⇑(pullback.diagonal f))
  ((D.map (𝟙 A.i) ≫ pullback.lift A.a A.b sorry) ((A.c.π.app A.i) s : ↥(D.obj A.i)) : ↥(pullback f f))
Tactic: refine hs A.i (𝟙 A.i) (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
⊢ Membership.mem (α := ↥(pullback.diagonalObj f)) (γ := Set ↥(pullback.diagonalObj f))
    (Set.range (ι := ↥X) ⇑(pullback.diagonal f))
    ((D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s : ↥(D.obj A.i)) : ↥(pullback f f))
have h₁ : Eq (α := ↥(pullback.diagonalObj f)) ((pullback.diagonal f) ((A.c.π.app A.i ≫ A.a) s : ↥X) : ↥(pullback.diagonalObj f))
  ((D.map (𝟙 A.i) ≫ pullback.lift A.a A.b sorry) ((A.c.π.app A.i) s : ↥(D.obj A.i)) : ↥(pullback f f))
Tactic: use (A.c.π.app A.i ≫ A.a) s
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const I) A.c.pt) A.i ⟶ pullback.diagonalObj f)
    (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯)
have h₀ : CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (pullback.fst f f) =
  CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ pullback.lift A.a A.b sorry) (pullback.fst f f)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
h₀ :
  CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (pullback.fst f f) =
    CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) (pullback.fst f f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const I) A.c.pt) A.i ⟶ pullback.diagonalObj f)
    (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯)
have h₁ : CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (pullback.snd f f) =
  CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ pullback.lift A.a A.b sorry) (pullback.snd f f)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
⊢ Eq (α := ↥(pullback.diagonalObj f)) ((pullback.diagonal f) ((A.c.π.app A.i ≫ A.a) s : ↥X) : ↥(pullback.diagonalObj f))
    ((D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s : ↥(D.obj A.i)) : ↥(pullback f f))
have H : Eq (α := Functor.obj (Functor.obj (Functor.const I) A.c.pt) A.i ⟶ pullback.diagonalObj f)
  (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (A.c.π.app A.i ≫ pullback.lift A.a A.b sorry)
Tactic: have H : A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f =
      A.c.π.app A.i ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb) := by ext <;> simp [hab]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
have this : ∀ (i : I), IsAffineHom (c.π.app i)
Tactic: have := isAffineHom_π_app _ _ hc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀) ↦
      ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover,
    h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
have choose : ∀ (k : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → I)
  (hki' :
    (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → k j ⟶ A.i')
  (heq :
    ∀ (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)),
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
        (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b),
  ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
Tactic: choose k hki' heq using A.exists_eq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀) ↦
      ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover,
    h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → I
hki' : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → k j ⟶ A.i'
heq :
  ∀ (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := OpenCover.finiteSubcover A.𝒰D
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
have inl : ∀ (h : IsEmpty.{u + 1} ↥(D.obj A.i')), ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
Tactic: rcases isEmpty_or_nonempty (D.obj A.i') with h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀) ↦
      ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover,
    h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → I
hki' : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → k j ⟶ A.i'
heq :
  ∀ (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := OpenCover.finiteSubcover A.𝒰D
inl : ∀ (h : IsEmpty.{u + 1} ↥(D.obj A.i')), ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
have inr : ∀ (h : Nonempty.{u + 1} ↥(D.obj A.i')), ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
Tactic: rcases isEmpty_or_nonempty (D.obj A.i') with h | h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀) ↦
      ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover,
    h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → I
hki' : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → k j ⟶ A.i'
heq :
  ∀ (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := OpenCover.finiteSubcover A.𝒰D
h : Nonempty.{u + 1} ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun (i : 𝒰Df.I₀) ↦ k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i')))) Finset.univ
o : 𝒰Df.I₀ := Nonempty.some ⋯
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
have ho : k (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ∈ O
Tactic: have ho : k (A.𝒰D.idx o.1) ∈ O := by
    simp [O]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
o : I := IsCofiltered.min i j
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have obtain : ∀ (k : I) (hik : k ⟶ IsCofiltered.min i j)
  (heq : D.map hik ≫ D.map (IsCofiltered.minToLeft i j) ≫ a = D.map hik ≫ D.map (IsCofiltered.minToRight i j) ≫ b),
  ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
Tactic: obtain ⟨k, hik, heq⟩ := Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType D t f c hc
    (D.map (IsCofiltered.minToLeft i j) ≫ a) (D.map (IsCofiltered.minToRight i j) ≫ b)
    (by simp [← ha])
    (by simp [← hb]) (by simpa)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
o : I := IsCofiltered.min i j
k : I
hik : k ⟶ IsCofiltered.min i j
heq : D.map hik ≫ D.map (IsCofiltered.minToLeft i j) ≫ a = D.map hik ≫ D.map (IsCofiltered.minToRight i j) ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have h : D.map (hik ≫ IsCofiltered.minToLeft i j) ≫ a = D.map (hik ≫ IsCofiltered.minToRight i j) ≫ b
Tactic: use k, hik ≫ IsCofiltered.minToLeft i j, hik ≫ IsCofiltered.minToRight i j
-- 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 : 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))
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))
have dsimp : ∀ (i : Iᵒᵖ), IsAffine.{u} (D.obj (Opposite.unop i))
Tactic: dsimp