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 : D.J
U : Opens ↑↑(D.U i)
X Y : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ
f' : X ⟶ Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop Y) =
    D.ιInvAppπApp U (unop X) ≫ (D.diagramOverOpen U).map f'

Tactic:
by
            induction X with | op X => ?_
            induction Y with | op Y => ?_
            let f : Y ⟶ X := f'.unop; have : f' = f.op := rfl; clear_value f; subst this
            rcases f with (_ | ⟨j, k⟩ | ⟨j, k⟩)
            · simp
            · simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
              congr 1
            simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
            -- It remains to show that the blue is equal to red + green in the original diagram.
            -- The proof strategy is illustrated in ![this diagram](https://i.imgur.com/mBzV1Rx.png)
            -- where we prove red = pink = light-blue = green = blue.
            change
              D.opensImagePreimageMap i j U ≫
                  (D.f j k).c.app _ ≫ (D.V (j, k)).presheaf.map (eqToHom _) =
                D.opensImagePreimageMap _ _ _ ≫
                  ((D.f k j).c.app _ ≫ (D.t j k).c.app _) ≫ (D.V (j, k)).presheaf.map (eqToHom _)
            rw [opensImagePreimageMap_app_assoc]
            simp_rw [Category.assoc]
            rw [opensImagePreimageMap_app_assoc, (D.t j k).c.naturality_assoc,
                snd_invApp_t_app_assoc,
                ← PresheafedSpace.comp_c_app_assoc]
            -- light-blue = green is relatively easy since the part that differs does not involve
            -- partial inverses.
            have :
              D.t' j k i ≫ (π₁ k, i, j) ≫ D.t k i ≫ 𝖣.f i k =
                (pullbackSymmetry _ _).hom ≫ (π₁ j, i, k) ≫ D.t j i ≫ D.f i j := by
              rw [← 𝖣.t_fac_assoc, 𝖣.t'_comp_eq_pullbackSymmetry_assoc,
                pullbackSymmetry_hom_comp_snd_assoc, pullback.condition, 𝖣.t_fac_assoc]
            rw [congr_app this,
                PresheafedSpace.comp_c_app_assoc (pullbackSymmetry _ _).hom]
            simp_rw [Category.assoc]
            congr 1
            rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc,
              NatTrans.naturality_assoc]
            simp_rw [Functor.op_obj]
            rw [← PresheafedSpace.comp_c_app_assoc, congr_app (pullbackSymmetry_hom_comp_snd _ _)]
            simp_rw [Category.assoc, Functor.op_obj, comp_base, Opens.map_comp_obj,
              TopCat.Presheaf.pushforward_obj_map]
            rw [IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.inv_naturality_assoc,
              IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc]
            repeat rw [← (D.V (j, k)).presheaf.map_comp]
            rfl

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

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ U = (Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U)

Tactic:
ext1

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U = ↑((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : Q.IsLocal := isLocal_affineProperty P
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j : ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i).I₀
⊢ Q (Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f ⟨i, j⟩)

Tactic:
have : P (𝒰.pullbackHom f i) := by
      refine (P.arrow_mk_iso_iff
        (morphismRestrictEq _ ?_ ≪≫ morphismRestrictOpensRange f (𝒰.f i))).mp (H i)
      exact (Scheme.Opens.opensRange_ι _).symm

Goal state after:
case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this✝ : Q.IsLocal := isLocal_affineProperty P
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j : ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i).I₀
this : P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ Q (Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f ⟨i, j⟩)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case mk
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
fst✝ : (openCoverOfBase 𝒰 f f).I₀
snd✝ :
  ((fun i ↦
        ((fun i ↦ openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom 𝒰 f i) (Cover.pullbackHom 𝒰 f i))
            i).toPreZeroHypercover)
      fst✝).I₀
⊢ (diagonalCover f 𝒰 𝒱).f ⟨fst✝, snd✝⟩ =
    pullback.map ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst)
      ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst) f f
      ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst))
      ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst)) (𝒰.f ⟨fst✝, snd✝⟩.fst) ⋯ ⋯

Tactic:
ext1

Goal state after:
case mk.h₀
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
fst✝ : (openCoverOfBase 𝒰 f f).I₀
snd✝ :
  ((fun i ↦
        ((fun i ↦ openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom 𝒰 f i) (Cover.pullbackHom 𝒰 f i))
            i).toPreZeroHypercover)
      fst✝).I₀
⊢ (diagonalCover f 𝒰 𝒱).f ⟨fst✝, snd✝⟩ ≫ pullback.fst f f =
    pullback.map ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst)
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst) f f
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst))
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst)) (𝒰.f ⟨fst✝, snd✝⟩.fst) ⋯ ⋯ ≫
      pullback.fst f f

case h₁
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
fst✝ : (openCoverOfBase 𝒰 f f).I₀
snd✝ :
  ((fun i ↦
        ((fun i ↦ openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom 𝒰 f i) (Cover.pullbackHom 𝒰 f i))
            i).toPreZeroHypercover)
      fst✝).I₀
⊢ (diagonalCover f 𝒰 𝒱).f ⟨fst✝, snd✝⟩ ≫ pullback.snd f f =
    pullback.map ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst)
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst) f f
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst))
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst)) (𝒰.f ⟨fst✝, snd✝⟩.fst) ⋯ ⋯ ≫
      pullback.snd f f
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource P

Tactic:
refine .mk_of_small (fun {X Y f} 𝒰 hf ↦ ?_) (fun {X Y f} 𝒰 hf ↦ ?_) <;>
  simp_rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top _ (iSup_affineOpens_eq_top Y),
      HasAffineProperty.iff_of_isAffine, morphismRestrict_comp] at hf ⊢
  · intro i U
    let 𝒰' : X.OpenCover := (Scheme.Cover.ulift 𝒰).add (𝒰.f i)
    exact (H (f ∣_ U.1) (𝒰'.restrict _)).mp (hf _) none
  · intro U
    rw [H (f ∣_ U.1) (Scheme.OpenCover.restrict 𝒰 _)]
    intro i
    exact hf _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ pullback.diagonal (Spec.map (ofHom (algebraMap R S))) =
    Spec.map (ofHom (lmul' R).toRingHom) ≫ (pullbackSpecIso R S S).inv

Tactic:
ext1

Goal state after:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ pullback.diagonal (Spec.map (ofHom (algebraMap R S))) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S))) =
    (Spec.map (ofHom (lmul' R).toRingHom) ≫ (pullbackSpecIso R S S).inv) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))

case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ pullback.diagonal (Spec.map (ofHom (algebraMap R S))) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S))) =
    (Spec.map (ofHom (lmul' R).toRingHom) ≫ (pullbackSpecIso R S S).inv) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q.diagonal f ↔ P.diagonal f

Tactic:
refine ⟨fun hf ↦ ?_, diagonal_of_diagonal_of_isPullback P .of_id_fst⟩

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
hf : Q.diagonal f
⊢ P.diagonal f
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
x : ↥X
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))

Tactic:
rw [Scheme.Hom.stalkMap_comp]

Goal state after:
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
x : ↥X
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (e ≫ f) x))

Tactic:
rw [Scheme.Hom.stalkMap_comp]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (e x) ≫ Scheme.Hom.stalkMap e x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (f ≫ e) x))

Tactic:
rw [Scheme.Hom.stalkMap_comp]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
x : ↥X
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.stalkMap e (f x) ≫ Scheme.Hom.stalkMap f x))
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, ⊤)),
    Ideal.span ↑s = ⊤ →
      (∀ (r : ↥s), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen ↑r)) →
        sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
introv hs hs' U

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 = ⊤
hs' : ∀ (r : ↥s), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen ↑r)
U : ↑X.affineOpens
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
⊢ IsEmbedding fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)

Tactic:
let 𝒲 (i) := ((𝒰.pullback₁ g).X i).affineOpenCover.openCover

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).affineOpenCover.openCover
⊢ IsEmbedding fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
⊢ QuasiSeparatedSpace ↥X

Tactic:
rw [← quasiCompact_affineProperty_iff_quasiSeparatedSpace X.toSpecΓ]

Goal state after:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ CompactSpace ↥X) X.toSpecΓ
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], SpecializingMap ⇑f → (∃ R, Y = Spec R) → IsClosedMap ⇑f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x✝ : QuasiCompact (Scheme.Cover.pullbackHom Y.affineCover f i)
⊢ SpecializingMap ⇑(Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
exact IsZariskiLocalAtTarget.of_isPullback
      (P := topologically @SpecializingMap) (.of_hasPullback _ _) H

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, ↑↑i
⊢ U = ⨆ i, ↑↑i

Tactic:
ext1

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, ↑↑i
⊢ ↑U = ↑(⨆ i, ↑↑i)
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
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ P f

Tactic:
HasAffineProperty.iff_of_isAffine (P := P)

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case refine_2
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
⊢ ∃ n y,
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Tactic:
obtain ⟨s, hs', hs⟩ :=
      isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp
        ⟨hSU _ _ Set.subset_union_left S.2 hS Set.subset_union_right U.1.2
            U.2.isCompact,
          (S ⊓ U.1).2⟩

Goal state after:
case refine_2
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
⊢ ∃ n y,
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
this : Finite ↑s
val✝ : Fintype ↑s
⊢ S ⊓ ↑U = ⨆ i, ↑↑i

Tactic:
ext1

Goal state after:
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ↑(S ⊓ ↑U) = ↑(⨆ i, ↑↑i)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
⊢ I.IsMaximal

Tactic:
have h : I ≠ ⊤ := Ideal.IsPrime.ne_top'

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ ↑p.length ≤ (RelSeries.last p).asIdeal.height

Tactic:
rw [height_eq_primeHeight]

Goal state after:
case a.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ ↑p.length ≤ (RelSeries.last p).asIdeal.primeHeight