mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y)))

Tactic:
have := PresheafedSpace.stalkMap.comp
          (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom
          (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom y

Goal state after:
ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap
      ((colimit.ι (F ⋙ forgetToSheafedSpace) i).hom ≫
        (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom)
      y =
    PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y) ≫
      PresheafedSpace.Hom.stalkMap (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom y
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y)))
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
refine (pullbackRightPullbackFstIso _ _ _).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 z)) (pullback.fst (𝒰.f y) (𝒰.f x))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.t k i).base)

Tactic:
refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
      rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_1
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z =
    (pullbackSymmetry (𝒰.f j) (𝒰.f i)).hom ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f

Tactic:
rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t

Tactic:
𝒰.gluedCover.isOpen_iff

Goal state after:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
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
i j : 𝒰.I₀
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    (gluing 𝒰 f g).V (i, j)

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

Goal state after:
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 j : 𝒰.I₀
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) (𝒰.f j) ⟶ (gluing 𝒰 f g).V (i, j)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
⊢ IsEmpty ↥Z

Tactic:
refine ⟨fun z ↦ ?_⟩
  fapply eq_bot_iff.mp <| disjoint_iff.mp <| disjoint_opensRange_sigmaι g i j hij
  · exact (a ≫ Sigma.ι g i).base z
  · exact ⟨⟨a.base z, rfl⟩, ⟨b.base z, by rw [← Scheme.Hom.comp_apply, h.w]⟩⟩

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
i j : 𝒰.I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯

Tactic:
simp [gluedLiftPullbackMap]

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
i j : 𝒰.I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.snd s.fst (𝒰.f j)

Tactic:
simp [gluedLiftPullbackMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e : (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨ix, x⟩ = (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨iy, y⟩
this : (α ix) x = (α iy) y
h : ¬ix = iy
⊢ False

Tactic:
exact Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl

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

Goal state before:
pp: case op.op.fst
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
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) ≫
      D.ιInvAppπApp U (unop (op (WalkingMultispan.left (j, k)))) =
    D.ιInvAppπApp U (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
              congr 1

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

Goal state before:
pp: case 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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map ((pullback.fst (D.f j i) (D.f j k)).base ≫ (D.t j i).base ≫ (D.f i j).base)).1 U))) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
                (pullback (D.f j k) (D.f j i)).presheaf).map
            (eqToHom ⋯) ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map ((pullback.fst (D.f k i) (D.f k j)).base ≫ (D.t k i).base ≫ (D.f i k).base)).1 U)) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
Opens.map_comp_obj,

Goal state after:
case 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
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).obj
              ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))))) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
                (pullback (D.f j k) (D.f j i)).presheaf).map
            (eqToHom ⋯) ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map (pullback.fst (D.f k i) (D.f k j)).base).obj
                    ((Opens.map (D.t k i).base).obj ((Opens.map (D.f i k).base).obj U)))) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)
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
⊢ coprod.inr ≫
      coprodComparison Scheme.Spec (op R) (op S) ≫
        Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv) =
    coprod.inr ≫ coprodSpec ↑R ↑S

Tactic:
· rw [coprodComparison_inr_assoc, coprodSpec, coprod.inr_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inr,
        limit.isoLimitCone_inv_π]
      rfl

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
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [reassoc_of% hα₁, homOfLE_tAux F _ _ fi fj, Iso.hom_inv_id_assoc, reassoc_of% hα₂]

Goal state after:
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
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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 := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f

Tactic:
rintro X Y f ι U hU H
    let 𝒰 := Y.openCoverOfIsOpenCover U hU
    apply of_openCover 𝒰.affineRefinement.openCover
    rintro ⟨i, j⟩
    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
    rw [← Q.cancel_left_of_respectsIso (𝒰.pullbackCoverAffineRefinementObjIso f _).inv,
      𝒰.pullbackCoverAffineRefinementObjIso_inv_pullbackHom]
    exact of_isPullback (.of_hasPullback _ _) this

Goal state after:
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 <;> simp [diagonalCover, Cover.pullbackHom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2
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, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
        ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst) =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      pullback.fst ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
        ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨i, (j, j)⟩.fst)
