mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case 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
i : 𝒰.I₀
⊢ (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯) ≫
      pullback.snd (p1 𝒰 f g) (𝒰.f i) =
    𝟙 (pullback (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)

Tactic:
Category.assoc,

Goal state after:
case 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
i : 𝒰.I₀
⊢ pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
      pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i) =
    𝟙 (pullback (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case inv_hom_id.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
i : 𝒰.I₀
⊢ (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
Category.assoc,

Goal state after:
case inv_hom_id.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
i : 𝒰.I₀
⊢ pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.fst (𝒰.f i ≫ f) g =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map
      (((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) ≫
        coprod.inl.unop) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))

Tactic:
Category.assoc,

Goal state after:
case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map
      ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
        (opProdIsoCoprod R S).unop.inv ≫ coprod.inl.unop) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map
      (((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) ≫
        coprod.inr.unop) =
    Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S))

Tactic:
Category.assoc,

Goal state after:
case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map
      ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
        (opProdIsoCoprod R S).unop.inv ≫ coprod.inr.unop) =
    Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
x : ↥(Spec (R ix))
y : ↥(Spec (R iy))
e :
  (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) ix))) x =
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) iy))) y
this : (DFinsupp.single iy 1) iy ∈ y.asIdeal
⊢ False

Tactic:
simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this

Goal state after:
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✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫ (pullback.congrHom h₁ ⋯).hom) ≫
      pullback.fst s.fst (𝒰.f i) ≫ m =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫ (pullback.congrHom h₁ ⋯).hom) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i

