awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
rw :
  Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of S))
    (Iso.hom (pullbackSpecIso R S T) ≫
      Iso.inv (pullbackSpecIso R S T) ≫
        pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
rw₁ rw₂ :
  Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of S))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
⊢ Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of S))
    (Iso.hom (pullbackSpecIso R S T) ≫ Spec.map (ofHom includeLeftRingHom))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))

Tactic:
rw [← pullbackSpecIso_inv_fst, Iso.hom_inv_id_assoc]

Premises used: AlgebraicGeometry.pullbackSpecIso_inv_fst, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of S))
    (Iso.hom (pullbackSpecIso R S T) ≫ Spec.map (ofHom (algebraMap S (S ⊗[R] T))))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))

Tactic:
pullbackSpecIso_hom_fst ..

Premises used: Algebra.TensorProduct.includeLeftRingHom, AlgebraicGeometry.pullbackSpecIso_hom_fst, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
rw :
  Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of T))
    (Iso.hom (pullbackSpecIso R S T) ≫
      Iso.inv (pullbackSpecIso R S T) ≫
        pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
    (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
rw₁ rw₂ :
  Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of T))
    (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
    (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
⊢ Iso.hom (pullbackSpecIso R S T) ≫ Spec.map (ofHom (↑includeRight : T →+* S ⊗[R] T)) =
    pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))

Tactic:
rw [← pullbackSpecIso_inv_snd, Iso.hom_inv_id_assoc]

Premises used: AlgebraicGeometry.pullbackSpecIso_inv_snd, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of R))
    (Iso.hom (pullbackSpecIso R S T) ≫ Spec.map (ofHom (algebraMap R (S ⊗[R] T))))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))) ≫
      Spec.map (ofHom (algebraMap R S)))

Tactic:
simp [Algebra.TensorProduct.algebraMap_def]

Premises used: Algebra.TensorProduct.algebraMap_def
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
A B C P : CommRingCat
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ P
inr : C ⟶ P
h : IsPushout f g inl inr
⊢ IsPullback (Spec.map inl) (Spec.map inr) (Spec.map f) (Spec.map g)

Tactic:
IsPullback.map Scheme.Spec h.op.flip

Premises used: AlgebraicGeometry.Spec, Quiver.Hom.unop, AlgebraicGeometry.Spec.map, AlgebraicGeometry.Scheme.Spec, CategoryTheory.IsPullback.flip, CategoryTheory.IsPushout.op, CategoryTheory.IsPullback.map
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
h : IsPushout (P := pushout f g) f g (pushout.inl f g) (pushout.inr f g)
⊢ IsPullback (P := Spec (pushout f g)) (Spec.map (pushout.inl f g)) (Spec.map (pushout.inr f g)) (Spec.map f)
    (Spec.map g)

Tactic:
apply isPullback_SpecMap_of_isPushout

Premises used: AlgebraicGeometry.isPullback_SpecMap_of_isPushout
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
⊢ IsPushout (P := pushout f g) f g (pushout.inl f g) (pushout.inr f g)

Tactic:
IsPushout.of_hasPushout f g

Premises used: CategoryTheory.IsPushout.of_hasPushout
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
⊢ IsPushout (P := pushout f g) f g (pushout.inl f g) (pushout.inr f g)

Tactic:
exact IsPushout.of_hasPushout f g

Premises used: CategoryTheory.IsPushout.of_hasPushout
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h₀ :
  Eq (α := Spec (of S) ⟶ Spec (of S))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
      (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
      (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
h₁ :
  Eq (α := Spec (of S) ⟶ Spec (of S))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
      (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
      (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
⊢ Eq (α := Spec (of S) ⟶ pullback.diagonalObj (X := Spec (of S)) (Y := Spec (of R)) (Spec.map (ofHom (algebraMap R S))))
    (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
    (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h₀ :
  Spec.map (𝟙 (of S)) =
    Spec.map (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom) (ofHom (↑(lmul' R) : S ⊗[R] S →+* S)))
⊢ Eq (α := Spec (of S) ⟶ Spec (of S))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
      (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
      (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))

Tactic:
simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
    AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.diagonal_snd, AlgebraicGeometry.pullbackSpecIso_inv_snd, AlgebraicGeometry.Spec.map_id, CategoryTheory.Limits.pullback.diagonal_fst, AlgebraicGeometry.pullbackSpecIso_inv_fst, AlgHom.toRingHom_eq_coe, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h₁ :
  Spec.map (𝟙 (of S)) =
    Spec.map
      (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
        (ofHom (↑(lmul' R) : S ⊗[R] S →+* S)))
⊢ Eq (α := Spec (of S) ⟶ Spec (of S))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
      (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
      (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))

Tactic:
simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
    AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.diagonal_snd, AlgebraicGeometry.pullbackSpecIso_inv_snd, AlgebraicGeometry.Spec.map_id, CategoryTheory.Limits.pullback.diagonal_fst, AlgebraicGeometry.pullbackSpecIso_inv_fst, AlgHom.toRingHom_eq_coe, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h₀ :
  𝟙 (of S) = CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom) (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))
⊢ Spec.map (𝟙 (of S)) =
    Spec.map (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom) (ofHom (↑(lmul' R) : S ⊗[R] S →+* S)))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h₀ :
  ∀ (x : (↑(of S) : Type u)),
    Eq (α := (↑(of S) : Type u))
      ((Hom.hom (𝟙 (of S)) : (a : (↑(of S) : Type u)) → (↑(of S) : Type u)) x : (↑(of S) : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom)
                (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))) :
            (a : (↑(of S) : Type u)) → (↑(of S) : Type u))
          x :
        (↑(of S) : Type u))
⊢ 𝟙 (of S) = CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom) (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : (↑(of S) : Type u)
h₀ : x = (lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] 1)
⊢ Eq (α := (↑(of S) : Type u))
    ((Hom.hom (𝟙 (of S)) : (a : (↑(of S) : Type u)) → (↑(of S) : Type u)) x : (↑(of S) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom)
              (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))) :
          (a : (↑(of S) : Type u)) → (↑(of S) : Type u))
        x :
      (↑(of S) : Type u))

Tactic:
change x = Algebra.TensorProduct.lmul' R (S := S) (x ⊗ₜ[R] 1)

Premises used: Algebra.TensorProduct.lmul', TensorProduct.tmul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : (↑(of S) : Type u)
⊢ x = (lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] 1)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h₁ :
  𝟙 (of S) =
    CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
      (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))
⊢ Spec.map (𝟙 (of S)) =
    Spec.map
      (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
        (ofHom (↑(lmul' R) : S ⊗[R] S →+* S)))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h₁ :
  ∀ (x : (↑(of S) : Type u)),
    Eq (α := (↑(of S) : Type u))
      ((Hom.hom (𝟙 (of S)) : (a : (↑(of S) : Type u)) → (↑(of S) : Type u)) x : (↑(of S) : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
                (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))) :
            (a : (↑(of S) : Type u)) → (↑(of S) : Type u))
          x :
        (↑(of S) : Type u))
⊢ 𝟙 (of S) =
    CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
      (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : (↑(of S) : Type u)
h₁ : x = (lmul' R : (a : S ⊗[R] S) → S) (1 ⊗ₜ[R] x)
⊢ Eq (α := (↑(of S) : Type u))
    ((Hom.hom (𝟙 (of S)) : (a : (↑(of S) : Type u)) → (↑(of S) : Type u)) x : (↑(of S) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
              (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))) :
          (a : (↑(of S) : Type u)) → (↑(of S) : Type u))
        x :
      (↑(of S) : Type u))

Tactic:
change x = Algebra.TensorProduct.lmul' R (S := S) (1 ⊗ₜ[R] x)

Premises used: Algebra.TensorProduct.lmul', TensorProduct.tmul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : (↑(of S) : Type u)
⊢ x = (lmul' R : (a : S ⊗[R] S) → S) (1 ⊗ₜ[R] x)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
M S T : Scheme
inst : M.Over S
f : T ⟶ S
inst_1 : MonObj (Over.mk (M ↘ S))
⊢ MonObj (Over.mk (pullback (M ↘ S) f ↘ T))

Tactic:
exact Over.monObjMkPullbackSnd

Premises used: CategoryTheory.Over.monObjMkPullbackSnd
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
M S T : Scheme
inst : M.Over S
f : T ⟶ S
inst_1 : MonObj (Over.mk (M ↘ S))
inst_2 : IsCommMonObj (Over.mk (M ↘ S))
⊢ IsCommMonObj (Over.mk (pullback (M ↘ S) f ↘ T))

Tactic:
Over.isCommMonObj_mk_pullbackSnd

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Over.isCommMonObj_mk_pullbackSnd, CategoryTheory.over
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
M S T : Scheme
inst : M.Over S
f : T ⟶ S
inst_1 : MonObj (Over.mk (M ↘ S))
inst_2 : IsCommMonObj (Over.mk (M ↘ S))
⊢ IsCommMonObj (Over.mk (pullback (M ↘ S) f ↘ T))

Tactic:
exact Over.isCommMonObj_mk_pullbackSnd

Premises used: CategoryTheory.Over.isCommMonObj_mk_pullbackSnd
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
M S T : Scheme
inst : M.Over S
f : T ⟶ S
inst_1 : GrpObj (Over.mk (M ↘ S))
⊢ GrpObj (Over.mk (pullback (M ↘ S) f ↘ T))

Tactic:
exact Over.grpObjMkPullbackSnd

Premises used: CategoryTheory.Over.grpObjMkPullbackSnd
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
M S T : Scheme
inst : M.Over S
f : T ⟶ S
⊢ pullback.snd (M ↘ S) (𝟙 S) ≫ 𝟙 S = pullback (M ↘ S) (𝟙 S) ↘ S

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
M S T : Scheme
inst : M.Over S
f : T ⟶ S
inst_1 : MonObj (Over.mk (M ↘ S))
⊢ IsMonHom (M := Over.mk (pullback (M ↘ S) (𝟙 S) ↘ S)) (N := Over.mk (M ↘ S))
    (Hom.asOver (pullback.fst (M ↘ S) (𝟙 S)) S)

Tactic:
Over.isMonHom_pullbackFst_id_right

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.over, CategoryTheory.OverClass.asOver, CategoryTheory.OverClass.asOverHom, CategoryTheory.Over.isMonHom_pullbackFst_id_right
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
M S T : Scheme
inst : M.Over S
f : T ⟶ S
inst_1 : MonObj (Over.mk (M ↘ S))
⊢ IsMonHom (M := Over.mk (pullback (M ↘ S) (𝟙 S) ↘ S)) (N := Over.mk (M ↘ S))
    (Hom.asOver (pullback.fst (M ↘ S) (𝟙 S)) S)

Tactic:
exact Over.isMonHom_pullbackFst_id_right

Premises used: CategoryTheory.Over.isMonHom_pullbackFst_id_right
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
rw : IsSeparated (Y := ⊤_ Scheme) (X.toSpecΓ ≫ terminal.from (Spec Γ(X, ⊤)))
⊢ IsSeparated (Y := ⊤_ Scheme) (terminal.from X)

Tactic:
rw [← terminal.comp_from X.toSpecΓ]

Premises used: CategoryTheory.Limits.terminal.comp_from, AlgebraicGeometry.Scheme.toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
⊢ IsSeparated (Y := ⊤_ Scheme) (X.toSpecΓ ≫ terminal.from (Spec Γ(X, ⊤)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
rw : IsIso.{u, u + 1} (X := IdealSheafData.subscheme (X := Spec Γ(X, ⊤)) ⊥) (IdealSheafData.subschemeι ⊥)
⊢ IsIso (Hom.ker X.toSpecΓ).subschemeι

Tactic:
rw [X.ker_toSpecΓ]

Premises used: AlgebraicGeometry.Scheme.ker_toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
⊢ IsIso.{u, u + 1} (X := IdealSheafData.subscheme (X := Spec Γ(X, ⊤)) ⊥) (IdealSheafData.subschemeι ⊥)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
⊢ IsIso (Hom.imageι X.toSpecΓ)

Tactic:
have : IsIso X.toSpecΓ.imageι := by delta Hom.imageι Hom.image; rw [X.ker_toSpecΓ]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
rw : IsOpenImmersion (Hom.toImage X.toSpecΓ ≫ Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion X.toSpecΓ

Tactic:
rw [← X.toSpecΓ.toImage_imageι]

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_imageι, AlgebraicGeometry.Scheme.toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion (Hom.toImage X.toSpecΓ ≫ Hom.imageι X.toSpecΓ)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Y.IsQuasiAffine
inst_1 : IsImmersion f
inst_2 : CompactSpace.{u} ↥X
rw : IsImmersion (f ≫ Y.toSpecΓ)
⊢ IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))

Tactic:
rw [← toSpecΓ_naturality]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Y.IsQuasiAffine
inst_1 : IsImmersion f
inst_2 : CompactSpace.{u} ↥X
⊢ IsImmersion (f ≫ Y.toSpecΓ)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Y.IsQuasiAffine
inst_1 : IsImmersion f
inst_2 : CompactSpace.{u} ↥X
⊢ IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))

Tactic:
have : IsImmersion (X.toSpecΓ ≫ Spec.map f.appTop) := by rw [← toSpecΓ_naturality]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Y.IsQuasiAffine
inst_1 : IsImmersion f
inst_2 : CompactSpace.{u} ↥X
this : IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))
⊢ IsImmersion X.toSpecΓ

Tactic:
have : IsImmersion X.toSpecΓ := .of_comp _ (Spec.map f.appTop)
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Y.IsQuasiAffine
inst_1 : IsImmersion f
inst_2 : CompactSpace.{u} ↥X
this_1 : IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))
this : IsImmersion X.toSpecΓ
⊢ X.IsQuasiAffine

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
⊢ Opens.IsBasis.{u} (α := ↥X)
    {x : TopologicalSpace.Opens ↥X | ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}

Tactic:
Opens.isBasis_iff_nbhd.mpr fun {U x} hxU ↦ ?_

Premises used: Iff.mpr, TopologicalSpace.Opens.isBasis_iff_nbhd
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
refine :
  ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X} (hxU : x ∈ U),
    ∃ (U' : TopologicalSpace.Opens ↥X),
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
          {x : TopologicalSpace.Opens ↥X |
            ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}
          U' ∧
        x ∈ U' ∧ U' ≤ U
⊢ Opens.IsBasis.{u} (α := ↥X)
    {x : TopologicalSpace.Opens ↥X | ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}

Tactic:
refine Opens.isBasis_iff_nbhd.mpr fun {U x} hxU ↦ ?_

Premises used: Iff.mpr, TopologicalSpace.Opens.isBasis_iff_nbhd
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
obtain :
  ∀ (r : (↑Γ(X, ⊤) : Type u))
    (hxr :
      Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
        (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
              (a : ↥X) → ↥(Spec Γ(X, ⊤)))
            x :
          ↥(Spec Γ(X, ⊤))))
    (hrU :
      (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
            (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
          (↑U : Set ↥X)),
    ∃ (U' : TopologicalSpace.Opens ↥X),
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
          {x : TopologicalSpace.Opens ↥X |
            ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}
          U' ∧
        x ∈ U' ∧ U' ≤ U
⊢ ∃ (U' : TopologicalSpace.Opens ↥X),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
        {x : TopologicalSpace.Opens ↥X |
          ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U

Tactic:
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, hxr, hrU⟩ := (PrimeSpectrum.isBasis_basic_opens
    (R := Γ(X, ⊤))).exists_subset_of_mem_open (Set.mem_image_of_mem _ hxU) (X.toSpecΓ ''ᵁ U).2

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, AlgebraicGeometry.Scheme.toSpecΓ, Set.mem_image_of_mem, TopologicalSpace.Opens.is_open', CategoryTheory.Functor.obj, PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open