awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : IsAffine X
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
S : Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_6 : LocallyOfFiniteType f
inst_7 : IsAffine S
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hS : ∃ (R : CommRingCat.{u}), S = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (f : X ⟶ Spec R) [LocallyOfFiniteType f]
    [IsAffine.{u} (Spec R)] (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f),
    ∃ (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

Tactic:
obtain ⟨R, rfl⟩ := hS

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : IsAffine X
inst_4 : ∀ (i : I), IsAffine.{u} (D.obj i)
inst_5 : IsAffine.{u} c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_6 : LocallyOfFiniteType f
inst_7 : IsAffine.{u} (Spec R)
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} [IsAffine X] (a : D.obj i ⟶ X) (b : D.obj j ⟶ X) (hab : c.π.app i ≫ a = c.π.app j ≫ b)
        (f : X ⟶ Spec R) [LocallyOfFiniteType f] (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f)
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
        ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b
wlog :
  ∀ {X : Scheme.{u}} [IsAffine X] (a : D.obj i ⟶ X) (b : D.obj j ⟶ X) (hab : c.π.app i ≫ a = c.π.app j ≫ b)
    (f : X ⟶ Spec R) [LocallyOfFiniteType f] (ha : t.app i = a ≫ f) (hb : t.app j = b ≫ f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), ∃ (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

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

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

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

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

Tactic:
simpa using this (a ≫ X.isoSpec.hom) (b ≫ X.isoSpec.hom) (by simp [hab]) (X.isoSpec.inv ≫ f)
      (by simp [ha]) (by simp [hb]) ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.isoSpec, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
X : Scheme
inst_6 : IsAffine X
a : D.obj i ⟶ X
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
f : X ⟶ Spec R
inst_7 : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) [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) (f : Spec S ⟶ Spec R) [LocallyOfFiniteType f] (ha : t.app i = a ≫ f)
    (hb : t.app j = b ≫ f), ∃ (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

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
f : Spec S ⟶ Spec R
inst_7 : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
obtain :
  ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)] (ha : t.app i = a ≫ Spec.map φ) (hb : t.app j = b ≫ Spec.map φ),
    ∃ (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

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
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
⊢ ∃ (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

Premises used: CommRingCat, AlgebraicGeometry.Scheme.Spec
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
dsimp : IsIso.{u, u + 1} (X := D.obj i) (D.obj i).toSpecΓ
⊢ IsIso (e.app i)

Tactic:
dsimp [e]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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.{u, u + 1} (X := D.obj i) (D.obj i).toSpecΓ

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
⊢ ∀ (i : I), IsIso (e.app i)

Tactic:
have inst (i) : IsIso (e.app i) := by dsimp [e]; 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 : ∀ (i : I), IsIso (e.app i)
⊢ IsIso e

Tactic:
have inst : IsIso e := NatIso.isIso_of_isIso_app e
-- 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_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
dsimp : IsAffine.{u} (Spec Γ(D.obj i, ⊤))
⊢ IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)

Tactic:
dsimp
-- 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_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} (Spec Γ(D.obj i, ⊤))

Tactic:
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 : IsIso e
⊢ ∀ (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
-- 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)
dsimp : IsAffine.{u} c.pt
⊢ IsAffine.{u} ((Cone.postcompose (asIso e).hom).obj c).pt

Tactic:
dsimp
-- 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} c.pt

Tactic:
infer_instance