awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddCommMonoid A
s : Multiset (WithConv A)
⊢ s.sum.ofConv = (Multiset.map ofConv s).sum

Tactic:
map_multiset_sum (WithConv.addEquiv _) _

Premises used: map_multiset_sum, WithConv.addEquiv
-- Module: Mathlib.Algebra.WithConv
Goal:
A : Type u_2
inst : AddCommMonoid A
s : Multiset A
⊢ toConv s.sum = (Multiset.map toConv s).sum

Tactic:
map_multiset_sum (WithConv.addEquiv _).symm _

Premises used: map_multiset_sum, WithConv.addEquiv, AddEquiv.symm
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : AddCommMonoid A
inst_1 : Semiring R
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
f : A ≃ₗ[R] B
x : WithConv A
⊢ Eq.{u_3 + 1} (α := WithConv B) ((congrLinearEquiv f : (a : WithConv A) → WithConv B) x : WithConv B)
    (toConv ((f : (a : A) → B) x.ofConv) : WithConv B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : AddCommMonoid A
inst_1 : Semiring R
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
f : A ≃ₗ[R] B
⊢ (congrLinearEquiv f).symm = congrLinearEquiv f.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, WithConv.congrLinearEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : AddCommMonoid A
inst_1 : Semiring R
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
f : A ≃ₗ[R] B
x : WithConv B
⊢ Eq.{u_2 + 1} (α := WithConv A) (((congrLinearEquiv f).symm : (a : WithConv B) → WithConv A) x : WithConv A)
    (toConv ((f.symm : (a : B) → A) x.ofConv) : WithConv A)

Tactic:
simp
-- Module: Mathlib.Algebra.WithConv
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : AddCommMonoid A
inst_1 : Semiring R
inst_2 : Module R A
inst_3 : AddCommMonoid B
inst_4 : Module R B
f : A ≃ₗ[R] B
⊢ (congrLinearEquiv f).toEquiv = WithConv.congr f.toEquiv

Tactic:
rfl

Premises used: Equiv.trans, LinearEquiv.toEquiv, WithConv.congr, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
⊢ IsIso (ΓSpec.adjunction.unit.app X)

Tactic:
@IsAffine.affine X _

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.Scheme.toSpecΓ, AlgebraicGeometry.IsAffine.affine
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
⊢ X.isoSpec.hom ≫ Spec.map (Hom.appTop f) = f ≫ Y.isoSpec.hom

Tactic:
simp only [isoSpec, asIso_hom, Scheme.toSpecΓ_naturality]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.asIso_hom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₁ : (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₂ : X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₃ : f ≫ Y.toSpecΓ ≫ Y.isoSpec.inv = f
rw₄ : f ≫ Y.toSpecΓ ≫ (asIso Y.toSpecΓ).inv = f
rw₅ : f ≫ Y.toSpecΓ ≫ inv Y.toSpecΓ = f
rw₆ : f ≫ 𝟙 Y = f
rw₇ rw₈ : f = f
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f

Tactic:
rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.asIso_inv, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.asIso_hom, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
⊢ X.toSpecΓ ≫ X.isoSpec.inv = 𝟙 X

Tactic:
X.isoSpec.hom_inv_id

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
⊢ X.isoSpec.inv ≫ X.toSpecΓ = 𝟙 (Spec Γ(X, ⊤))

Tactic:
X.isoSpec.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, AlgebraicGeometry.Scheme.isoSpec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
⊢ Scheme.Spec.essImage X ↔ IsAffine X

Tactic:
⟨fun h => ⟨Functor.essImage.unit_isIso h⟩,
    fun _ => ΓSpec.adjunction.mem_essImage_of_unit_isIso _⟩

Premises used: AlgebraicGeometry.IsAffine.mk, AlgebraicGeometry.ΓSpec.adjunction, CategoryTheory.Functor.essImage.unit_isIso, Iff.intro, CategoryTheory.Adjunction.mem_essImage_of_unit_isIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : AffineScheme
⊢ IsAffine.{u} (X.obj (P := Scheme.Spec.essImage))

Tactic:
⟨Functor.essImage.unit_isIso X.property⟩

Premises used: AlgebraicGeometry.IsAffine.mk, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.essImage.unit_isIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCatᵒᵖ
⊢ IsAffine.{u_1} (Scheme.Spec.obj R)

Tactic:
AlgebraicGeometry.isAffine_affineScheme ⟨_, Scheme.Spec.obj_mem_essImage R⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, AlgebraicGeometry.Spec, CategoryTheory.Functor.obj_mem_essImage, AlgebraicGeometry.Scheme.Spec, AlgebraicGeometry.isAffine_affineScheme
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
⊢ IsAffine.{u_1} (Spec R)

Tactic:
AlgebraicGeometry.isAffine_affineScheme ⟨_, Scheme.Spec.obj_mem_essImage (op R)⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, AlgebraicGeometry.Spec, CategoryTheory.Functor.obj_mem_essImage, AlgebraicGeometry.Scheme.Spec, AlgebraicGeometry.isAffine_affineScheme, Opposite.op
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
h : IsAffine Y
rw : ∀ (h : Scheme.Spec.essImage Y), Scheme.Spec.essImage X
⊢ IsAffine X

Tactic:
rw [← essImage_Spec] at h ⊢

Premises used: AlgebraicGeometry.essImage_Spec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X

Tactic:
Functor.essImage.ofIso (asIso f).symm h

Premises used: CategoryTheory.Functor.essImage.ofIso, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X

Tactic:
exact Functor.essImage.ofIso (asIso f).symm h

Premises used: CategoryTheory.Functor.essImage.ofIso, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ IsAffine X ↔ IsAffine Y

Tactic:
⟨fun _ ↦ .of_isIso (inv f), fun _ ↦ .of_isIso f⟩

Premises used: AlgebraicGeometry.IsAffine.of_isIso, Iff.intro, CategoryTheory.inv
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
⊢ (Spec R).isoSpec = Scheme.Spec.mapIso (ΓSpecIso R).op

Tactic:
Iso.ext (SpecMap_ΓSpecIso_hom R).symm

Premises used: AlgebraicGeometry.SpecMap_ΓSpecIso_hom, Eq.symm, CategoryTheory.Iso.ext
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
⊢ Iso.hom (Spec R).isoSpec = Spec.map (ΓSpecIso R).hom

Tactic:
(SpecMap_ΓSpecIso_hom R).symm

Premises used: AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.toSpecΓ, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
⊢ Iso.inv (Spec R).isoSpec = Spec.map (ΓSpecIso R).inv

Tactic:
congr($(isoSpec_Spec R).inv)

Premises used: congrArg, id, AlgebraicGeometry.Scheme.isoSpec_Spec, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
inst : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
rw : f ≫ Y.toSpecΓ = g ≫ Y.toSpecΓ
rw₁ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f) = g ≫ Y.toSpecΓ
rw₂ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f) = X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g)
rw₃ rw₄ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g) = X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g)
⊢ f = g

Tactic:
rw [← cancel_mono Y.toSpecΓ, Scheme.toSpecΓ_naturality, Scheme.toSpecΓ_naturality, e]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.AffineCover.{u_1, u} P S
i : 𝒰.I₀ (P := P)
⊢ IsAffine.{u} (𝒰.cover (P := P).X i)

Tactic:
inferInstanceAs <| IsAffine (Spec _)

Premises used: _private.0.AlgebraicGeometry.instIsAffineXSchemeCover._proof_1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
⊢ ∀ (i : I), IsIso (α.app i)

Tactic:
have (i : _) : IsIso (α.app i) := IsAffine.affine
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this : ∀ (i : I), IsIso (α.app i)
⊢ IsIso α

Tactic:
have : IsIso α := NatIso.isIso_of_isIso_app α
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this : IsIso α
suffices : PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp
⊢ PreservesLimit D Scheme.Γ.rightOp

Tactic:
suffices PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp from
    preservesLimit_of_iso_diagram _ (asIso α).symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this : IsIso α
have :
  ∀ (this : CreatesLimitsOfSize.{v, w, u, u, u + 1, u + 1} Scheme.Spec),
    PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp
⊢ PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp

Tactic:
have := monadicCreatesLimits.{v, w} Scheme.Spec.{u}
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this_2 : IsIso α
this : CreatesLimitsOfSize.{v, w, u, u, u + 1, u + 1} Scheme.Spec
suffices : PreservesLimit (D ⋙ Scheme.Γ.rightOp) (Scheme.Spec ⋙ Scheme.Γ.rightOp)
⊢ PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp

Tactic:
suffices PreservesLimit (D ⋙ Scheme.Γ.rightOp) (Scheme.Spec ⋙ Scheme.Γ.rightOp) from
    preservesLimit_comp_of_createsLimit _ _
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this_2 : IsIso α
this : CreatesLimitsOfSize.{v, w, u, u, u + 1, u + 1} Scheme.Spec
⊢ PreservesLimit (D ⋙ Scheme.Γ.rightOp) (Scheme.Spec ⋙ Scheme.Γ.rightOp)

Tactic:
preservesLimit_of_natIso _ (NatIso.op Scheme.SpecΓIdentity)

Premises used: CategoryTheory.Limits.preservesLimit_of_natIso, AlgebraicGeometry.Scheme.SpecΓIdentity, CategoryTheory.NatIso.op
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this_2 : IsIso α
this : CreatesLimitsOfSize.{v, w, u, u, u + 1, u + 1} Scheme.Spec
⊢ PreservesLimit (D ⋙ Scheme.Γ.rightOp) (Scheme.Spec ⋙ Scheme.Γ.rightOp)

Tactic:
exact preservesLimit_of_natIso _ (NatIso.op Scheme.SpecΓIdentity)

Premises used: CategoryTheory.Limits.preservesLimit_of_natIso, AlgebraicGeometry.Scheme.SpecΓIdentity, CategoryTheory.NatIso.op
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Schemeᵒᵖ
inst_1 : ∀ (i : I), IsAffine.{u} (unop (D.obj i))
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (D.leftOp.obj i)

Tactic:
have (i : _) : IsAffine (D.leftOp.obj i) := Functor.leftOp_obj D _ ▸ inferInstance
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Schemeᵒᵖ
inst_1 : ∀ (i : I), IsAffine.{u} (unop (D.obj i))
this : ∀ (i : Iᵒᵖ), IsAffine.{u} (D.leftOp.obj i)
⊢ PreservesColimit D Scheme.Γ

Tactic:
preservesColimit_of_rightOp D Scheme.Γ

Premises used: AlgebraicGeometry.Scheme.Γ, CategoryTheory.Limits.preservesColimit_of_rightOp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Schemeᵒᵖ
inst_1 : ∀ (i : I), IsAffine.{u} (unop (D.obj i))
this : ∀ (i : Iᵒᵖ), IsAffine.{u} (D.leftOp.obj i)
⊢ PreservesColimit D Scheme.Γ

Tactic:
exact preservesColimit_of_rightOp D Scheme.Γ

Premises used: AlgebraicGeometry.Scheme.Γ, CategoryTheory.Limits.preservesColimit_of_rightOp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ Spec.Full

Tactic:
Functor.Full.toEssImage _

Premises used: AlgebraicGeometry.AffineScheme, CategoryTheory.Functor.Full.toEssImage, AlgebraicGeometry.AffineScheme.Spec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ Spec.Faithful

Tactic:
Functor.Faithful.toEssImage _

Premises used: CategoryTheory.Functor.Faithful.toEssImage, AlgebraicGeometry.AffineScheme, AlgebraicGeometry.AffineScheme.Spec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ Spec.EssSurj

Tactic:
Functor.EssSurj.toEssImage (F := _)

Premises used: CategoryTheory.Functor.EssSurj.toEssImage, AlgebraicGeometry.AffineScheme, AlgebraicGeometry.AffineScheme.Spec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ forgetToScheme.Full

Tactic:
inferInstanceAs Scheme.Spec.essImage.ι.Full

Premises used: _private.0.AlgebraicGeometry.AffineScheme.forgetToScheme_full._proof_1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ forgetToScheme.Faithful

Tactic:
inferInstanceAs Scheme.Spec.essImage.ι.Faithful

Premises used: _private.0.AlgebraicGeometry.AffineScheme.forgetToScheme_faithful._proof_1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ Γ.rightOp.IsEquivalence

Tactic:
equivCommRingCat.isEquivalence_functor

Premises used: Quiver.Hom.op, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Functor.rightOp, AlgebraicGeometry.AffineScheme, AlgebraicGeometry.AffineScheme.equivCommRingCat
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ Γ.rightOp.op.IsEquivalence

Tactic:
equivCommRingCat.op.isEquivalence_functor

Premises used: CategoryTheory.Functor.op, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Equivalence.op, CategoryTheory.Equivalence.isEquivalence_functor, AlgebraicGeometry.AffineScheme.equivCommRingCat
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ Γ.IsEquivalence

Tactic:
inferInstanceAs (Γ.{u}.rightOp.op ⋙ (opOpEquivalence _).functor).IsEquivalence

Premises used: _private.0.AlgebraicGeometry.AffineScheme.ΓIsEquiv._proof_1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ HasColimits AffineScheme

Tactic:
haveI := Adjunction.has_limits_of_equivalence.{u} Γ.{u}
  Adjunction.has_colimits_of_equivalence.{u} (opOpEquivalence AffineScheme.{u}).inverse

Premises used: CategoryTheory.opOpEquivalence, AlgebraicGeometry.AffineScheme, CategoryTheory.Adjunction.has_colimits_of_equivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ HasColimitsOfSize.{u, u, u, u + 1} AffineSchemeᵒᵖ

Tactic:
haveI := Adjunction.has_colimits_of_equivalence Γ.{u}
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
this : HasColimitsOfSize.{u, u, u, u + 1} AffineSchemeᵒᵖ
⊢ HasLimits.{u, u + 1} AffineSchemeᵒᵖᵒᵖ

Tactic:
haveI : HasLimits AffineScheme.{u}ᵒᵖᵒᵖ := Limits.hasLimits_op_of_hasColimits
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
this_1 : HasColimitsOfSize.{u, u, u, u + 1} AffineSchemeᵒᵖ
this : HasLimits.{u, u + 1} AffineSchemeᵒᵖᵒᵖ
⊢ HasLimits AffineScheme

Tactic:
Adjunction.has_limits_of_equivalence (opOpEquivalence AffineScheme.{u}).inverse

Premises used: CategoryTheory.Adjunction.has_limits_of_equivalence, CategoryTheory.opOpEquivalence, AlgebraicGeometry.AffineScheme, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
this_1 : HasColimitsOfSize.{u, u, u, u + 1} AffineSchemeᵒᵖ
this : HasLimits.{u, u + 1} AffineSchemeᵒᵖᵒᵖ
⊢ HasLimits AffineScheme

Tactic:
exact Adjunction.has_limits_of_equivalence (opOpEquivalence AffineScheme.{u}).inverse
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ PreservesLimits Γ.rightOp

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
apply :
  PreservesLimitsOfSize.{u_1, u_1, u_1, u_1, u_1 + 1, u_1 + 1}
    ((equivCommRingCat.functor ⋙ equivCommRingCat.inverse) ⋙ forgetToScheme)
⊢ PreservesLimits forgetToScheme

Tactic:
apply +allowSynthFailures @preservesLimits_of_natIso _ _ _ _ _ _
    (Functor.isoWhiskerRight equivCommRingCat.unitIso forgetToScheme).symm

Premises used: CategoryTheory.Equivalence.unitIso, AlgebraicGeometry.AffineScheme.forgetToScheme, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight, AlgebraicGeometry.AffineScheme.equivCommRingCat, CategoryTheory.Limits.preservesLimits_of_natIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
⊢ PreservesLimits (equivCommRingCat.functor ⋙ Scheme.Spec)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
Y : Scheme
U : (↑Y.affineOpens : Type u)
⊢ IsAffine.{u} (↑(↑U : Y.Opens) : Scheme)

Tactic:
U.property

Premises used: Set.Mem, setOf, AlgebraicGeometry.IsAffineOpen, AlgebraicGeometry.Scheme.affineOpens, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
inst : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (Scheme.Hom.opensRange f)

Tactic:
.of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.IsAffineOpen, AlgebraicGeometry.Scheme.ofRestrict, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
inst : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
refine : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥(Y.restrict ⋯)) ⇑(Y.ofRestrict ⋯))
⊢ IsAffineOpen (Scheme.Hom.opensRange f)

Tactic:
refine .of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
inst : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥(Y.restrict ⋯)) ⇑(Y.ofRestrict ⋯))

Tactic:
Subtype.range_val.symm

