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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).base ≫ (↑U).isoSpec.inv.base))

Tactic:
← TopCat.epi_iff_surjective

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Epi ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).base ≫ (↑U).isoSpec.inv.base)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
⊢ ∀ (hxU : x ∈ U),
    (structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
      (structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)

Tactic:
hxU

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ (structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
    (structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f

Tactic:
rw [fromSpec_preimage_basicOpen', ← basicOpen_eq_of_affine]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this :
  (pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))) ≫
      (pullback.snd (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))) ≫
        pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
    𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
simp only [Category.assoc, IsIso.inv_hom_id_assoc] at this

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq :
  (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i))
this :
  pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ D.t j i ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
    𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑x)) (hU.primeIdealOf x).asIdeal

Tactic:
by
  rcases x with ⟨x, hx⟩
  set y := hU.primeIdealOf ⟨x, hx⟩ with hy
  have : hU.fromSpec y = x := hy ▸ hU.fromSpec_primeIdealOf ⟨x, hx⟩
  clear_value y
  subst this
  exact hU.isLocalization_stalk' y hx

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
else

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
⊢ HasPullback (D.f' i j) (D.f' i k)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
else

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
⊢ HasPullback (D.f' i j) (D.f' i k)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (sigmaIsoSigma D.diagram.left).inv) ⟨(i, j), y⟩)))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (sigmaIsoSigma D.diagram.left).inv) ⟨(i, j), y⟩)))

Tactic:
rw [sigmaIsoSigma_inv_apply]

Goal state after:
case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
    ((ConcreteCategory.hom (sigmaIsoSigma D.U).hom)
      ((ConcreteCategory.hom
          (D.diagram.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor D.diagram.right))
            (colimit.isColimit (Discrete.functor D.diagram.left))))
        ((ConcreteCategory.hom (Sigma.ι D.diagram.left (i, j))) y)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom)

Tactic:
← TopCat.epi_iff_surjective

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ Epi (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ pullback (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) ⟶
    pullback (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))

Tactic:
refine ?_ ≫ (pullbackSymmetry _ _).hom

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ pullback (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) ⟶
    pullback (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
apply pullback.hom_ext <;> simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom

Tactic:
apply pullback.hom_ext <;> simp

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
i j k : 𝒰.I₀
⊢ pullback (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶ pullback (fV 𝒰 f g j k) (fV 𝒰 f g j i)

Tactic:
refine ?_ ≫ (pullbackSymmetry _ _).hom

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ pullback (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶ pullback (fV 𝒰 f g j i) (fV 𝒰 f g j k)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
U : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
𝒰 : X.OpenCover := { I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι, mem₀ := ⋯ }
⊢ f = g

Tactic:
exact 𝒰.hom_ext _ _ hU

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f
h₂ : αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f
h₁' :
  ∀ (x : ↥X'), ((BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f) x = (αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl) x
⊢ IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
    IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr

Tactic:
have h₂' (x : _) := congr($h₂ x).symm

Goal state after:
case refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f
h₂ : αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f
h₁' :
  ∀ (x : ↥X'), ((BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f) x = (αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl) x
h₂' :
  ∀ (x : ↥Y'), ((BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f) x = (αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr) x
⊢ IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
    IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr
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 : ι
⊢ ∀ ⦃j : ι⦄,
    ix ≠ j →
      Function.onFun Disjoint (fun x ↦ Set.range ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) x)))) ix
        j

Tactic:
iy

Goal state after:
ι : 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 : ι
⊢ ix ≠ iy →
    Function.onFun Disjoint (fun x ↦ Set.range ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) x)))) ix
      iy
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
⊢ ∀ ⦃a : ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))⦄,
    a ∈ (fun x ↦ Set.range ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) x)))) ix →
      ∀ ⦃b : ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))⦄,
        b ∈ (fun x ↦ Set.range ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) x)))) iy → a ≠ b

Tactic:
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ e

Goal state after:
ι : 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
⊢ False
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.fst 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.fst f g

Tactic:
by simp [p1]

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 : D.J
U : Opens ↑↑(D.U i)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (D.f i i).base)

Tactic:
← TopCat.epi_iff_surjective

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ Epi (D.f i i).base
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✝
𝒰 : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ =
    (pullbackSymmetry f (𝒰.f i ≫ g)).hom ≫
      pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯ ≫ (pullbackSymmetry g f).hom