Tactic:
Category.assoc,

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
      (pullback.congrHom h₁ ⋯).hom ≫ pullback.fst s.fst (𝒰.f i) ≫ m =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫ (pullback.congrHom h₁ ⋯).hom) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom) ≫ pullback.fst (𝒰.f i ≫ f) g =
    ((((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
            pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
          (pullbackSymmetry s.fst (𝒰.f i)).hom) ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g

Tactic:
Category.assoc,

Goal state after:
case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.fst (𝒰.f i ≫ f) g =
    (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
      pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯ ≫
        (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
          pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ pullback.fst (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom) ≫ pullback.snd (𝒰.f i ≫ f) g =
    ((((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
            pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
          (pullbackSymmetry s.fst (𝒰.f i)).hom) ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
      pullback.snd (𝒰.f i ≫ f) g

Tactic:
Category.assoc,

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.snd (𝒰.f i ≫ f) g =
    (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
      pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯ ≫
        (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
          pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ pullback.snd (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
i : 𝒰.I₀
⊢ P
    (((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (Scheme.Hom.opensRange (𝒰.f i)).ι ⋯).hom ≫
        (Scheme.Hom.opensRange (𝒰.f i)).ι) ≫
      f)

Tactic:
Category.assoc,

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
i : 𝒰.I₀
⊢ P
    ((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (Scheme.Hom.opensRange (𝒰.f i)).ι ⋯).hom ≫
      (Scheme.Hom.opensRange (𝒰.f i)).ι ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : (Scheme.Cover.ulift 𝒰).I₀
⊢ P
    (((IsOpenImmersion.isoOfRangeEq (𝒰.f (Scheme.Cover.idx 𝒰 i)) (Scheme.Hom.opensRange (𝒰.f (Scheme.Cover.idx 𝒰 i))).ι
            ⋯).inv ≫
        𝒰.f (Scheme.Cover.idx 𝒰 i)) ≫
      f)

Tactic:
Category.assoc,

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : (Scheme.Cover.ulift 𝒰).I₀
⊢ P
    ((IsOpenImmersion.isoOfRangeEq (𝒰.f (Scheme.Cover.idx 𝒰 i)) (Scheme.Hom.opensRange (𝒰.f (Scheme.Cover.idx 𝒰 i))).ι
          ⋯).inv ≫
      𝒰.f (Scheme.Cover.idx 𝒰 i) ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P (((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (Scheme.Hom.opensRange (𝒰.f i)).ι ⋯).inv ≫ 𝒰.f i) ≫ f)

Tactic:
Category.assoc,

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : 𝒰.I₀
⊢ P ((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (Scheme.Hom.opensRange (𝒰.f i)).ι ⋯).inv ≫ 𝒰.f i ≫ f)
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✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ pullback.snd f g =
    ((Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
        (gluing (Cover.ulift 𝒰) f g).ι ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
          (limit.isoLimitCone
              { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv) ≫
      pullback.snd f g

Tactic:
by simp [p2]

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ ∃ i, x ∈ V i

Tactic:
use x, hxU x

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

Goal state before:
pp: case basicOpen
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
r : ↑Γ(Y, ↑U)
h : Q (f ∣_ ↑U)
⊢ Q (f ∣_ ↑(Y.affineBasicOpen r))

Tactic:
have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this

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

Goal state before:
pp: case openCover
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
s : Finset ↑Γ(Y, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (f ∣_ ↑(Y.affineBasicOpen ↑f_1))
⊢ Q (f ∣_ ↑U)

Tactic:
| openCover U s hs H =>

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [cocone, ← hm, glueDataι_naturality,
      ← GlueData.ι_isoLocallyRingedSpace_inv, -ι_gluedIso_inv_assoc, -ι_gluedIso_inv]

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

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

Tactic:
Category.assoc,

Goal state after:
case h.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U i =
    𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ (lift (D.f i j) s.fst ⋯ ≫ (D.vPullbackCone i j).snd) ≫ D.ι j = s.snd ≫ D.ι j

Tactic:
Category.assoc,

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ lift (D.f i j) s.fst ⋯ ≫ (D.vPullbackCone i j).snd ≫ D.ι j = s.snd ≫ D.ι j
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: ⊢ @Surjective = topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective

Tactic:
ext; exact surjective_iff _

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

Goal state before:
pp: case hP₂
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → SpecializingMap f → SpecializingMap (s.restrictPreimage f)

Tactic:
introv _ _ hf
    rw [specializingMap_iff_closure_singleton_subset] at hf ⊢
    intro ⟨x, hx⟩ ⟨y, hy⟩ hcl
    simp only [closure_subtype, Set.restrictPreimage_mk, Set.image_singleton] at hcl
    obtain ⟨a, ha, hay⟩ := hf x hcl
    rw [← specializes_iff_mem_closure] at hcl
    exact ⟨⟨a, by simp [hay, hy]⟩, by simpa [closure_subtype], by simpa⟩

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
⊢ (targetAffineLocally Q).diagonal f

Tactic:
let 𝒱 := Scheme.Pullback.openCoverOfLeftRight.{u} 𝒰 𝒰 f f

Goal state after:
Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
⊢ (targetAffineLocally Q).diagonal f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₁ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ (U : Opens X), P f → P (f ∘ Subtype.val)
hP₂ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ {ι : Type u} (U : ι → Opens X), IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f
⊢ IsZariskiLocalAtSource (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
apply IsZariskiLocalAtSource.mk'
  · introv hf
    exact hP₁ f f.continuous _ hf
  · introv hU hf
    exact hP₂ f f.continuous _ hU hf

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ ∃ s, s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, ↑i

Tactic:
refine ⟨Set.range g, Set.finite_range g, ?_⟩

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ X.basicOpen f = ⨆ i ∈ Set.range g, ↑i
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
⊢ ∃ n, f ^ n * x = 0

Tactic:
replace e : U = iSup fun i : s => (i : X.Opens) := by
    ext1; simpa using e

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 = ⨆ i, ↑↑i
⊢ ∃ n, f ^ n * x = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
S : X.Opens
⊢ IsCompact S.carrier →
    ∀ (U : ↑X.affineOpens),
      (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) →
        IsQuasiSeparated (S ⊔ ↑U).carrier →
          ∀ (f : ↑Γ(X, S ⊔ ↑U)) (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

Tactic:
hS

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),
    (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) →
      IsQuasiSeparated (S ⊔ ↑U).carrier →
        ∀ (f : ↑Γ(X, S ⊔ ↑U)) (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
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case openCover
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)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
hs : Ideal.span ↑s = ⊤
H : ∀ (f_1 : ↥s), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(X.affineBasicOpen ↑f_1) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
| openCover U s hs H =>

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], KrullDimLE n (Rₚ P)
⊢ KrullDimLE n R

Tactic:
Ring.krullDimLE_iff

Goal state after:
R : Type u_1
inst✝³ : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], ringKrullDim (Rₚ P) ≤ ↑n
⊢ ringKrullDim R ≤ ↑n
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : closure {x} ∈ irreducibleComponents ↥(Spec R)
inst✝ : IsReduced (Spec R)
⊢ x.asIdeal ∈ minimalPrimes ↑R

Tactic:
rwa [← PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
this : ∀ {X : Scheme} (x : ↥X), (∃ R, X = Spec R) → ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
h : ¬∃ R, X = Spec R
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f
y : ↥(Spec R)
hsub : f y ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑⊤
⊢ ringKrullDim ↑(X.presheaf.stalk (f y)) = ↑(coheight y)

Tactic:
← this _ ⟨R, rfl⟩

Goal state after:
case inr
X : Scheme
this : ∀ {X : Scheme} (x : ↥X), (∃ R, X = Spec R) → ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
h : ¬∃ R, X = Spec R
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f
y : ↥(Spec R)
hsub : f y ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑⊤
⊢ ringKrullDim ↑(X.presheaf.stalk (f y)) = ringKrullDim ↑((Spec R).presheaf.stalk y)
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: case e_a
X Y : Scheme
f : X ⟶ Y
⊢ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective)
      f ↔
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop f

Tactic:
exact ⟨fun H ↦ inferInstanceAs (IsIso (TopCat.isoOfHomeo
    (H.1.1.toHomeomorphOfSurjective H.2)).hom), fun (_ : IsIso f.base) ↦
    let e := (TopCat.homeoOfIso <| asIso f.base); ⟨e.isOpenEmbedding, e.surjective⟩⟩

Goal state after: