mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
        𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    D.diagramOverOpenπ U j ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
        𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

Tactic:
simp_rw [Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          D.diagramOverOpenπ U j ≫
            (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
                (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
              𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    D.diagramOverOpenπ U j ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
        𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        ((D.f i i).c.app (op U) ≫
            (D.t i i).c.app ((Opens.map (D.f i i).base).op.obj (op U)) ≫
              invApp (D.f i i)
                  (unop (op ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ≫
                (D.U i).presheaf.map (eqToHom ⋯).op) ≫
          (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
            (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
rw [congr_app (D.t_id _), id_c_app]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        ((D.f i i).c.app (op U) ≫
            ((D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U))) ≫
                (D.V (i, i)).presheaf.map (eqToHom ⋯)) ≫
              invApp (D.f i i)
                  (unop (op ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ≫
                (D.U i).presheaf.map (eqToHom ⋯).op) ≫
          (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
            (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        ((D.f i i).c.app (op U) ≫
            ((D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U))) ≫
                (D.V (i, i)).presheaf.map (eqToHom ⋯)) ≫
              invApp (D.f i i)
                  (unop (op ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ≫
                (D.U i).presheaf.map (eqToHom ⋯).op) ≫
          (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
            (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
simp_rw [Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        (D.f i i).c.app (op U) ≫
          (D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U))) ≫
            (D.V (i, i)).presheaf.map (eqToHom ⋯) ≫
              invApp (D.f i i) ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))) ≫
                (D.U i).presheaf.map (eqToHom ⋯).op ≫
                  (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
                    (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).OpenCover

Tactic:
by
  apply
    (openCoverOfBase' 𝒰 f g).copy 𝒰.I₀
      (fun i =>
        pullback (pullback.snd _ _ : pullback f (𝒰.f i) ⟶ _)
          (pullback.snd _ _ : pullback g (𝒰.f i) ⟶ _))
      (fun i =>
        pullback.map _ _ _ _ (pullback.fst _ _) (pullback.fst _ _) (𝒰.f i)
          pullback.condition.symm pullback.condition.symm)
      ((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit).symm) fun _ => Iso.refl _
  intro i
  rw [Iso.refl_hom, Category.id_comp, openCoverOfBase'_f]
  ext : 1 <;>
  · simp only [limit.lift_π, PullbackCone.mk_π_app, Equiv.trans_apply, Category.assoc,
    limit.lift_π_assoc, cospan_left, Category.comp_id,
      limit.isoLimitCone_inv_π_assoc, PullbackCone.π_app_left, IsPullback.cone_fst,
      pullbackSymmetry_hom_comp_snd_assoc, limit.isoLimitCone_inv_π,
      PullbackCone.π_app_right, IsPullback.cone_snd, pullbackSymmetry_hom_comp_fst_assoc]
    rfl

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        (D.U i).presheaf.map (homOfLE ⋯).op ≫
          (D.U i).presheaf.map
              ((opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
            (D.U i).presheaf.map (eqToHom ⋯).op ≫
              (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
                (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
iterate 3 rw [← Functor.map_comp_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map
          ((((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
              (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
            (eqToHom ⋯).op) ≫
        (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.left.e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) =
    limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))

Tactic:
simp_rw [Category.assoc]

Goal state after:
case op.left.e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
            (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) =
    limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))

Tactic:
simp_rw [Category.assoc]

Goal state after:
case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2.h₀
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
i : (openCoverOfBase 𝒰 f f).I₀
j : (𝒱 i).I₀
H :
  pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.snd ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.fst ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))
⊢ ((pullback.map (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) (pullback.diagonal f)
            (pullback.map ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) f f
              ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
            (𝟙 X) (𝟙 ((diagonalCover f 𝒰 𝒱).X ⟨i, (j, j)⟩)) (𝟙 (pullback.diagonalObj f)) ⋯ ⋯ ≫
          (pullbackDiagonalMapIso f (𝒰.f i) ((𝒱 i).f j) ((𝒱 i).f j)).hom ≫
            CategoryTheory.inv (pullback.diagonal ((𝒱 i).f j))) ≫
        pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) ≫
      pullback.fst ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) =
    (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
        𝟙 ((diagonalCover f 𝒰 𝒱).X ⟨i, (j, j)⟩)) ≫
      pullback.fst ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))

Tactic:
simp only [Category.assoc, pullback.diagonal_fst, Category.comp_id]
    simp only [← Category.assoc, IsIso.comp_inv_eq]
    apply pullback.hom_ext <;> simp [H]

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
⊢ P ((algebraMap S Sₜ).comp f)

Tactic:
let e : Localization.Away t ≃+* Sₜ :=
      (IsLocalization.algEquiv (Submonoid.powers t) _ _).toRingEquiv
    have : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t)) :=
      RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _) _).symm)
    rw [this, RingHom.comp_assoc]
    exact hP.left _ _ (hs t ht)

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
⊢ ∀ (i : (a : ↑s) × ↑(t a)),
    P
      ((algebraMap S
            ((fun x ↦
                match x with
                | ⟨a, b⟩ => Localization.Away ↑b)
              i)).comp
        f)

Tactic:
intro ⟨a, b⟩
    rw [IsScalarTower.algebraMap_eq S (Localization.Away a.val) (Localization.Away b.val)]
    apply ht _ _ b.property

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen r)

Tactic:
sourceAffineLocally_morphismRestrict

Goal state after:
case to_basicOpen
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen ↑r)
U : ↑X.affineOpens
r : ↑↑s
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

Tactic:
sourceAffineLocally_morphismRestrict

Goal state after:
case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
U : ↑X.affineOpens
r : ↑↑s
hs' :
  ∀ (r : ↥s) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen ↑r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen ↑r) (↑V) e))
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑g)
⊢ CompactSpace ↥(pullback f₁ f₂)

