awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_2 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_3 : IsCofiltered I
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_6 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_7 : IsAffine.{u} (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_8 : 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.{u} ↥(D.obj i)]
    [∀ (i : I), IsAffine.{u} (D.obj i)] [IsAffine.{u} c.pt] (t : D ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b) (ha : t.app i = a ≫ Spec.map φ)
    (hb : t.app j = b ≫ Spec.map φ) (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_9 : ∀ (i : I), IsIso (e.app i)
inst_10 : IsIso e
inst : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
⊢ IsAffine.{u} ((Cone.postcompose (asIso e).hom).obj c).pt

Tactic:
have inst : IsAffine ((Cone.postcompose (asIso e).hom).obj c).pt := by
      dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_2 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_3 : IsCofiltered I
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_6 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_7 : IsAffine.{u} (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_8 : 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.{u} ↥(D.obj i)]
    [∀ (i : I), IsAffine.{u} (D.obj i)] [IsAffine.{u} c.pt] (t : D ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b) (ha : t.app i = a ≫ Spec.map φ)
    (hb : t.app j = b ≫ Spec.map φ) (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_9 : ∀ (i : I), IsIso (e.app i)
inst_10 : IsIso e
inst_11 : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
inst : IsAffine.{u} ((Cone.postcompose (asIso e).hom).obj c).pt
⊢ ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ (inv e).app i ≫ a =
    ((Cone.postcompose (asIso e).hom).obj c).π.app j ≫ (inv e).app j ≫ b

Tactic:
simp [hab]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_2 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_3 : IsCofiltered I
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_6 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_7 : IsAffine.{u} (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_8 : 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.{u} ↥(D.obj i)]
    [∀ (i : I), IsAffine.{u} (D.obj i)] [IsAffine.{u} c.pt] (t : D ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b) (ha : t.app i = a ≫ Spec.map φ)
    (hb : t.app j = b ≫ Spec.map φ) (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_9 : ∀ (i : I), IsIso (e.app i)
inst_10 : IsIso e
inst_11 : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
inst : IsAffine.{u} ((Cone.postcompose (asIso e).hom).obj c).pt
⊢ (inv e ≫ t).app i = ((inv e).app i ≫ a) ≫ Spec.map φ

Tactic:
simp [ha]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_2 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_3 : IsCofiltered I
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_6 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_7 : IsAffine.{u} (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_8 : 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.{u} ↥(D.obj i)]
    [∀ (i : I), IsAffine.{u} (D.obj i)] [IsAffine.{u} c.pt] (t : D ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b) (ha : t.app i = a ≫ Spec.map φ)
    (hb : t.app j = b ≫ Spec.map φ) (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_9 : ∀ (i : I), IsIso (e.app i)
inst_10 : IsIso e
inst_11 : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
inst : IsAffine.{u} ((Cone.postcompose (asIso e).hom).obj c).pt
⊢ (inv e ≫ t).app j = ((inv e).app j ≫ b) ≫ Spec.map φ

Tactic:
simp [hb]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_2 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_3 : IsCofiltered I
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_6 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_7 : IsAffine.{u} (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_8 : 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.{u} ↥(D.obj i)]
    [∀ (i : I), IsAffine.{u} (D.obj i)] [IsAffine.{u} c.pt] (t : D ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b) (ha : t.app i = a ≫ Spec.map φ)
    (hb : t.app j = b ≫ Spec.map φ) (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_9 : ∀ (i : I), IsIso (e.app i)
inst_10 : IsIso e
inst_11 : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
inst : IsAffine.{u} ((Cone.postcompose (asIso e).hom).obj c).pt
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j),
    (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map hik ≫ (inv e).app i ≫ a =
      (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map hjk ≫ (inv e).app j ≫ b

Tactic:
have := this (D ⋙ Scheme.Γ.rightOp ⋙ Scheme.Spec) ((Cone.postcompose (asIso e).hom).obj c)
      ((IsLimit.postcomposeHomEquiv (asIso e) c).symm hc) (inv e ≫ t)
      ((inv e).app _ ≫ a) ((inv e).app _ ≫ b) (by simp [hab]) (by simp [ha]) (by simp [hb])
      ⟨D ⋙ Scheme.Γ.rightOp, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_2 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_3 : IsCofiltered I
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_6 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_7 : IsAffine.{u} (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_8 : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this_1 :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace.{u} ↥(D.obj i)]
    [∀ (i : I), IsAffine.{u} (D.obj i)] [IsAffine.{u} c.pt] (t : D ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b) (ha : t.app i = a ≫ Spec.map φ)
    (hb : t.app j = b ≫ Spec.map φ) (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_9 : ∀ (i : I), IsIso (e.app i)
inst_10 : IsIso e
inst_11 : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
inst : IsAffine.{u} ((Cone.postcompose (asIso e).hom).obj c).pt
this :
  ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j),
    (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map hik ≫ (inv e).app i ≫ a =
      (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map hjk ≫ (inv e).app j ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (inv e).app k ≫ D.map hik ≫ a = (inv e).app k ≫ D.map hjk ≫ b

Tactic:
simp_rw [(inv e).naturality_assoc] at this

Premises used: CategoryTheory.inv, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_2 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_3 : IsCofiltered I
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_6 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_7 : IsAffine.{u} (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_8 : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this_1 :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace.{u} ↥(D.obj i)]
    [∀ (i : I), IsAffine.{u} (D.obj i)] [IsAffine.{u} c.pt] (t : D ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b) (ha : t.app i = a ≫ Spec.map φ)
    (hb : t.app j = b ≫ Spec.map φ) (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_9 : ∀ (i : I), IsIso (e.app i)
inst_10 : IsIso e
inst_11 : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
inst : IsAffine.{u} ((Cone.postcompose (asIso e).hom).obj c).pt
this : ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (inv e).app k ≫ D.map hik ≫ a = (inv e).app k ≫ D.map hjk ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b

Tactic:
simpa using this
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_6 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_7 : IsAffine.{u} c.pt
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
obtain :
  ∀ (D : I ⥤ CommRingCatᵒᵖ) (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c)
    [∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)] [∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)]
    [IsAffine.{u} c.pt] (t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : (D ⋙ Scheme.Spec).obj i ⟶ Spec S) (b : (D ⋙ Scheme.Spec).obj j ⟶ Spec S) (hab : c.π.app i ≫ a = c.π.app j ≫ b)
    (ha : t.app i = a ≫ Spec.map φ) (hb : t.app j = b ≫ Spec.map φ),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ a = (D ⋙ Scheme.Spec).map hjk ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b

Tactic:
obtain ⟨D, rfl⟩ := hD

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : (D ⋙ Scheme.Spec).obj i ⟶ Spec S
b : (D ⋙ Scheme.Spec).obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
obtain :
  ∀ (a : S ⟶ Opposite.unop (D.obj i)) (hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ b)
    (ha : t.app i = Spec.map a ≫ Spec.map φ),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ a = (D ⋙ Scheme.Spec).map hjk ≫ b

Tactic:
obtain ⟨a, rfl⟩ := Spec.map_surjective a

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
b : (D ⋙ Scheme.Spec).obj j ⟶ Spec S
hb : t.app j = b ≫ Spec.map φ
a : S ⟶ Opposite.unop (D.obj i)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ b
ha : t.app i = Spec.map a ≫ Spec.map φ
obtain :
  ∀ (b : S ⟶ Opposite.unop (D.obj j)) (hb : t.app j = Spec.map b ≫ Spec.map φ)
    (hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j),
      (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ b

Tactic:
obtain ⟨b, rfl⟩ := Spec.map_surjective b

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : S ⟶ Opposite.unop (D.obj i)
ha : t.app i = Spec.map a ≫ Spec.map φ
b : S ⟶ Opposite.unop (D.obj j)
hb : t.app j = Spec.map b ≫ Spec.map φ
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
⊢ ∀ {X Y : I} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) X ⟶
        Functor.obj (Functor.obj (Functor.const I) (Spec R)) Y)
      (CategoryTheory.Functor.map (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) f ≫
        Iso.hom
          ((fun (x : I) ↦
              (Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x) :
                Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x ≅
                  Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x))
            Y))
      (Iso.hom
          ((fun (x : I) ↦
              (Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x) :
                Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x ≅
                  Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x))
            X) ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const I) (Spec R)) f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : S ⟶ Opposite.unop (D.obj i)
ha : t.app i = Spec.map a ≫ Spec.map φ
b : S ⟶ Opposite.unop (D.obj j)
hb : t.app j = Spec.map b ≫ Spec.map φ
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
e : Iso (C := I ⥤ Scheme) (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec)
  (Functor.obj (Functor.const I) (Spec R)) :=
  NatIso.ofComponents
    (fun (x : I) ↦ Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x)) ⋯
x x_1 : Iᵒᵖ
f : x ⟶ x_1
⊢ Eq (α := Spec (D.leftOp.obj x_1) ⟶ Spec (Functor.obj (Functor.obj (Functor.const Iᵒᵖ) R) x))
    (Spec.map
      (CategoryTheory.Functor.map (Functor.obj (Functor.const Iᵒᵖ) R) f ≫
        (fun (i : Iᵒᵖ) ↦
            (Spec.preimage (t.app (Opposite.unop i)) :
              Functor.obj (Functor.obj (Functor.const Iᵒᵖ) R) i ⟶ D.leftOp.obj i))
          x_1))
    (Spec.map
      ((fun (i : Iᵒᵖ) ↦
            (Spec.preimage (t.app (Opposite.unop i)) :
              Functor.obj (Functor.obj (Functor.const Iᵒᵖ) R) i ⟶ D.leftOp.obj i))
          x ≫
        D.leftOp.map f))

Tactic:
simpa using (t.naturality f.unop).symm

Premises used: Quiver.Hom.unop, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : S ⟶ Opposite.unop (D.obj i)
ha : t.app i = Spec.map a ≫ Spec.map φ
b : S ⟶ Opposite.unop (D.obj j)
hb : t.app j = Spec.map b ≫ Spec.map φ
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
e : Iso (C := I ⥤ Scheme) (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec)
  (Functor.obj (Functor.const I) (Spec R)) :=
  NatIso.ofComponents
    (fun (x : I) ↦ Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x)) ⋯
w :
  ∀ (x : I),
    t.app x =
      NatTrans.app
        (Functor.whiskerRight
            (NatTrans.rightOp { app := fun (i : Iᵒᵖ) ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ })
            Scheme.Spec ≫
          e.hom)
        x
⊢ t =
    Functor.whiskerRight
        (NatTrans.rightOp { app := fun (i : Iᵒᵖ) ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ })
        Scheme.Spec ≫
      e.hom

Tactic:
ext : 2
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : S ⟶ Opposite.unop (D.obj i)
ha : t.app i = Spec.map a ≫ Spec.map φ
b : S ⟶ Opposite.unop (D.obj j)
hb : t.app j = Spec.map b ≫ Spec.map φ
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
e : Iso (C := I ⥤ Scheme) (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec)
  (Functor.obj (Functor.const I) (Spec R)) :=
  NatIso.ofComponents
    (fun (x : I) ↦ Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x)) ⋯
obtain :
  ∀ (t : Functor.obj (Functor.const Iᵒᵖ) R ⟶ D.leftOp)
    (ha : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ)
    (hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j),
      (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b

Tactic:
obtain ⟨t, rfl⟩ : ∃ t' : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp,
      t = Functor.whiskerRight (NatTrans.rightOp t') Scheme.Spec ≫ e.hom :=
    ⟨⟨fun i ↦ Spec.preimage (t.app i.unop), fun _ _ f ↦ Spec.map_injective
      (by simpa using (t.naturality f.unop).symm)⟩, by ext : 2; simp [e]⟩

Premises used: Opposite, CategoryTheory.Functor.const, CategoryTheory.Functor.leftOp, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
e : Iso (C := I ⥤ Scheme) (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec)
  (Functor.obj (Functor.const I) (Spec R)) :=
  NatIso.ofComponents
    (fun (x : I) ↦ Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x)) ⋯
t : Functor.obj (Functor.const Iᵒᵖ) R ⟶ D.leftOp
ha : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
have :
  ∀ (this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j),
      (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b

Tactic:
have := monadicCreatesLimits Scheme.Spec