awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
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 : 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)
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
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 : 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)
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 : 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) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
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 (goal)
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.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
have 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
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⟩
-- 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 : 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
⊢ c.π.app i ≫ e.app i ≫ g = a
have rwa : (c.π.app i ≫ e.app i) ≫ g = a
Tactic: rwa [← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_5 : ∀ (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
have obtain : ∀ (D : I ⥤ CommRingCatᵒᵖ) (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c)
  [∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)] (t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R))
  (a : c.pt ⟶ Spec S) (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)),
  ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
Tactic: obtain ⟨D, rfl⟩ := hD
Cleared hypotheses: D, c, hc, inst_5, t, a, ha, hD
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
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
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
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)) ⋯
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
have obtain : ∀ (t : Functor.obj (Functor.const Iᵒᵖ) R ⟶ D.leftOp)
  (ha :
    c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
      CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)),
  ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
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 :
  c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
have inr : ∀
  (this :
    ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S)
      (ha :
        c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
          CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
      (hc' : ∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
      ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
        c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i)
  (hc' : ¬∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
  ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
Tactic: wlog hc' : ∃ c' : Cocone D.leftOp, c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c') generalizing c
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
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 :
  c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
inr :
  ∀
    (this :
      ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S)
        (ha :
          c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
            CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
        (hc' : ∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
        ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
          c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i)
    (hc' : ¬∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
have wlog : ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S)
  (ha :
    c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
      CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
  (hc' : ∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
  ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
Tactic: wlog hc' : ∃ c' : Cocone D.leftOp, c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c') generalizing c
Cleared hypotheses: c, hc, a, ha
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
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 :
  c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S)
    (ha :
      c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
        CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hc' : ∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
have inst : IsAffine.{u} c.pt
Tactic: have inst : IsAffine c.pt := isAffine_of_isLimit _ hc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst_1 : Category.{u, u} I
inst_2 : IsCofiltered I
R : CommRingCat
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
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 :
  c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S)
    (ha :
      c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
        CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hc' : ∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
inst : IsAffine.{u} c.pt
e' : (D ⋙ Scheme.Spec).op ⋙ Γ ≅ D.leftOp := D.leftOp.isoWhiskerLeft SpecΓIdentity
c' : Cone D := coneOfCoconeLeftOp ((Cocone.precompose e'.inv).obj (Γ.mapCocone c.op))
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
have inst₁ : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop ((D ⋙ Scheme.Spec).op.obj i))
Tactic: have inst : ∀ i, IsAffine ((D ⋙ Scheme.Spec).op.obj i).unop := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst_1 : Category.{u, u} I
inst_2 : IsCofiltered I
R : CommRingCat
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
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 :
  c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S)
    (ha :
      c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
        CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hc' : ∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
inst_7 : IsAffine.{u} c.pt
e' : (D ⋙ Scheme.Spec).op ⋙ Γ ≅ D.leftOp := D.leftOp.isoWhiskerLeft SpecΓIdentity
c' : Cone D := coneOfCoconeLeftOp ((Cocone.precompose e'.inv).obj (Γ.mapCocone c.op))
inst : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop ((D ⋙ Scheme.Spec).op.obj i))
⊢ (Scheme.Spec.mapCone c').π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) ((Iso.inv c.pt.isoSpec ≫ a) ≫ Spec.map φ)
have w : ∀ (i : I),
  ((Scheme.Spec.mapCone c').π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i =
    NatTrans.app (CategoryTheory.Functor.map (Functor.const I) ((Iso.inv c.pt.isoSpec ≫ a) ≫ Spec.map φ)) i
Tactic: ext i