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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
trans hU.fromSpec ⁻¹' (⨆ f : s, X.basicOpen (f : Γ(X, U))).1 = hU.fromSpec ⁻¹' U.1
    · refine ⟨fun h => by rw [h], ?_⟩
      intro h
      apply_fun Set.image hU.fromSpec at h
      rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.range_fromSpec]
        at h
      simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
      ext1
      refine Set.Subset.antisymm ?_ h
      simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
      intro x _
      exact X.basicOpen_le x
    · simp only [Opens.iSup_def, Set.preimage_iUnion]
      congr! 1
      · refine congr_arg (Set.iUnion ·) ?_
        ext1 x
        exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)
      · exact congr_arg Opens.carrier hU.fromSpec_preimage_self

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
hik : ¬i = k
hjk : j = k
⊢ ((if hij : i = j then
        (pullbackSymmetry (D.f' i j) (D.f' i k)).hom ≫
          pullback.map (D.f' i k) (D.f' i j) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i j) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
        else
          if hjk : j = k then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
          else
            pullback.map (D.f' i j) (D.f' i k) (D.f i j hij) (D.f i k hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i j k hij hik hjk ≫
                pullback.map (D.f j k hjk) (D.f j i ⋯) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯) ≫
      (if hij : j = k then
          (pullbackSymmetry (D.f' j k) (D.f' j i)).hom ≫
            pullback.map (D.f' j i) (D.f' j k) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : j = i then
            have this := ⋯;
            pullback.fst (D.f' j k) (D.f' j i) ≫
              eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
          else
            if hjk : k = i then
              have this := ⋯;
              pullback.fst (D.f' j k) (D.f' j i) ≫
                eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
            else
              pullback.map (D.f' j k) (D.f' j i) (D.f j k hij) (D.f j i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' j k i hij hik hjk ≫
                  pullback.map (D.f k i hjk) (D.f k j ⋯) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                    ⋯) ≫
        if hij : k = i then
          (pullbackSymmetry (D.f' k i) (D.f' k j)).hom ≫
            pullback.map (D.f' k j) (D.f' k i) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : k = j then
            have this := ⋯;
            pullback.fst (D.f' k i) (D.f' k j) ≫
              eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
          else
            if hjk : i = j then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k j) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
            else
              pullback.map (D.f' k i) (D.f' k j) (D.f k i hij) (D.f k j hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' k i j hij hik hjk ≫
                  pullback.map (D.f i j hjk) (D.f i k ⋯) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                    ⋯) =
    𝟙 (pullback (D.f' i j) (D.f' i k))

Tactic:
subst hjk
      ext <;> simp [hij, Ne.symm hij, fst_eq_snd_of_mono_eq]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ (((((((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
                  ofHom
                    {
                      toFun := fun x ↦
                        ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
                      continuous_toFun := ⋯ }) ≫
                (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
              (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').hom) ≫
            ofHom
              {
                toFun := fun x ↦
                  ⟨(⟨↑((ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩,
                continuous_toFun := ⋯ }) ≫
          (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').inv) ≫
        (pullbackIsoProdSubtype (h.V k i).inclusion' (h.V k j).inclusion').hom) ≫
      ofHom
        {
          toFun := fun x ↦
            ⟨(⟨↑((ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩,
          continuous_toFun := ⋯ } =
    𝟙 (pullback (h.V i j).inclusion' (h.V i k).inclusion') ≫
      (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom

Tactic:
simp only [Iso.inv_hom_id_assoc, Category.assoc, Category.id_comp]

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
⊢ (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
      ofHom
          {
            toFun := fun x ↦
              ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
            continuous_toFun := ⋯ } ≫
        ofHom
            {
              toFun := fun x ↦
                ⟨(⟨↑((ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t j k)) (↑x).1), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          ofHom
            {
              toFun := fun x ↦
                ⟨(⟨↑((ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t k i)) (↑x).1), ⋯⟩,
              continuous_toFun := ⋯ } =
    (pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x y : ↑(ofOpenSubsets U).glued
e : (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x = (ConcreteCategory.hom (fromOpenSubsetsGlue U)) y
⊢ x = y

Tactic:
obtain ⟨i, ⟨x, hx⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
y : ↑(ofOpenSubsets U).glued
i : (ofOpenSubsets U).J
x : ↑(of α)
hx : x ∈ U i
e :
  (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) y
⊢ (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx⟩ = y
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]

Goal state after:
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
⊢ D.ιInvAppπApp U (WalkingMultispan.left (j, k)) =
    D.ιInvAppπApp U (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

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

Goal state after:
case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ D.ιInvAppπApp U (WalkingMultispan.left (j, k)) =
    D.ιInvAppπApp U (WalkingMultispan.right ((MultispanShape.prod D.J).snd (j, k))) ≫
      (D.diagramOverOpen U).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (j, k)))
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),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        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:
intro X'

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' : Scheme
⊢ ∀ {Y' : Scheme} (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        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.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
i : J
⊢ t F i i = 𝟙 ↑(V F i i)

Tactic:
refine (Scheme.Opens.iSupOpenCover _).hom_ext _ _ fun k ↦ ?_
  simp only [Category.comp_id, ← cancel_mono (Scheme.Opens.ι _), Category.assoc,
    IsOpenImmersion.lift_fac, Scheme.Cover.ι_glueMorphisms, t, tAux, V]
  simp [Scheme.Opens.iSupOpenCover, Iso.inv_comp_eq, Subsingleton.elim k.2.1 k.2.2]

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 : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
trans pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι _

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j

X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
⊢ IsZariskiLocalAtTarget P

Tactic:
by
  refine .mk_of_iff_of_zeroHypercover fun {X Y} f 𝒰 ↦ ?_
  refine ⟨fun hf i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange _ _)).mp (restrict _ _ hf),
    fun h ↦ ?_⟩
  refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange <| .ulift 𝒰) ?_
  exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h _)

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

Goal state before:
pp: case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)

Tactic:
intro _

Goal state after:
case h₁
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ : Scheme
⊢ ∀ {Y Z : Scheme} (e : X✝ ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], of P f → of P (e.hom ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)

Tactic:
intro _

Goal state after:
case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ : Scheme
⊢ ∀ {Y Z : Scheme} (e : Y ≅ Z) (f : X✝ ⟶ Y) [inst : IsAffine Y], of P f → of P (f ≫ e.hom)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

Tactic:
by
  rw [← @cancel_mono
          (f := (componentwiseDiagram 𝖣.diagram.multispan _).map
            (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 _) ..]
  · simp_rw [Category.assoc]
    rw [limit.w_assoc]
    erw [limit.lift_π_assoc]
    rw [Category.comp_id, Category.comp_id]
    change _ ≫ _ ≫ (_ ≫ _) ≫ _ = _
    rw [congr_app (D.t_id _), id_c_app]
    simp_rw [Category.assoc]
    rw [← Functor.map_comp_assoc]
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): change `rw` to `erw`
    erw [IsOpenImmersion.inv_naturality_assoc]
    erw [IsOpenImmersion.app_invApp_assoc]
    iterate 3 rw [← Functor.map_comp_assoc]
    rw [NatTrans.naturality_assoc]
    erw [← (D.V (i, j)).presheaf.map_comp]
    convert!
      limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (i, j)))
  · rw [Category.comp_id]
    apply +allowSynthFailures mono_comp
    change Mono ((_ ≫ D.f j i).c.app _)
    rw [comp_c_app]
    apply +allowSynthFailures mono_comp
    · erw [D.ι_image_preimage_eq i j U]
      infer_instance
    · have : IsIso (D.t i j).c := by apply c_isIso_of_iso
      infer_instance

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
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₀
⊢ pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      (diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩ ≫ pullback.fst f f =
    pullback.snd (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫
      (diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩ ≫ pullback.snd f f

Tactic:
rw [← pullback.condition_assoc, ← pullback.condition_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 : 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₀
⊢ pullback.fst (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫ pullback.diagonal f ≫ pullback.fst f f =
    pullback.fst (pullback.diagonal f) ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ≫ pullback.diagonal f ≫ pullback.snd f f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

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

Tactic:
· rw [← limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))),
      ← Category.assoc, Category.id_comp]
    congr 1
    simp_rw [Category.assoc]
    apply π_ιInvApp_π

Goal state after:
case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))
Module: Mathlib.AlgebraicGeometry.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)
this✝ : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
this :
  f =
    X.topIso.inv ≫
      (X.isoOfEq this✝).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom
⊢ P
    (X.topIso.inv ≫
      (X.isoOfEq this✝).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom)

Tactic:
cancel_left_of_respectsIso (P := P),

Goal state after:
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)
this✝ : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
this :
  f =
    X.topIso.inv ≫
      (X.isoOfEq this✝).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom
⊢ P ((f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₃
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), SpecializingMap ((U i).carrier.restrictPreimage f)) → SpecializingMap f

Tactic:
introv hU _ hsp

Goal state after:
case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp : ∀ (i : ι), SpecializingMap ((U i).carrier.restrictPreimage f)
⊢ SpecializingMap f
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: ⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Surjective ⇑e.toRingHom

Tactic:
intro _

Goal state after:
R✝ : Type u_1
⊢ ∀ {S : Type u_1} [inst : CommRing R✝] [inst_1 : CommRing S] (e : R✝ ≃+* S), Function.Surjective ⇑e.toRingHom
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (pullback.diagonal (U.ι ≫ f) ≫ g f U)

Tactic:
← pullback.comp_diagonal

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (U.ι ≫ pullback.diagonal f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (pullback.diagonal (U.ι ≫ f) ≫ g f U)

Tactic:
rw [← pullback.comp_diagonal]

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (U.ι ≫ pullback.diagonal f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
apply IsStableUnderBaseChange.mk (locally_respectsIso hPi)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T) →
      Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap S (S ⊗[R] T))