Tactic:
rw [IsOpenImmersion.range_pullback_to_base_of_left] at e

Goal state after:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑f₁ ∩ Set.range ⇑f₂)
⊢ CompactSpace ↥(pullback f₁ f₂)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : p.FiniteHeight
⊢ ∃ l, RelSeries.last l = { asIdeal := p, isPrime := ⋯ } ∧ ↑l.length = p.height

Tactic:
by
  obtain ⟨n, hn⟩ := ENat.ne_top_iff_exists.mp (p.height_ne_top (IsPrime.ne_top ‹_›))
  rw [Ideal.height_eq_primeHeight, Ideal.primeHeight] at hn ⊢
  obtain ⟨l, last, len⟩ := Order.exists_series_of_height_eq_coe (⟨p, ‹_›⟩ : PrimeSpectrum R) hn.symm
  exact ⟨l, last, len ▸ hn⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ I.height ≤ J.height

Tactic:
simp only [I.height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]
  refine le_iInf₂ (fun p hp ↦ ?_)
  have := hp.isPrime
  obtain ⟨q, hq, e⟩ := Ideal.exists_minimalPrimes_le (h.trans hp.le)
  have := hq.isPrime
  exact (iInf₂_le q hq).trans (Ideal.height_mono_of_isPrime e)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
R S : CommRingCat
φ : R ⟶ S
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
by
  have H := (isLocal_ringHomProperty P).respectsIso
  rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I.ideal = J.ideal
⊢ I = J

Tactic:
obtain ⟨i, _, s, hs⟩ := I
  obtain ⟨j, _, t, ht⟩ := J
  subst h
  congr
  rw [hs, ht]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (⊤ U) = ⊤ (X.affineBasicOpen f)

