mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {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:
;

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {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)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso
    ((pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY)

Tactic:
;

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso
    ((pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY =
    pushoutSection ⋯ hUSX hUST ⋯

Tactic:
;

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY =
    pushoutSection ⋯ hUSX hUST ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
i : ↑I
⊢ ↑↑i ≤ ⨆ i ∈ I, ↑i

Tactic:
;

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
i : ↑I
⊢ ↑↑i ≤ ⨆ i ∈ I, ↑i
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
i✝ : ↑I
i : ↥T
⊢ i ∈ ↑↑i✝ → i ∈ ⨆ i ∈ I, ↑i

Tactic:
;

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
i✝ : ↑I
i : ↥T
⊢ i ∈ ↑↑i✝ → i ∈ ⨆ i ∈ I, ↑i
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j : Over i
⊢ IsOpenImmersion ({ app := fun j ↦ (D.map j.hom ⁻¹ᵁ U).ι, naturality := ⋯ }.app j)

Tactic:
;

Goal state after:
I : Type u
inst✝ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
i : I
U : (D.obj i).Opens
j : Over i
⊢ IsOpenImmersion ({ app := fun j ↦ (D.map j.hom ⁻¹ᵁ U).ι, naturality := ⋯ }.app j)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x).universally f

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x).universally f
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij :
  (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map fi)) xi =
    (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map fj)) xj
⊢ ∃ l fli flj x,
    (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map fli)) x = xi ∧
      (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map flj)) x = xj

Tactic:
simp only [Functor.comp_obj, functorOfLocallyDirected_obj, forget_obj, Functor.comp_map,
      functorOfLocallyDirected_map, forget_map, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk] at hxij
    have : 𝒰.f i xi = 𝒰.f j xj := by
      rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
        ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
    obtain ⟨z, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback xi xj this
    obtain ⟨l, gi, gj, y, rfl⟩ := 𝒰.exists_lift_trans_eq z
    refine ⟨l, gi, gj, y, ?_, ?_⟩ <;> simp [← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ diagonal (@Surjective) f ↔ Surjective (pullback.diagonal f)

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ diagonal (@Surjective) f ↔ Surjective (pullback.diagonal f)
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
this :
  ∀ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j),
    pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
        (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ =
      pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
          (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
        iso.inv
⊢ ∃ k hki hkj y,
    (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯)
        y =
      x

Tactic:
obtain ⟨k, hki, hkj, yk, hyk⟩ := 𝒰.exists_lift_trans_eq ((iso.hom ≫ pullback.snd _ _) x)

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.190} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
this :
  ∀ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j),
    pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
        (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ =
      pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
          (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
        iso.inv
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
yk : ↥(𝒰.X k)
hyk :
  (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) yk = (iso.hom ≫ pullback.snd f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) x
⊢ ∃ k hki hkj y,
    (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯)
        y =
      x
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.61} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
x : ↥(pullback ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f j))
⊢ ∃ k hki hkj y,
    (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯)
        y =
      x

Tactic:
dsimp at i j x ⊢
    let iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
        pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
      pullbackRightPullbackFstIso _ _ _ ≪≫ pullback.congrHom pullback.condition rfl ≪≫
        pullbackAssoc ..
    have (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) :
        (pullback.lift
          (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) (by simp) (by simp))
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) (by simp) (by simp))
            (by simp)) =
          pullback.map _ _ _ _ (𝟙 Y) (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) (by simp)) (𝟙 X)
            (by simp) (by simp) ≫ iso.inv := by
      apply pullback.hom_ext <;> apply pullback.hom_ext <;> simp [iso]
    obtain ⟨k, hki, hkj, yk, hyk⟩ := 𝒰.exists_lift_trans_eq ((iso.hom ≫ pullback.snd _ _) x)
    refine ⟨k, hki, hkj, show x ∈ Set.range _ from ?_⟩
    rw [this, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, Pullback.range_map]
    use iso.hom x
    simp only [Hom.id_base, TopCat.hom_id, ContinuousMap.coe_id, Set.range_id, Set.preimage_univ,
      Set.univ_inter, Set.mem_preimage, Set.mem_range, hom_inv_apply, and_true]
    exact ⟨yk, hyk⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
j : I
fj : ∀ {X : I}, X ∈ Finset.image (fun x ↦ i ⟨↑x, ⋯⟩) hsf.toFinset.attach → Nonempty (j ⟶ X)
⊢ ∃ i V, IsCompact ↑V ∧ c.π.app i ⁻¹ᵁ V = sSup s

Tactic:
replace fj : ∀ b : s, j ⟶ i b := fun b ↦ (@fj (i b) (by simpa using ⟨b.1, b.2, rfl⟩)).some

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
j : I
fj : (b : ↑s) → j ⟶ i b
⊢ ∃ i V, IsCompact ↑V ∧ c.π.app i ⁻¹ᵁ V = sSup s
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i : 𝒰.I₀
⊢ IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) ⋯ ≫ 𝒰.f i = 𝟙 (𝒰.X i) ≫ 𝒰.f i

Tactic:
;

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i : 𝒰.I₀
⊢ IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) ⋯ ≫ 𝒰.f i = 𝟙 (𝒰.X i) ≫ 𝒰.f i
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i✝ j✝ k✝ : 𝒰.I₀
hij : i✝ ⟶ j✝
hjk : j✝ ⟶ k✝
⊢ IsOpenImmersion.lift (𝒰.f k✝) (𝒰.f i✝) ⋯ ≫ 𝒰.f k✝ =
    (IsOpenImmersion.lift (𝒰.f j✝) (𝒰.f i✝) ⋯ ≫ IsOpenImmersion.lift (𝒰.f k✝) (𝒰.f j✝) ⋯) ≫ 𝒰.f k✝

Tactic:
;

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i✝ j✝ k✝ : 𝒰.I₀
hij : i✝ ⟶ j✝
hjk : j✝ ⟶ k✝
⊢ IsOpenImmersion.lift (𝒰.f k✝) (𝒰.f i✝) ⋯ ≫ 𝒰.f k✝ =
    (IsOpenImmersion.lift (𝒰.f j✝) (𝒰.f i✝) ⋯ ≫ IsOpenImmersion.lift (𝒰.f k✝) (𝒰.f j✝) ⋯) ≫ 𝒰.f k✝
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
i✝ j✝ : X.directedAffineCover.I₀
⊢ i✝ ≤ j✝ ↔ Hom.opensRange (X.directedAffineCover.f i✝) ≤ Hom.opensRange (X.directedAffineCover.f j✝)

Tactic:
;

Goal state after:
P : MorphismProperty Scheme
X : Scheme
i✝ j✝ : X.directedAffineCover.I₀
⊢ i✝ ≤ j✝ ↔ Hom.opensRange (X.directedAffineCover.f i✝) ≤ Hom.opensRange (X.directedAffineCover.f j✝)
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
i✝ j✝ : X.directedAffineCover.I₀
⊢ i✝ ≤ j✝ ↔ i✝ ≤ j✝

Tactic:
;

Goal state after:
P : MorphismProperty Scheme
X : Scheme
i✝ j✝ : X.directedAffineCover.I₀
⊢ i✝ ≤ j✝ ↔ i✝ ≤ j✝
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (ConcreteCategory.hom ((F ⋙ forget).map fi)) xi = (ConcreteCategory.hom ((F ⋙ forget).map fj)) xj
⊢ ∃ l fli flj x,
    (ConcreteCategory.hom ((F ⋙ forget).map fli)) x = xi ∧ (ConcreteCategory.hom ((F ⋙ forget).map flj)) x = xj

Tactic:
by
    simp only [Functor.comp_obj, Scheme.forget_obj, Functor.comp_map, Scheme.forget_map] at heq
    obtain ⟨l, fli, flj, x, hi, hj⟩ := (G ⋙ Scheme.forget).exists_map_eq_of_isLocallyDirected fi fj
        (s.app i xi) (s.app j xj) <| by
      simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
      dsimp at heq
      rw [← Scheme.Hom.comp_apply, ← s.naturality, Scheme.Hom.comp_apply, heq,
        ← Scheme.Hom.comp_apply, s.naturality]
      simp
    use l, fli, flj
    let e := (hs fli).isoPullback
    obtain ⟨z, h1, h2⟩ := Scheme.Pullback.exists_preimage_pullback xi x hi.symm
    refine ⟨e.inv z, ?_, ?_⟩
    · simp [← h1, ← Scheme.Hom.comp_apply, e]
    · apply H fj
      simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, ← Scheme.Hom.comp_apply,
        Category.assoc, ← Functor.map_comp, show flj ≫ fj = fli ≫ fi by subsingleton]
      dsimp at heq
      simp [e, Functor.map_comp, ← heq, h1]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i✝ j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : D.obj i✝ ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i✝ ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i✝ = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i✝ ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i✝ ≫ a = c.π.app j ≫ b →
      t.app i✝ = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
i : I
⊢ IsIso (D.obj i).toSpecΓ

Tactic:
;

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i✝ j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : D.obj i✝ ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i✝ ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i✝ = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i✝ ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i✝ ≫ a = c.π.app j ≫ b →
      t.app i✝ = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
i : I
⊢ IsIso (D.obj i).toSpecΓ
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁸ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁷ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁶ : IsCofiltered I
inst✝⁵ : ∀ (i : I), IsAffine (D.obj i)
inst✝⁴ : IsAffine c.pt
i✝ j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
a : D.obj i✝ ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i✝ ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝¹ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i✝ = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i✝ ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i✝ ≫ a = c.π.app j ≫ b →
      t.app i✝ = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝ : ∀ (i : I), IsIso (e.app i)
inst : IsIso e
i : I
⊢ IsAffine (Spec Γ(D.obj i, ⊤))

Tactic:
;

Goal state after:
I : Type u
inst✝⁸ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁷ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁶ : IsCofiltered I
inst✝⁵ : ∀ (i : I), IsAffine (D.obj i)
inst✝⁴ : IsAffine c.pt
i✝ j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
a : D.obj i✝ ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i✝ ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝¹ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i✝ = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i✝ ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i✝ ≫ a = c.π.app j ≫ b →
      t.app i✝ = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝ : ∀ (i : I), IsIso (e.app i)
inst : IsIso e
i : I
⊢ IsAffine (Spec Γ(D.obj i, ⊤))