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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
S : Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
inst_4 : LocallyOfFinitePresentation f
inst_5 : IsAffine S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ 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)
    [LocallyOfFinitePresentation f] [IsAffine.{u} (Spec R)]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_4 : LocallyOfFinitePresentation f
inst_5 : IsAffine.{u} (Spec R)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
        (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f))
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
wlog :
  ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_4 : LocallyOfFinitePresentation f
inst_5 : IsAffine.{u} (Spec R)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
this :
  ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) ((a ≫ X.isoSpec.hom) ≫ X.isoSpec.inv ≫ f)

Tactic:
simp [ha, - Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f : X ⟶ Spec R
inst_4 : LocallyOfFinitePresentation f
inst_5 : IsAffine.{u} (Spec R)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
this :
  ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inr :
  ∀ (i : I) (f_1 : D.obj i ⟶ Spec Γ(X, ⊤))
    (hf : c.π.app i ≫ f_1 = a ≫ X.isoSpec.hom ∧ f_1 ≫ X.isoSpec.inv ≫ f = t.app i),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
obtain ⟨i, f, hf⟩ := this (a ≫ X.isoSpec.hom) (X.isoSpec.inv ≫ f)
      (by simp [ha, - Functor.map_comp]) ⟨_, 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
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f_1 : X ⟶ Spec R
inst_4 : LocallyOfFinitePresentation f_1
inst_5 : IsAffine.{u} (Spec R)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f_1)
this :
  ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : I
f : D.obj i ⟶ Spec Γ(X, ⊤)
hf : c.π.app i ≫ f = a ≫ X.isoSpec.hom ∧ f ≫ X.isoSpec.inv ≫ f_1 = t.app i
⊢ c.π.app i ≫ f ≫ X.isoSpec.inv = a ∧ (f ≫ X.isoSpec.inv) ≫ f_1 = t.app i

Tactic:
simpa [← Iso.comp_inv_eq] using hf

Premises used: CategoryTheory.Iso.comp_inv_eq
-- 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 : IsCofiltered I
inst_2 : IsAffine X
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
f_1 : X ⟶ Spec R
inst_4 : LocallyOfFinitePresentation f_1
inst_5 : IsAffine.{u} (Spec R)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f_1)
this :
  ∀ {X : Scheme.{u}} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : I
f : D.obj i ⟶ Spec Γ(X, ⊤)
hf : c.π.app i ≫ f = a ≫ X.isoSpec.hom ∧ f ≫ X.isoSpec.inv ≫ f_1 = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f_1 = t.app i

Tactic:
exact ⟨i, f ≫ X.isoSpec.inv, by simpa [← Iso.comp_inv_eq] using hf⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
X : Scheme
inst_4 : IsAffine X
a : c.pt ⟶ X
f : X ⟶ Spec R
inst_5 : LocallyOfFinitePresentation f
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) [IsAffine.{u} (Spec S)] (a : c.pt ⟶ Spec S) (f : Spec S ⟶ Spec R)
    [LocallyOfFinitePresentation f] (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

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 : IsCofiltered I
inst_2 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
f : Spec S ⟶ Spec R
inst_5 : LocallyOfFinitePresentation f
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
obtain :
  ∀ (φ : R ⟶ S) [LocallyOfFinitePresentation (Spec.map φ)]
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

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 : IsCofiltered I
inst_2 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
inr :
  ∀
    (this :
      ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
        (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
        (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
        (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
        ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i)
    (hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
wlog :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i

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 : IsCofiltered I
inst_2 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
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 : IsCofiltered I
inst_2 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
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 : IsCofiltered I
inst_2 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
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 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
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 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_7 : ∀ (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 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_7 : ∀ (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 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_7 : ∀ (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 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_7 : ∀ (i : I), IsIso (e.app i)
inst_8 : IsIso e
inst : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
⊢ ((Cone.postcompose (asIso e).hom).obj c).π ≫ inv e ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)

Tactic:
simpa using 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 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_7 : ∀ (i : I), IsIso (e.app i)
inst_8 : IsIso e
inst : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
inr :
  ∀ (i : I) (g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S)
    (hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a) (hg' : g ≫ Spec.map φ = (inv e ≫ t).app i),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i

Tactic:
obtain ⟨i, g, hg, hg'⟩ := this _ _ ((IsLimit.postcomposeHomEquiv (asIso e) c).symm hc)
      (inv e ≫ t) a (by simpa using ha) ⟨D ⋙ Scheme.Γ.rightOp, rfl⟩

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, AlgebraicGeometry.Scheme.Γ, CategoryTheory.Functor.comp, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.Functor.rightOp, Equiv.symm, DFunLike.coe, rfl, CategoryTheory.asIso
-- 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 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_7 : ∀ (i : I), IsIso (e.app i)
inst_8 : IsIso e
inst : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
rwa rwa₁ rwa₂ rwa₃ : (c.π.app i ≫ e.app i) ≫ g = a
⊢ c.π.app i ≫ e.app i ≫ g = a

Tactic:
rwa [← Category.assoc]

Premises used: CategoryTheory.Category.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 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_7 : ∀ (i : I), IsIso (e.app i)
inst_8 : IsIso e
inst : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
⊢ (e.app i ≫ g) ≫ Spec.map φ = t.app i

Tactic:
simp [hg']