Tactic:
simp [Ideal.map_top]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case refine_2
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
e : Γ(X, { carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ }) ≅
  CommRingCat.of
    ↑((X.sheaf.obj.obj (op { carrier := Sᶜ, is_open' := ⋯ })).prodFan
          (X.sheaf.obj.obj (op { carrier := Tᶜ, is_open' := ⋯ }))).1 :=
  (X.sheaf.isProductOfDisjoint { carrier := Sᶜ, is_open' := ⋯ } { carrier := Tᶜ, is_open' := ⋯ }
        ?refine_1).conePointUniqueUpToIso
    ((X.sheaf.obj.obj (op { carrier := Sᶜ, is_open' := ⋯ })).prodFanIsLimit
      (X.sheaf.obj.obj (op { carrier := Tᶜ, is_open' := ⋯ })))
⊢ False

Tactic:
have : IsDomain (Γ(X, ⟨Sᶜ, hS.1⟩) × Γ(X, ⟨Tᶜ, hT.1⟩)) :=
      e.symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _
    exact false_of_nontrivial_of_product_domain Γ(X, ⟨Sᶜ, hS.1⟩) Γ(X, ⟨Tᶜ, hT.1⟩)

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
⊢ Z ≤ I.support ↔ I ≤ vanishingIdeal Z

Tactic:
simp only [le_def, vanishingIdeal_ideal, ← PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal]
  trans ∀ U : X.affineOpens, (Z : Set X) ∩ U ⊆ I.support ∩ U
  · refine ⟨fun H U x hx ↦ ⟨H hx.1, hx.2⟩, fun H x hx ↦ ?_⟩
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
    exact (H ⟨U, hU⟩ ⟨hx, hxU⟩).1
  refine forall_congr' fun U ↦ ?_
  rw [coe_support_inter, ← Set.image_subset_image_iff U.2.fromSpec.isOpenEmbedding.injective,
    Set.image_preimage_eq_inter_range, IsAffineOpen.fromSpec_image_zeroLocus,
    IsAffineOpen.range_fromSpec]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ U.fromSpecStalkOfMem x hxU ≫ U.toSpecΓ = Spec.map (X.presheaf.germ U x hxU)

Tactic:
by
  rw [fromSpecStalkOfMem, Opens.toSpecΓ, Category.assoc, fromSpecStalk_toSpecΓ_assoc,
    ← Spec.map_comp, ← Spec.map_comp]
  congr 1
  rw [IsIso.comp_inv_eq, Iso.inv_comp_eq]
  erw [Hom.germ_stalkMap U.ι U ⟨x, hxU⟩]
  rw [Opens.ι_app, Opens.topIso_hom, ← Functor.map_comp_assoc]
  exact (U.toScheme.presheaf.germ_res (homOfLE le_top) ⟨x, hxU⟩ (U := U.ι ⁻¹ᵁ U) hxU).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
⊢ IsAffineHom (X.basicOpen r).ι

Tactic:
constructor
  intro U hU
  fapply (Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion (X.basicOpen r).ι).mp
  convert! hU.basicOpen (X.presheaf.map (homOfLE le_top).op r)
  rw [X.basicOpen_res]
  ext1
  refine Set.image_preimage_eq_inter_range.trans ?_
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)

pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)

Tactic:
· intro X Y Z e f ⟨hZ, ⟨hY, hf⟩⟩
    simpa [hP.cancel_right_isIso, IsAffine.of_isIso e.hom]

Goal state after:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))

Tactic:
rw [map, ← le_support_iff_le_vanishingIdeal, TopologicalSpace.Closeds.closure_le]
    refine .trans ?_ (Hom.range_subset_ker_support _)
    rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
H : IsAffineOpen (f ⁻¹ᵁ ↑U)
⊢ (I.map f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.app f ↑U)) (I.ideal ⟨f ⁻¹ᵁ ↑U, H⟩)

Tactic:
have : RingHom.ker (I.subschemeObjIso ⟨_, H⟩).inv.hom = ⊥ :=
    RingHom.ker_coe_equiv (I.subschemeObjIso ⟨_, H⟩).symm.commRingCatIsoToRingEquiv
  simp [map, ← RingHom.comap_ker, subschemeι_app _ ⟨_, H⟩,
    this, ← RingHom.ker_eq_comap_bot]

Goal state after: