awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
⊢ Set.range (ι := ↥(D.obj A.i')) ⇑A.g ⊆
    (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))

Tactic:
simpa [ExistsHomHomCompEqCompAux.hii', g] using A.exists_index.choose_spec.choose_spec

Premises used: Exists.choose_spec, AlgebraicGeometry.ExistsHomHomCompEqCompAux.g, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, AlgebraicGeometry.ExistsHomHomCompEqCompAux.hii'
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
⊢ ∀ (i : I), IsAffineHom (c.π.app i)

Tactic:
have := isAffineHom_π_app _ _ hc
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
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
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b

Tactic:
choose k hki' heq using A.exists_eq

Premises used: AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
inr : ∀ (h : Nonempty.{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

Tactic:
rcases isEmpty_or_nonempty (D.obj A.i') with h | h

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, isEmpty_or_nonempty, AlgebraicGeometry.ExistsHomHomCompEqCompAux.i', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 : IsEmpty.{u + 1} ↥(D.obj A.i')
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b

Tactic:
⟨A.i', A.hii', isInitialOfIsEmpty.hom_ext _ _⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, AlgebraicGeometry.isInitialOfIsEmpty, AlgebraicGeometry.ExistsHomHomCompEqCompAux.i', AlgebraicGeometry.ExistsHomHomCompEqCompAux.hii', Exists.intro
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 : IsEmpty.{u + 1} ↥(D.obj A.i')
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b

Tactic:
exact ⟨A.i', A.hii', isInitialOfIsEmpty.hom_ext _ _⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ∈ O

Tactic:
simp [O]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ∈ O

Tactic:
have ho : k (A.𝒰D.idx o.1) ∈ O := by
    simp [O]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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_1 : I
a b : D.obj i_1 ⟶ X
ha : t.app i_1 = a ≫ f
hb : t.app i_1 = b ≫ f
hab : c.π.app i_1 ≫ a = c.π.app i_1 ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i_1, 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 ⋯
ho : k (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ∈ O
i : 𝒰Df.I₀
⊢ k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ∈ O

Tactic:
simp [O]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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_1 : I
a b : D.obj i_1 ⟶ X
ha : t.app i_1 = a ≫ f
hb : t.app i_1 = b ≫ f
hab : c.π.app i_1 ≫ a = c.π.app i_1 ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i_1, 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 ⋯
ho : k (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ∈ O
i : 𝒰Df.I₀
⊢ A.i' ∈ O

Tactic:
simp [O]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
⊢ Eq (α := D.obj (IsCofiltered.min i j) ⟶ Functor.obj (Functor.obj (Functor.const I) S) (IsCofiltered.min i j))
    (t.app (IsCofiltered.min i j)) ((D.map (IsCofiltered.minToLeft i j) ≫ a) ≫ f)

Tactic:
simp [← ha]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
⊢ Eq (α := D.obj (IsCofiltered.min i j) ⟶ Functor.obj (Functor.obj (Functor.const I) S) (IsCofiltered.min i j))
    (t.app (IsCofiltered.min i j)) ((D.map (IsCofiltered.minToRight i j) ≫ b) ≫ f)

Tactic:
simp [← hb]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const I) c.pt) (IsCofiltered.min i j) ⟶ X)
    (c.π.app (IsCofiltered.min i j) ≫ D.map (IsCofiltered.minToLeft i j) ≫ a)
    (c.π.app (IsCofiltered.min i j) ≫ D.map (IsCofiltered.minToRight i j) ≫ b)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
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
⊢ ∃ (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)

Premises used: AlgebraicGeometry.Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType, CategoryTheory.Functor.map, CategoryTheory.IsCofiltered.minToRight, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsCofiltered.minToLeft
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
h : D.map (hik ≫ IsCofiltered.minToLeft i j) ≫ a = D.map (hik ≫ IsCofiltered.minToRight i j) ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b

Tactic:
use k, hik ≫ IsCofiltered.minToLeft i j, hik ≫ IsCofiltered.minToRight i j

Premises used: CategoryTheory.IsCofiltered.minToRight, CategoryTheory.IsCofiltered.minToLeft
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
⊢ D.map (hik ≫ IsCofiltered.minToLeft i j) ≫ a = D.map (hik ≫ IsCofiltered.minToRight i j) ≫ b

Tactic:
simpa using heq
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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))
dsimp : ∀ (i : Iᵒᵖ), IsAffine.{u} (D.obj (Opposite.unop i))
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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} (D.obj (Opposite.unop i))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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))

Tactic:
have : ∀ i, IsAffine (D.op.obj i).unop := by dsimp; infer_instance