awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_4 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_5 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_6 : 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_7 : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
inr :
  ∀
    (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),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have wlog : ∀ (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
Tactic: wlog hD : ∃ D' : I ⥤ CommRingCatᵒᵖ, D = D' ⋙ Scheme.Spec generalizing D
Cleared hypotheses: D, c, hc, inst_1, inst_3, inst_4, t, a, b, hab, ha, hb
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_4 : IsAffine.{u} c.pt
i_1 j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_5 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_6 : IsAffine.{u} (Spec S)
a : D.obj i_1 ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i_1 ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst_7 : LocallyOfFiniteType (Spec.map φ)
ha : t.app i_1 = 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_1 ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i_1 ≫ a = c.π.app j ≫ b)
    (ha : t.app i_1 = a ≫ Spec.map φ) (hb : t.app j = b ≫ Spec.map φ)
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i_1) (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
i : I
⊢ IsIso (e.app i)
have dsimp : IsIso.{u, u + 1} (X := D.obj i) (D.obj i).toSpecΓ
Tactic: dsimp [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_4 : IsAffine.{u} c.pt
i j : I
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_5 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_6 : 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_7 : 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
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have inst : ∀ (i : I), IsIso (e.app i)
Tactic: have inst (i) : IsIso (e.app i) := by dsimp [e]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
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 : ∀ (i : I), IsIso (e.app i)
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have inst₁ : IsIso e
Tactic: have inst : IsIso e := NatIso.isIso_of_isIso_app e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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_1 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_1 ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i_1 ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst_8 : LocallyOfFiniteType (Spec.map φ)
ha : t.app i_1 = 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_1 ⟶ Spec S) (b : D.obj j ⟶ Spec S) (hab : c.π.app i_1 ≫ a = c.π.app j ≫ b)
    (ha : t.app i_1 = a ≫ Spec.map φ) (hb : t.app j = b ≫ Spec.map φ)
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (k : I) (hik : k ⟶ i_1) (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 : IsIso e
i : I
⊢ IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
have dsimp : IsAffine.{u} (Spec Γ(D.obj i, ⊤))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
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 : IsIso e
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have inst₁ : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
Tactic: have inst (i) : IsAffine ((D ⋙ Scheme.Γ.rightOp ⋙ Scheme.Spec).obj i) := by
      dsimp; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
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)
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have inst₁ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
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.map hik ≫ a = D.map hjk ≫ b
have 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
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⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
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), D.map hik ≫ a = D.map hjk ≫ b
have 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
Tactic: simp_rw [(inv e).naturality_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
have 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
Tactic: obtain ⟨D, rfl⟩ := hD
Cleared hypotheses: D, c, hc, inst_5, inst_6, inst_7, t, a, b, hab, ha, hb, hD
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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 φ
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ a = (D ⋙ Scheme.Spec).map hjk ≫ b
have 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
Tactic: obtain ⟨a, rfl⟩ := Spec.map_surjective a
Cleared hypotheses: a, hab, ha
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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 φ
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ b
have 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
Tactic: obtain ⟨b, rfl⟩ := Spec.map_surjective b
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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)) ⋯
⊢ t =
    Functor.whiskerRight
        (NatTrans.rightOp { app := fun (i : Iᵒᵖ) ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ })
        Scheme.Spec ≫
      e.hom
have w : ∀ (x : I),
  t.app x =
    NatTrans.app
      (Functor.whiskerRight
          (NatTrans.rightOp { app := fun (i : Iᵒᵖ) ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := sorry })
          Scheme.Spec ≫
        e.hom)
      x
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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)) ⋯
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
have 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
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]⟩
Cleared hypotheses: t, ha, hb
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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 φ
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
have 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
Tactic: have := monadicCreatesLimits Scheme.Spec