Premises used: Set.Mem, setOf, Subtype.range_val, Set.range, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
inst : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥(Y.restrict ⋯)) ⇑(Y.ofRestrict ⋯))

Tactic:
exact Subtype.range_val.symm

Premises used: Subtype.range_val, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
⊢ IsAffineOpen (Scheme.Hom.opensRange (𝟙 X))

Tactic:
isAffineOpen_opensRange (𝟙 X)

Premises used: AlgebraicGeometry.isAffineOpen_opensRange, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
h : ⊤ = Scheme.Hom.opensRange (𝟙 X)
⊢ IsAffineOpen.{u_1} (X := X) ⊤

Tactic:
convert! isAffineOpen_opensRange (𝟙 X)

Premises used: AlgebraicGeometry.isAffineOpen_opensRange, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
h : (↑⊤ : Set ↥X) = (↑(Scheme.Hom.opensRange (𝟙 X)) : Set ↥X)
⊢ ⊤ = Scheme.Hom.opensRange (𝟙 X)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
⊢ (↑⊤ : Set ↥X) = (↑(Scheme.Hom.opensRange (𝟙 X)) : Set ↥X)

Tactic:
Set.range_id.symm

Premises used: Set.univ, setOf, Set.range_id, Set.range, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
⊢ (↑⊤ : Set ↥X) = (↑(Scheme.Hom.opensRange (𝟙 X)) : Set ↥X)

Tactic:
exact Set.range_id.symm

Premises used: Set.range_id, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
obtain :
  ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ X)
    (hf :
      IsOpenImmersion f ∧
        Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)),
    ∃ (W : X.Opens), IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ (↑U : Set ↥X)
⊢ ∃ (W : X.Opens), IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ (↑U : Set ↥X)

Tactic:
obtain ⟨R, f, hf⟩ := AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset hxU

Premises used: AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
R : CommRingCat
f : Spec R ⟶ X
hf :
  IsOpenImmersion f ∧
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
⊢ ∃ (W : X.Opens), IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ (↑U : Set ↥X)

Tactic:
⟨Scheme.Hom.opensRange f (H := hf.1),
    ⟨AlgebraicGeometry.isAffineOpen_opensRange f (H := hf.1), hf.2.1, hf.2.2⟩⟩

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.isAffineOpen_opensRange, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
R : CommRingCat
f : Spec R ⟶ X
hf :
  IsOpenImmersion f ∧
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
⊢ ∃ (W : X.Opens), IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ (↑U : Set ↥X)

Tactic:
exact ⟨Scheme.Hom.opensRange f (H := hf.1),
    ⟨AlgebraicGeometry.isAffineOpen_opensRange f (H := hf.1), hf.2.1, hf.2.2⟩⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
x : ↥X
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X) (_ : IsOpenImmersion f) (y : ↥(Spec R)), f y = x

Tactic:
⟨X.affineOpenCover.X _, X.affineOpenCover.f _, inferInstance, X.affineOpenCover.covers x⟩

Premises used: inferInstance, AlgebraicGeometry.Scheme.AffineCover.f, AlgebraicGeometry.Scheme.AffineCover.covers, AlgebraicGeometry.Scheme.affineOpenCover, Exists.intro, AlgebraicGeometry.Scheme.AffineCover.X
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
i : X.affineCover.I₀
⊢ IsAffine.{u_1} (X.affineCover.X i)

Tactic:
isAffine_Spec _

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.isAffine_Spec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
𝒰 : AffineOpenCover.{u_2, u_1} X
i : 𝒰.I₀ (P := IsOpenImmersion)
⊢ IsAffine.{u_1} (𝒰.openCover.X i)

Tactic:
inferInstanceAs (IsAffine (Spec (𝒰.X i)))

Premises used: _private.0.AlgebraicGeometry.Scheme.isAffine_affineOpenCover._proof_1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : CompactSpace.{u_1} ↥X
𝒰 : Scheme.OpenCover.{u_2, u_1} X
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u_1} (𝒰.X i)
i : 𝒰.finiteSubcover.I₀
⊢ IsAffine.{u_1} (𝒰.finiteSubcover.X i)

Tactic:
inferInstanceAs (IsAffine (𝒰.X _))

Premises used: _private.0.AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover._proof_1