awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
⊢ Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤

Tactic:
have H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤ := by
    rw [Scheme.Hom.comp_preimage, ← top_le_iff]
    exact .trans (by simp) (Scheme.Hom.preimage_mono _ H)
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
⊢ D.map (Over.hom (Over.mk (𝟙 i))) ⁻¹ᵁ U = U

Tactic:
simp
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
⊢ Eq (α :=
    (Functor.obj (C := Over i) (Functor.obj (Functor.const (Over i)) (opensCone D c i U).pt) (Over.mk (𝟙 i))).Opens)
    ((opensCone D c i U).π.app (Over.mk (𝟙 i)) ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq ⋯) ≫ U.ι) ⁻¹ᵁ V) ⊤

Tactic:
simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.comp_base
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
obtain :
  ∀ (j : Over i) (fji : j ⟶ Over.mk (𝟙 i))
    (hj : (opensDiagram D i U).map fji ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq ⋯) ≫ U.ι) ⁻¹ᵁ V = ⊤),
    ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V

Tactic:
obtain ⟨j, fji, hj⟩ := exists_map_eq_top _ _ (isLimitOpensCone D c hc i U) (i := .mk (𝟙 i))
    (((Scheme.isoOfEq _ (by simp)).hom ≫ U.ι) ⁻¹ᵁ V)
    (by simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base])

Premises used: AlgebraicGeometry.isLimitOpensCone, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.isoOfEq, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, AlgebraicGeometry.exists_map_eq_top, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (opensDiagram D i U).map fji ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq ⋯) ≫ U.ι) ⁻¹ᵁ V = ⊤
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V

Tactic:
⟨j.left, j.hom, ?_⟩

Premises used: CategoryTheory.Over.left, Exists.intro, CategoryTheory.Over.hom
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (opensDiagram D i U).map fji ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq ⋯) ≫ U.ι) ⁻¹ᵁ V = ⊤
refine : D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≤ D.map fji ⁻¹ᵁ V

Tactic:
refine ⟨j.left, j.hom, ?_⟩
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (opensDiagram D i U).map fji ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq ⋯) ≫ U.ι) ⁻¹ᵁ V = ⊤
⊢ Eq (α := (↑(D.map j.hom ⁻¹ᵁ U) : Scheme).Opens) ((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left fji) ⁻¹ᵁ V) ⊤

Tactic:
simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base] using hj

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.comp_base
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (opensDiagram D i U).map fji ⁻¹ᵁ (Iso.hom ((D.obj i).isoOfEq ⋯) ≫ U.ι) ⁻¹ᵁ V = ⊤
⊢ Eq (α := (↑(D.map j.hom ⁻¹ᵁ U) : Scheme).Opens) ((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left fji) ⁻¹ᵁ V) ⊤

Tactic:
replace hj : (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map fji.left ⁻¹ᵁ V = ⊤ := by
    simpa [← Scheme.Hom.comp_preimage, -Scheme.Hom.comp_base] using hj
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ D.map (Over.Hom.left fji) ⁻¹ᵁ V
⊢ Over.Hom.left fji = j.hom

Tactic:
simpa using fji.w

Premises used: CategoryTheory.Over.Hom.w
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
H_1 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
H : Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ D.map (Over.Hom.left fji) ⁻¹ᵁ V
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ V

Tactic:
simpa [show fji.left = j.hom by simpa using fji.w] using hj
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
obtain :
  ∀ (j₁ : I) (fj₁i : j₁ ⟶ i) (e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V),
    ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V

Tactic:
obtain ⟨j₁, fj₁i, e₁⟩ := exists_map_preimage_le_map_preimage D c hc hU H.le

Premises used: Eq.le, AlgebraicGeometry.exists_map_preimage_le_map_preimage
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
obtain :
  ∀ (j₂ : I) (fj₂i : j₂ ⟶ i) (e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U),
    ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V

Tactic:
obtain ⟨j₂, fj₂i, e₂⟩ := exists_map_preimage_le_map_preimage D c hc hV H.ge

Premises used: Eq.ge, AlgebraicGeometry.exists_map_preimage_le_map_preimage
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
obtain :
  ∀ (k : I) (fkj₁ : k ⟶ j₁) (fkj₂ : k ⟶ j₂) (e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i),
    ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V

Tactic:
obtain ⟨k, fkj₁, fkj₂, e⟩ := IsCofiltered.cospan fj₁i fj₂i

Premises used: CategoryTheory.IsCofiltered.cospan
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V

Tactic:
⟨k, fkj₁ ≫ fj₁i, le_antisymm ?_ ?_⟩

Premises used: le_antisymm, Exists.intro, CategoryTheory.CategoryStruct.comp
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
refine_1 : D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V
refine_2 : D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = D.map fji ⁻¹ᵁ V

Tactic:
refine ⟨k, fkj₁ ≫ fj₁i, le_antisymm ?_ ?_⟩
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V

Tactic:
simpa only [Scheme.Hom.comp_preimage, Functor.map_comp] using Scheme.Hom.preimage_mono _ e₁

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Functor.map_comp, AlgebraicGeometry.Scheme.Hom.preimage_mono
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
refine_2 : D.map (fkj₂ ≫ fj₂i) ⁻¹ᵁ V ≤ D.map (fkj₂ ≫ fj₂i) ⁻¹ᵁ U
⊢ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U

Tactic:
rw [e]
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
hV : IsCompact (↑V : Set ↥(D.obj i))
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ D.map (fkj₂ ≫ fj₂i) ⁻¹ᵁ V ≤ D.map (fkj₂ ≫ fj₂i) ⁻¹ᵁ U

Tactic:
simpa only [Scheme.Hom.comp_preimage, Functor.map_comp] using Scheme.Hom.preimage_mono _ e₂

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Functor.map_comp, AlgebraicGeometry.Scheme.Hom.preimage_mono
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
⊢ TopologicalSpace.Opens.IsBasis.{u} (α := ↥c.pt)
    {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}

Tactic:
TopologicalSpace.Opens.isBasis_iff_nbhd.mpr fun {U x} hxU ↦ ?_

Premises used: Iff.mpr, TopologicalSpace.Opens.isBasis_iff_nbhd
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
refine :
  ∀ {U : TopologicalSpace.Opens ↥c.pt} {x : ↥c.pt} (hxU : x ∈ U),
    ∃ (U' : TopologicalSpace.Opens ↥c.pt),
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
          {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
          U' ∧
        x ∈ U' ∧ U' ≤ U
⊢ TopologicalSpace.Opens.IsBasis.{u} (α := ↥c.pt)
    {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}

Tactic:
refine TopologicalSpace.Opens.isBasis_iff_nbhd.mpr fun {U x} hxU ↦ ?_

Premises used: Iff.mpr, TopologicalSpace.Opens.isBasis_iff_nbhd
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
obtain :
  ∀ (i : I),
    ∃ (U' : TopologicalSpace.Opens ↥c.pt),
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
          {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
          U' ∧
        x ∈ U' ∧ U' ≤ U
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U

Tactic:
obtain ⟨i⟩ := IsCofiltered.nonempty (C := I)

Premises used: CategoryTheory.IsCofiltered.nonempty
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
obtain :
  ∀ (V : TopologicalSpace.Opens ↥(D.obj i)) (hV : IsAffineOpen V)
    (hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))),
    ∃ (U' : TopologicalSpace.Opens ↥c.pt),
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
          {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
          U' ∧
        x ∈ U' ∧ U' ≤ U
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U

Tactic:
obtain ⟨_, ⟨V, hV : IsAffineOpen V, rfl⟩, hxV, -⟩ :=
    (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (c.π.app i x)) isOpen_univ

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
⊢ ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))

Tactic:
have (j : _) : IsAffine ((opensDiagram D i V).op.obj j).unop := hV.preimage _
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))
⊢ ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i V).obj j)

Tactic:
have (j : _) : IsAffine ((opensDiagram D i V).obj j) := hV.preimage _
-- 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this_1 : ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i V).obj j)
obtain :
  ∀ (r : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V) : Type u))
    (hrU : (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r ≤ U)
    (hxr :
      (↑(Subtype.mk (p := fun (x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) i)) ↦ x ∈ U) x hxU) :
          ↥(((Functor.const I).obj c.pt).obj i)) ∈
        (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r),
    ∃ (U' : TopologicalSpace.Opens ↥c.pt),
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
          {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
          U' ∧
        x ∈ U' ∧ U' ≤ U
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U

Tactic:
obtain ⟨r, hrU, hxr⟩ := IsAffineOpen.exists_basicOpen_le
    (Scheme.isAffine_of_isLimit _ (isLimitOpensCone D c hc i V)) (V := U) ⟨x, hxU⟩ hxV

Premises used: AlgebraicGeometry.isLimitOpensCone, Subtype.mk, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, AlgebraicGeometry.Scheme.isAffine_of_isLimit