Tactic:
apply pullback.hom_ext <;> simp

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 : PullbackCone f✝ g✝
𝒰X : X.OpenCover
𝒰Y : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰X.I₀
j : 𝒰Y.I₀
⊢ pullback.map (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) f g (𝒰X.f (i, j).1) (𝒰Y.f (i, j).2) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g))).hom ≫
      (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun x ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
        ((Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀).symm (i, j))

Tactic:
apply pullback.hom_ext <;> simp

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
⊢ P f

Tactic:
by
    have : (f ≫ g) ⁻¹ᵁ g.opensRange = ⊤ := by simp
    have : f = X.topIso.inv ≫ (X.isoOfEq this).inv ≫ (f ≫ g) ∣_ g.opensRange ≫
        (IsOpenImmersion.isoOfRangeEq g.opensRange.ι g (by simp)).hom := by
      simp [← cancel_mono g]
    simp_rw [this, cancel_left_of_respectsIso (P := P), cancel_right_of_respectsIso (P := P)]
    exact H _ _ hfg

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

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
⊢ Set.range ⇑f = Set.range ⇑g

Tactic:
rw [← hge]
  simp [Set.range_comp]

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

Goal state before:
pp: case e'_3
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) := ⋯
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
e_2✝ :
  pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) =
    pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom 𝒰 f i) ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom 𝒰 f i)
⊢ (pullbackDiagonalMapIso f (𝒰.f i) ((𝒰' i).f j) ((𝒰' i).f k)).inv ≫
      pullback.snd (pullback.diagonal f)
        (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
          ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) =
    pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
ext1 <;> simp [Scheme.Cover.pullbackHom]

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

Goal state before:
pp: case e'_3
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
e_1✝ :
  pullback (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯) =
    pullback (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯)
e_2✝ :
  pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) = pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)
⊢ (pullbackDiagonalMapIso f g f₁ f₂).hom ≫ pullback.mapDesc f₁ f₂ (pullback.snd f g) =
    pullback.snd (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯)

Tactic:
apply pullback.hom_ext <;> simp

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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
⊢ IsNilpotent f

Tactic:
obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU 1 f h

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
hf : X.basicOpen f = ⊥
h : (1 |_ X.basicOpen f) ⋯ = 0
n : ℕ
hn : f ^ n * 1 = 0
⊢ IsNilpotent f
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: ⊢ LocalizationPreserves fun R x ↦ IsReduced R

Tactic:
by
  introv R _ _
  constructor
  rintro x ⟨_ | n, e⟩
  · simpa using congr_arg (· * x) e
  obtain ⟨⟨y, m⟩, hx⟩ := IsLocalization.surj M x
  dsimp only at hx
  let hx' := congr_arg (· ^ n.succ) hx
  simp only [mul_pow, e, zero_mul, ← map_pow] at hx'
  rw [← (algebraMap R S).map_zero] at hx'
  obtain ⟨m', hm'⟩ := (IsLocalization.eq_iff_exists M S).mp hx'
  apply_fun (· * (m' : R) ^ n) at hm'
  simp only [mul_assoc, zero_mul, mul_zero] at hm'
  rw [← mul_left_comm, ← pow_succ', ← mul_pow] at hm'
  replace hm' := IsNilpotent.eq_zero ⟨_, hm'.symm⟩
  rw [← (IsLocalization.map_units S m).mul_left_inj, hx, zero_mul,
    IsLocalization.map_eq_zero_iff M]
  exact ⟨m', by rw [← hm', mul_comm]⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
⊢ 1 ≤ (span {x}).height

Tactic:
Ideal.height_eq_inf_minimalPrimes

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
⊢ 1 ≤ ⨅ J ∈ (span {x}).minimalPrimes, J.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
⊢ ⊥.height = 0

Tactic:
Ideal.height_eq_inf_minimalPrimes

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
⊢ ⨅ J ∈ ⊥.minimalPrimes, J.height = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hI : I.height = 0
p : Ideal R
w✝ : p.IsPrime
hIp : I ≤ p
hp0 : p.height = 0
⊢ I = ⊥

Tactic:
height_eq_zero_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hI : I.height = 0
p : Ideal R
w✝ : p.IsPrime
hIp : I ≤ p
hp0 : p ∈ minimalPrimes R
⊢ I = ⊥
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V

Tactic:
obtain ⟨_, ⟨j, rfl⟩, hx, i⟩ :=
    X.affineBasisCover_is_basis.exists_subset_of_mem_open (SetLike.mem_coe.2 x.prop) U.isOpen

Goal state after:
P : {X : Scheme} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U
h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ U V, U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat), P ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : ↑x ∈ Set.range ⇑(X.affineBasisCover.f j)
i : Set.range ⇑(X.affineBasisCover.f j) ⊆ ↑U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
⊢ IsReduced X

Tactic:
by
  constructor
  intro U
  rcases U.1.eq_empty_or_nonempty with h | h
  · have : U = ⊥ := SetLike.ext' h
    have : Subsingleton Γ(X, U) :=
      CommRingCat.subsingleton_of_isTerminal (X.sheaf.isTerminalOfEqEmpty this)
    infer_instance
  · have : Nonempty U := by simpa
    infer_instance

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
⊢ ∀ (h_1 : x ∈ ↑U),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1))
        (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1)) (I.ideal U)

Tactic:
hxU

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)