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_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 (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))

Tactic:
h
-- 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₁ :
  Eq (α := ↥((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))
    (((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))

Tactic:
convert! h
-- 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))
⊢ Eq (α := ↥(D.obj k.left))
    ((↑(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.obj k.left)) :
      ↥(D.obj k.left))
    ((↑(((opensDiagram D i U).map f) x) : ↥(D.obj k.left)) : ↥(D.obj k.left))

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_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_1 : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
hU :
  Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
    ((D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left)) : ↥(D.obj k.left))
hV :
  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)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
      ↥(D.map k.hom ⁻¹ᵁ U))
⊢ 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)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
      ↥(D.map k.hom ⁻¹ᵁ U))

Tactic:
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_1 : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
hU :
  Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
    ((D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left)) : ↥(D.obj k.left))
hV :
  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)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
      ↥(D.map k.hom ⁻¹ᵁ U))
h :
  Eq (α := ↥((opensDiagram D i U).obj k)) (((opensDiagram D i U).map f) x : ↥((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)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
      ↥(D.map k.hom ⁻¹ᵁ U))
⊢ Membership.mem (α := ↥((opensDiagram D i U).obj k)) V (((opensDiagram D i U).map f) x : ↥((opensDiagram D i U).obj k))

Tactic:
convert! 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_1 : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
hU :
  Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
    ((D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left)) : ↥(D.obj k.left))
hV :
  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)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
      ↥(D.map k.hom ⁻¹ᵁ U))
⊢ Eq (α := ↥(D.obj k.left)) ((↑(((opensDiagram D i U).map f) x) : ↥(D.obj k.left)) : ↥(D.obj k.left))
    ((↑(Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U)
            ((D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU) :
        ↥(D.obj k.left)) :
      ↥(D.obj k.left))

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_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_1 : IsAffineOpen V
e_1 : (opensDiagram D i U).obj j = (↑(D.map j.hom ⁻¹ᵁ U) : Scheme)
x : ↥((opensDiagram D i U).obj j)
hU :
  Membership.mem (α := ↥(D.obj k.left)) (D.map k.hom ⁻¹ᵁ U)
    ((D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left)) : ↥(D.obj k.left))
hV :
  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)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
      ↥(D.map k.hom ⁻¹ᵁ U))
⊢ Eq (α := ↥((opensDiagram D i U).obj k)) (((opensDiagram D i U).map f) x : ↥((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)) ((D.map j.hom ⁻¹ᵁ U).ι x : ↥(D.obj j.left))) hU :
      ↥(D.map k.hom ⁻¹ᵁ U))

Tactic:
exact Subtype.ext (by simp)

Premises used: Subtype.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_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
simp : D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ D.map j.hom ⁻¹ᵁ U
⊢ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ Scheme.Hom.opensRange (D.map j.hom ⁻¹ᵁ U).ι

Tactic:
simp only [opensDiagram_obj, Scheme.Opens.opensRange_ι]

Premises used: AlgebraicGeometry.Scheme.Opens.opensRange_ι, AlgebraicGeometry.opensDiagram_obj
-- 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
x : ↥(D.obj j.left)
y : ↥(D.obj k.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) y : ↥(D.obj i))
h₂ :
  Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁ ∈ (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
⊢ y = (D.map (Over.Hom.left f)) x

Tactic:
congr($e)

Premises used: 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
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
x : ↥(D.obj j.left)
y : ↥(D.obj k.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) y : ↥(D.obj i))
h₂ :
  Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁ ∈ (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
⊢ Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))

Tactic:
obtain rfl : y = (D.map f.left).base x := congr($e)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Over.Hom.left, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.Hom.base, 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
x : ↥(D.obj j.left)
y : ↥(D.obj k.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) y : ↥(D.obj i))
h₂ :
  Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁ ∈ (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
h₃ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
⊢ Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₃ :
      ↥(D.map k.hom ⁻¹ᵁ U))

Tactic:
obtain rfl : y = (D.map f.left).base x := congr($e)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Over.Hom.left, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.Hom.base, 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
x : ↥(D.obj j.left)
y : ↥(D.obj k.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) y : ↥(D.obj i))
h₂ :
  Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁ ∈ (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) y h₁) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
h₃ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
h₄ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₃ :
      ↥(D.map k.hom ⁻¹ᵁ U))
⊢ Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₃ :
          ↥(D.map k.hom ⁻¹ᵁ U)) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))

Tactic:
obtain rfl : y = (D.map f.left).base x := congr($e)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Over.Hom.left, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.Hom.base, 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
x : ↥(D.obj j.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
h₂ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
      ↥(D.map k.hom ⁻¹ᵁ U))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
          ↥(D.map k.hom ⁻¹ᵁ U)) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
⊢ Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) x : ↥(D.obj i))

Tactic:
rw [← Scheme.Hom.comp_apply] at h₁

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- 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
x : ↥(D.obj j.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
h₂ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
      ↥(D.map k.hom ⁻¹ᵁ U))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
          ↥(D.map k.hom ⁻¹ᵁ U)) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
h₃ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) x : ↥(D.obj i))
⊢ Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
      ↥(D.map k.hom ⁻¹ᵁ U))

Tactic:
rw [← Scheme.Hom.comp_apply] at h₁

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- 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
x : ↥(D.obj j.left)
h₁ : Membership.mem (α := ↥(D.obj i)) U ((D.map k.hom) ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left)) : ↥(D.obj i))
h₂ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
      ↥(D.map k.hom ⁻¹ᵁ U))
e :
  Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
          ↥(D.map k.hom ⁻¹ᵁ U)) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))
h₃ : Membership.mem (α := ↥(D.obj i)) U ((D.map (Over.Hom.left f) ≫ D.map k.hom) x : ↥(D.obj i))
h₄ :
  Membership.mem (α := ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) (↑V : Set ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme))
    (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
      ↥(D.map k.hom ⁻¹ᵁ U))
⊢ Eq (α := ↥(D.obj k.left))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
            (↑(↑(D.map k.hom ⁻¹ᵁ U) : Scheme).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom) :
          (a : ↥(↑(D.map k.hom ⁻¹ᵁ U) : Scheme)) → ↥(D.obj k.left))
        (Subtype.mk (p := fun (x : ↥(D.obj k.left)) ↦ x ∈ D.map k.hom ⁻¹ᵁ U) ((D.map (Over.Hom.left f)) x) h₁ :
          ↥(D.map k.hom ⁻¹ᵁ U)) :
      ↥(D.obj k.left))
    ((D.map (Over.Hom.left f)) x : ↥(D.obj k.left))

Tactic:
rw [← Scheme.Hom.comp_apply] at h₁

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- 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
⊢ ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)

Tactic:
have (j : Over i) : CompactSpace ↥((opensDiagram D i U).obj j) :=
    isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage (f := (D.map j.hom)) _ U.2 hU)
-- 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)
rw : LE.le (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) ⊤ ((c.π.app i ⁻¹ᵁ U).ι ⁻¹ᵁ c.π.app i ⁻¹ᵁ V)
⊢ Eq (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) (((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V) ⊤

Tactic:
rw [Scheme.Hom.comp_preimage, ← top_le_iff]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, top_le_iff
-- 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)
⊢ LE.le (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) ⊤ ((c.π.app i ⁻¹ᵁ U).ι ⁻¹ᵁ c.π.app i ⁻¹ᵁ 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 : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace.{u} ↥((opensDiagram D i U).obj j)
⊢ LE.le (α := (↑(c.π.app i ⁻¹ᵁ U) : Scheme).Opens) ⊤ ((c.π.app i ⁻¹ᵁ U).ι ⁻¹ᵁ c.π.app i ⁻¹ᵁ V)

Tactic:
exact .trans (by simp) (Scheme.Hom.preimage_mono _ H)