⊢ (pullback.congrHom ⋯ ⋯ ≪≫
          pullbackDiagonalMapIso f (𝒰.f ⟨i, (j, j)⟩.fst) ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1)
              ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.2) ≪≫
            (asIso (pullback.diagonal ((𝒱 ⟨i, (j, j)⟩.fst).f ⟨i, (j, j)⟩.snd.1))).symm).hom ≫
      (Arrow.mk (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))).hom =
    (Arrow.mk (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩))).hom ≫
      (Iso.refl (Arrow.mk (pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩))).right).hom

Tactic:
dsimp [Cover.pullbackHom] at H ⊢

Goal state after:
case refine_2
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.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫ 𝟙 ((diagonalCover f 𝒰 𝒱).X ⟨i, (j, j)⟩)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hxa : x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
s : ↑Γ(X, ↑V₁)
s' : ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
hBss' : X.basicOpen s = X.basicOpen s'
hBx : x ∈ X.basicOpen s
this✝¹ :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
this✝ : IsLocalization.Away r' ↑Γ(Y, Y.basicOpen r')
this : IsLocalization.Away s' ↑Γ(X, X.basicOpen s')
ers : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
heq :
  Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') ⋯ =
    Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
        ⋯ ≫
      CommRingCat.ofHom
        (algebraMap
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))))
          ↑(X.presheaf.1 (Opposite.op (X.basicOpen s'))))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) ers))

Tactic:
rw [f.appLE_congr _ hBrr' hBss' (fun f => P f.hom), heq]
    apply hPa _ s' _
    rw [U₂.2.appLE_eq_away_map f V₂.2]
    exact hPl _ _ _ _ h₂

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (x * (algebraMap R S) ↑m) ^ n.succ = (algebraMap R S) y ^ n.succ := congr_arg (fun x ↦ x ^ n.succ) hx
⊢ x = 0

Tactic:
simp only [mul_pow, e, zero_mul, ← map_pow] at hx'

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : 0 = (algebraMap R S) (y ^ n.succ)
⊢ x = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
⊢ (∀ (i : PrimeSpectrum R), ↑(Order.height i) ≤ n) ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n

Tactic:
refine ⟨fun h p hp ↦ ?_, fun h p ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ (i : PrimeSpectrum R), ↑(Order.height i) ≤ n
p : Ideal R
hp : p.IsPrime
⊢ ↑p.height ≤ n

case refine_2
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n
p : PrimeSpectrum R
⊢ ↑(Order.height p) ≤ n
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
⊢ ↑(⨆ (_ : I ≠ ⊤), I.height) ≤ ringKrullDim R

Tactic:
by_cases h : I = ⊤

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
h : I = ⊤
⊢ ↑(⨆ (_ : I ≠ ⊤), I.height) ≤ ringKrullDim R

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
h : ¬I = ⊤
⊢ ↑(⨆ (_ : I ≠ ⊤), I.height) ≤ ringKrullDim R
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↥(Spec R)
hx : x ∈ ⊤
hs : (CommRingCat.Hom.hom (Scheme.ΓSpecIso R).inv) ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) s) = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply] at hs

Goal state after:
case h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↥(Spec R)
hx : x ∈ ⊤
hs : s = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ IsOpenImmersion f✝ ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
        stalkwise fun {R S} [CommRing R] [CommRing S] x ↦ Function.Bijective ⇑x)
      f✝

Tactic:
exact IsOpenImmersion.iff_isIso_stalkMap.trans
    (and_congr Iff.rfl (forall_congr' fun x ↦ ConcreteCategory.isIso_iff_bijective _))

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
⊢ ↑Z ∩ ↑↑U ⊆ ↑I.support ∩ ↑↑U ↔ ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
coe_support_inter,

Goal state after:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
⊢ ↑Z ∩ ↑↑U ⊆ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ↔ ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
x : ↥X
⊢ IsPreimmersion (X.fromSpecResidueField x)

Tactic:
by
  dsimp only [Scheme.fromSpecResidueField]
  rw [IsPreimmersion.comp_iff]
  infer_instance

Goal state after: