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 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
i₁ i₂ : Over j
f : i₁ ⟶ i₂
⊢ Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left (Over.Hom.left f ≫ i₂.hom)) (Z i₂.left i₂.hom)

Tactic:
hstab ..
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
i₁ i₂ : Over j
f : i₁ ⟶ i₂
⊢ Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left (Over.Hom.left f ≫ i₂.hom)) (Z i₂.left i₂.hom)

Tactic:
exact hstab ..
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
⊢ ∃ (s : ↥c.pt), ∀ (i : I) (hij : i ⟶ j), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((c.π.app i) s : ↥(D.obj i))

Tactic:
simpa [Over.forall_iff] using exists_mem_of_isClosed_of_nonempty (Over.forget j ⋙ D) _
    ((Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c).symm hc)
    (fun i ↦ Z i.left i.hom) (fun _ ↦ hZc _ _) (fun _ ↦ hZne _ _) (fun _ ↦ hZcpt _ _)
    (fun {i₁ i₂} f ↦ by dsimp; rw [← Over.w f]; exact hstab ..)

Premises used: CategoryTheory.Functor.Initial.isLimitWhiskerEquiv, CategoryTheory.Functor.comp, CategoryTheory.Over.forget, CategoryTheory.Over.left, AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty, CategoryTheory.Over.forall_iff, Equiv.symm, DFunLike.coe, 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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
by_contra! : ∀ (H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤), False
⊢ ∃ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U = ⊤

Tactic:
by_contra! 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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
j : I
f : j ⟶ i
simp : ¬Eq (α := Set ↥(D.obj j)) (⇑(D.map f) ⁻¹' (↑U : Set ↥(D.obj i))) Set.univ
⊢ Set.Nonempty.{u} (α := ↥(D.obj j)) ((fun (j : I) (f : j ⟶ i) ↦ (↑(D.map f ⁻¹ᵁ U) : Set ↥(D.obj j))ᶜ) j f)

Tactic:
simp only [TopologicalSpace.Opens.map_coe, Set.nonempty_compl, ne_eq]

Premises used: TopologicalSpace.Opens.map_coe, ne_eq, Set.nonempty_compl
-- 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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
j : I
f : j ⟶ i
⊢ ¬Eq (α := Set ↥(D.obj j)) (⇑(D.map f) ⁻¹' (↑U : Set ↥(D.obj i))) Set.univ

Tactic:
SetLike.coe_injective.ne (H j f)

Premises used: Set.Mem, Set.univ, setOf, Function.Injective.ne, SetLike.coe_injective, Set.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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
j : I
f : j ⟶ i
⊢ ¬Eq (α := Set ↥(D.obj j)) (⇑(D.map f) ⁻¹' (↑U : Set ↥(D.obj i))) Set.univ

Tactic:
exact SetLike.coe_injective.ne (H j f)

Premises used: Function.Injective.ne, SetLike.coe_injective
-- 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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
j k : I
fkj : k ⟶ j
fji : j ⟶ i
x : ↥(D.obj k)
hx : ((D.map (fkj ≫ fji)) x : ↥(D.obj i)) ∉ U
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hx : ((D.map fkj ≫ D.map fji) x : ↥(D.obj i)) ∉ U),
    Membership.mem (α := ↥(D.obj j)) (γ := Set ↥(D.obj j))
      ((fun (j : I) (f : j ⟶ i) ↦ (↑(D.map f ⁻¹ᵁ U) : Set ↥(D.obj j))ᶜ) j fji) ((D.map fkj) x : ↥(D.obj j))
⊢ Membership.mem (α := ↥(D.obj j)) (γ := Set ↥(D.obj j))
    ((fun (j : I) (f : j ⟶ i) ↦ (↑(D.map f ⁻¹ᵁ U) : Set ↥(D.obj j))ᶜ) j fji) ((D.map fkj) x : ↥(D.obj j))

Tactic:
rwa [Functor.map_comp] at hx

Premises used: CategoryTheory.Functor.map_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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
obtain :
  ∀ (s : ↥c.pt)
    (hs :
      ∀ (i_1 : I) (hij : i_1 ⟶ i),
        Membership.mem (α := ↥(D.obj i_1)) (↑(D.map hij ⁻¹ᵁ U) : Set ↥(D.obj i_1))ᶜ ((c.π.app i_1) s : ↥(D.obj i_1))),
    False
⊢ False

Tactic:
obtain ⟨s, hs⟩ := exists_mem_of_isClosed_of_nonempty' D c hc (fun j f ↦ (D.map f ⁻¹ᵁ U)ᶜ)
    (fun j f ↦ (D.map f ⁻¹ᵁ U).2.isClosed_compl) (fun j f ↦ by
      simp only [TopologicalSpace.Opens.map_coe, Set.nonempty_compl, ne_eq]
      exact SetLike.coe_injective.ne (H j f))
    (fun j f ↦ (D.map f ⁻¹ᵁ U).2.isClosed_compl.isCompact)
    (fun j k fkj fji x (hx : _ ∉ U) ↦ by rwa [Functor.map_comp] at hx)

Premises used: Compl.compl, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, IsOpen.isClosed_compl, SetLike.coe, IsClosed.isCompact, AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', 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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
i : I
U : (D.obj i).Opens
hU : c.π.app i ⁻¹ᵁ U = ⊤
H : ∀ (j : I) (fji : j ⟶ i), D.map fji ⁻¹ᵁ U ≠ ⊤
s : ↥c.pt
hs :
  ∀ (i_1 : I) (hij : i_1 ⟶ i),
    Membership.mem (α := ↥(D.obj i_1)) (↑(D.map hij ⁻¹ᵁ U) : Set ↥(D.obj i_1))ᶜ ((c.π.app i_1) s : ↥(D.obj i_1))
⊢ s ∉ c.π.app i ⁻¹ᵁ U

Tactic:
simpa using hs i (𝟙 i)

Premises used: CategoryTheory.CategoryStruct.id
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
rw : D.map j.hom ⁻¹ᵁ U ≤ (D.map (Over.Hom.left f) ≫ D.map k.hom) ⁻¹ᵁ U
rw₁ : D.map j.hom ⁻¹ᵁ U ≤ D.map (Over.Hom.left f ≫ k.hom) ⁻¹ᵁ U
rw₂ rw₃ : D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ U
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map (Over.Hom.left f) ⁻¹ᵁ D.map k.hom ⁻¹ᵁ U

Tactic:
rw [← Scheme.Hom.comp_preimage, ← D.map_comp, Over.w f]

Premises used: CategoryTheory.Over.w, AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Functor.map_comp
-- 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
i : I
U : (D.obj i).Opens
j : Over i
⊢ IsOpenImmersion (X := (opensDiagram D i U).obj j) (Y := (Over.forget i ⋙ D).obj j)
    (NatTrans.app { app := fun (j : Over i) ↦ (D.map j.hom ⁻¹ᵁ U).ι, naturality := ⋯ } j)

Tactic:
infer_instance
-- 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
i : I
U : (D.obj i).Opens
j : Over i
rw : c.π.app i ⁻¹ᵁ U ≤ (c.π.app j.left ≫ D.map j.hom) ⁻¹ᵁ U
rw₁ rw₂ : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ U
⊢ c.π.app i ⁻¹ᵁ U ≤ c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ U

Tactic:
rw [← Scheme.Hom.comp_preimage, c.w]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, CategoryTheory.Limits.Cone.w
-- 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 : IsCofiltered I
i : I
U : (D.obj i).Opens
⊢ (Cone.postcompose (opensDiagramι D i U)).obj (opensCone D c i U) ⟶ Cone.whisker (Over.forget i) c

Tactic:
exact { hom := (c.π.app i ⁻¹ᵁ U).ι }
-- 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 : IsCofiltered I
i : I
U : (D.obj i).Opens
j : Over i
⊢ CategoryStruct.comp (Y := Cone.pt (F := Over.forget i ⋙ D) (Cone.whisker (Over.forget i) c))
      (ConeMorphism.hom { hom := (c.π.app i ⁻¹ᵁ U).ι, w := ⋯ } :
        ((Cone.postcompose (opensDiagramι D i U)).obj (opensCone D c i U)).pt ⟶
          Cone.pt (F := Over.forget i ⋙ D) (Cone.whisker (Over.forget i) c))
      (NatTrans.app (Cone.π (Cone.whisker (Over.forget i) c)) j :
        Functor.obj
            (Functor.obj (Functor.const (Over i)) (Cone.pt (F := Over.forget i ⋙ D) (Cone.whisker (Over.forget i) c)))
            j ⟶
          (Over.forget i ⋙ D).obj j) =
    (opensCone D c i U).π.app j ≫ (opensDiagramι D i U).app j

Tactic:
simp
-- 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 : IsCofiltered I
i : I
U : (D.obj i).Opens
j : Over i
⊢ Eq (α := (Cone.pt (F := Over.forget i ⋙ D) (Cone.whisker (Over.forget i) c)).Opens)
    (NatTrans.app (Cone.π (Cone.whisker (Over.forget i) c)) j ⁻¹ᵁ Scheme.Hom.opensRange ((opensDiagramι D i U).app j) :
      (Cone.pt (F := Over.forget i ⋙ D) (Cone.whisker (Over.forget i) c)).Opens)
    (Scheme.Hom.opensRange (X := Functor.obj (Functor.obj (Functor.const (Over i)) (opensCone D c i U).pt) j)
        (ConeMorphism.hom { hom := (c.π.app i ⁻¹ᵁ U).ι, w := ⋯ } :
          ((Cone.postcompose (opensDiagramι D i U)).obj (opensCone D c i U)).pt ⟶
            Cone.pt (F := Over.forget i ⋙ D) (Cone.whisker (Over.forget i) c)) :
      (Cone.pt (F := Over.forget i ⋙ D) (Cone.whisker (Over.forget i) c)).Opens)

Tactic:
simp [← Scheme.Hom.comp_preimage]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
⊢ IsAffineHom ((opensDiagram D i U).map f)

Tactic:
⟨fun V hV ↦ ?_⟩

Premises used: AlgebraicGeometry.IsAffineHom.mk
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
refine :
  ∀ (V : ((opensDiagram D i U).obj k).Opens) (hV : IsAffineOpen V), IsAffineOpen ((opensDiagram D i U).map f ⁻¹ᵁ V)
⊢ IsAffineHom ((opensDiagram D i U).map f)

Tactic:
refine ⟨fun V hV ↦ ?_⟩
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
⊢ IsAffineOpen (X := (↑(D.map j.hom ⁻¹ᵁ U) : Scheme))
    ((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V)

Tactic:
((hV.image_of_isOpenImmersion (D.map k.hom ⁻¹ᵁ U).ι).preimage
          (D.map f.left)).preimage_of_isOpenImmersion
      (D.map j.hom ⁻¹ᵁ U).ι ?_

Premises used: CategoryTheory.Over.Hom.left, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, CategoryTheory.Functor.map, AlgebraicGeometry.IsAffineOpen.preimage_of_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, CategoryTheory.Over.hom, CategoryTheory.Functor.obj, AlgebraicGeometry.IsAffineOpen.preimage
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
h :
  (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme) →
    (opensDiagram D i U).map f ⁻¹ᵁ V = (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V
this : D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ Scheme.Hom.opensRange (D.map j.hom ⁻¹ᵁ U).ι
⊢ IsAffineOpen ((opensDiagram D i U).map f ⁻¹ᵁ V)

Tactic:
convert!
    ((hV.image_of_isOpenImmersion (D.map k.hom ⁻¹ᵁ U).ι).preimage
          (D.map f.left)).preimage_of_isOpenImmersion
      (D.map j.hom ⁻¹ᵁ U).ι ?_

Premises used: CategoryTheory.Over.Hom.left, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, CategoryTheory.Functor.map, AlgebraicGeometry.IsAffineOpen.preimage_of_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, CategoryTheory.Over.hom, CategoryTheory.Functor.obj, AlgebraicGeometry.IsAffineOpen.preimage
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
h :
  ∀ (x : ↥((opensDiagram D i U).obj j)),
    x ∈ (↑((opensDiagram D i U).map f ⁻¹ᵁ V) : Set ↥((opensDiagram D i U).obj j)) ↔
      x ∈
        (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
          Set ↥((opensDiagram D i U).obj j))
⊢ (opensDiagram D i U).map f ⁻¹ᵁ V = (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V

Tactic:
ext x
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))
⊢ x ∈ (↑((opensDiagram D i U).map f ⁻¹ᵁ V) : Set ↥((opensDiagram D i U).obj j)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))

Tactic:
change _ ∈ V ↔ _
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
⊢ Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))

Tactic:
⟨fun h ↦ ⟨⟨(D.map f.left).base x.1, ?_⟩, ?_, rfl⟩, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Over.Hom.left, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, Subtype.mk, And.intro, Iff.intro, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, Subtype.val, DFunLike.coe, rfl
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  ∀
    (h :
      Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
        (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))),
    Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
      ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left)) : ↥(D.obj k.left))
h₁ :
  ∀
    (h :
      Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
        (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))),
    Membership.mem (α := ↥((opensDiagram D i U).obj k)) (↑V : Set ↥((opensDiagram D i U).obj k))
      (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U)
          ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left))) ⋯ :
        ↥(D.map k.hom ⁻¹ᵁ U))
h₂ :
  x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j)) →
    Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
⊢ Membership.mem (α := ↥((opensDiagram D i U).obj k)) V
      (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k)) ↔
    x ∈
      (↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) :
        Set ↥((opensDiagram D i U).obj j))

Tactic:
refine ⟨fun h ↦ ⟨⟨(D.map f.left).base x.1, ?_⟩, ?_, rfl⟩, ?_⟩
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) (↑x : ↥(D.obj j.left)) : ↥(D.obj i))
⊢ Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
    ((D.map (Over.Hom.left f)) (↑x : ↥(D.obj j.left)) : ↥(D.obj k.left))

Tactic:
change (D.map f.left ≫ D.map k.hom).base x.1 ∈ U

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Over.Hom.left, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, Subtype.val, DFunLike.coe, CategoryTheory.Over.hom
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map j.hom) (↑x : ↥(D.obj j.left)) : ↥(D.obj i))
⊢ Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) (↑x : ↥(D.obj j.left)) : ↥(D.obj i))

Tactic:
rw [← D.map_comp, Over.w f]

Premises used: CategoryTheory.Over.w, CategoryTheory.Functor.map_comp
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
⊢ Membership.mem (α := ↥(D.obj i)) U ((D.map j.hom) (↑x : ↥(D.obj j.left)) : ↥(D.obj i))

Tactic:
x.2

Premises used: Set.Mem, setOf, Set.preimage, Subtype.property
-- 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_1 : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
h :
  Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))
⊢ Membership.mem (α := ↥(D.obj i)) U ((D.map j.hom) (↑x : ↥(D.obj j.left)) : ↥(D.obj i))

Tactic:
exact x.2

Premises used: Subtype.property