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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ IsPullback (resLE g UX UY ⋯) (resLE iY UT UY ⋯) (resLE iX US UX hUSX) (resLE f US UT hUST)

Tactic:
by
  refine .paste_horiz (v₁₂ := iY.resLE _ _
    ((g.preimage_mono hUSX).trans_eq congr(($H.w) ⁻¹ᵁ US) :)) ?_ ?_
  · refine (IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_).flip
    simp only [Scheme.opensRange_homOfLE, ← Scheme.Hom.comp_preimage, Scheme.Hom.resLE_comp_ι]
    rw [Scheme.Hom.comp_preimage, ← (g ⁻¹ᵁ UX).ι.image_injective.eq_iff]
    simp only [Scheme.Hom.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι]
    simp [hUY]
  · refine .of_bot ?_ ?_ (isPullback_morphismRestrict f US)
    · simpa using (isPullback_morphismRestrict g UX).paste_vert H
    · simp [← cancel_mono US.ι, H.w]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Bijective ⇑(toOpenₗ R M ⊤)

Tactic:
have : IsLocalizedModule ⊥ (toOpenₗ R M ⊤) := by
    convert! (inferInstance : IsLocalizedModule (.powers 1) (toOpenₗ R M (basicOpen 1)))
    rw [PrimeSpectrum.basicOpen_one, Submonoid.powers_one]
  refine ⟨fun x y e ↦ by simpa using (IsLocalizedModule.eq_iff_exists ⊥ _).mp e, fun x ↦ ?_⟩
  obtain ⟨⟨x, _, rfl⟩, rfl⟩ := IsLocalizedModule.mk'_surjective ⊥ (toOpenₗ R M ⊤) x
  exact ⟨x, (IsLocalizedModule.mk'_one ..).symm⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj U)) ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app U =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← StructureSheaf.algebraMap_self_map _ U _ (homOfLE le_top).op, Category.assoc,
    NatTrans.naturality _ (homOfLE (le_top (a := U.unop))).op,
    ← unop_locallyRingedSpaceAdjunction_counit_app']

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of ↑(unop (op (CommRingCat.of R)))))).unop ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app (op ⊤) ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ Spec.map ((Scheme.ΓSpecIso R).inv ≫ (Scheme.ΓSpecIso R).hom) = 𝟙 (Spec R)

Tactic:
Iso.inv_hom_id,

Goal state after:
R : CommRingCat
⊢ Spec.map (𝟙 R) = 𝟙 (Spec R)
Module: Mathlib.CategoryTheory.GlueData

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

Tactic:
simp [t_fac, t_fac_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

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

Tactic:
simp [t_fac, t_fac_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
ϕ : R ⟶ R
⊢ map ϕ = 𝟙 (Spec R) ↔ ϕ = 𝟙 R

Tactic:
simp [← map_inj]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) y = x

Tactic:
simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]

Goal state after:
D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) y = x
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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s t : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩ + ↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) =
    (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) +
      (Localizations.comapFun f ↑x✝) (↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩)

Tactic:
map_add

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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s t : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) +
      (Localizations.comapFun f ↑x✝) (↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) =
    (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) +
      (Localizations.comapFun f ↑x✝) (↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫
      pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.snd gA gB =
    pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.fst (mk gB).hom f

Tactic:
← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).hom ≫
      Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫
        pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.snd gA gB =
    Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).hom ≫
      pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.fst (mk gB).hom f
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case e'_3
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
e_1✝ : ↑((Opens.toTopCat (of α)).obj (U i)) = ↑((ofOpenSubsets U).U i)
⊢ ⇑(ConcreteCategory.hom (U i).inclusion') ⁻¹' ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s =
    ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s

Tactic:
← ι_fromOpenSubsetsGlue,

Goal state after:
case e'_3
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
e_1✝ : ↑((Opens.toTopCat (of α)).obj (U i)) = ↑((ofOpenSubsets U).U i)
⊢ ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i ≫ fromOpenSubsetsGlue U)) ⁻¹'
      ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s =
    ⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫ pullback.snd (pullback.fst gA gB ≫ gA) f =
    pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f

Tactic:
← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).hom ≫
      Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫ pullback.snd (pullback.fst gA gB ≫ gA) f =
    Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).hom ≫
      pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
      ((PresheafedSpace.forget CommRingCat).mapIso
            (SheafedSpace.forgetToPresheafedSpace.mapIso
                (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                  D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫
              D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace) ≪≫
          D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.gluedIso
            (PresheafedSpace.forget CommRingCat)).inv =
    (D.ι i).base

Tactic:
Iso.trans_inv,

Goal state after:
D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
      (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.gluedIso
            (PresheafedSpace.forget CommRingCat)).inv ≫
        ((PresheafedSpace.forget CommRingCat).mapIso
            (SheafedSpace.forgetToPresheafedSpace.mapIso
                (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                  D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫
              D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace)).inv =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (SheafedSpace.forgetToPresheafedSpace.mapIso
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                D.toLocallyRingedSpaceGlueData.isoSheafedSpace) ≪≫
            D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace).inv =
    (D.ι i).base

Tactic:
Iso.trans_inv,

Goal state after:
D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          (SheafedSpace.forgetToPresheafedSpace.mapIso
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                D.toLocallyRingedSpaceGlueData.isoSheafedSpace)).inv) =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          SheafedSpace.forgetToPresheafedSpace.map
            (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                D.toLocallyRingedSpaceGlueData.isoSheafedSpace).inv) =
    (D.ι i).base

Tactic:
Iso.trans_inv,

Goal state after:
D : GlueData
i : D.J
⊢ (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i) ≫
      (PresheafedSpace.forget CommRingCat).map
        (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv ≫
          SheafedSpace.forgetToPresheafedSpace.map
            (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
              (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv)) =
    (D.ι i).base
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫ D.isoCarrier.inv =
    (D.ι i).base

Tactic:
delta isoCarrier
  rw [Iso.trans_inv, GlueData.ι_gluedIso_inv_assoc, Functor.mapIso_inv, Iso.trans_inv,
    Functor.mapIso_inv, Iso.trans_inv, SheafedSpace.forgetToPresheafedSpace_map,
    PresheafedSpace.forget_map,
    PresheafedSpace.forget_map, ← PresheafedSpace.comp_base, ← Category.assoc,
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι_isoPresheafedSpace_inv i]
  dsimp
  rw [← Category.assoc, ← PresheafedSpace.comp_base,
    ← InducedCategory.comp_hom, D.toLocallyRingedSpaceGlueData.ι_isoSheafedSpace_inv i,
    ← PresheafedSpace.comp_base]
  change (_ ≫ D.isoLocallyRingedSpace.inv).base = _
  rw [D.ι_isoLocallyRingedSpace_inv i]

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 : 𝒰.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
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i

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

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

Tactic:
by
  simp only [t'_fst_fst_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ Epi (fromGlued 𝒰).base

Tactic:
TopCat.epi_iff_surjective

Goal state after:
X : Scheme
𝒰 : X.OpenCover
⊢ Function.Surjective ⇑(fromGlued 𝒰)
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
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
        (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t' k i j).c.app (op U) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))

Tactic:
· rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc,
      (D.t' k i j).c.naturality_assoc]
    simp_rw [← Category.assoc]
    dsimp
    rw [← comp_c_app, congr_app (D.t_fac k i j), comp_c_app]
    dsimp
    simp_rw [Category.assoc]
    rw [IsOpenImmersion.inv_naturality, IsOpenImmersion.inv_naturality_assoc,
      IsOpenImmersion.app_inv_app'_assoc]
    · simp_rw [← (𝖣.V (k, i)).presheaf.map_comp]; rfl
    rintro x ⟨y, -, eq⟩
    replace eq := ConcreteCategory.congr_arg (𝖣.t i k).base eq
    change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x at eq
    rw [𝖣.t_inv, id_base, TopCat.id_app] at eq
    subst eq
    use (inv (D.t' k i j)).base y
    change (inv (D.t' k i j) ≫ π₁ k, i, j).base y = _
    congr 3
    rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
⊢ Epi f.base

Tactic:
TopCat.epi_iff_surjective

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
⊢ Function.Surjective ⇑f
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
⊢ Nonempty (IsColimit c')

Tactic:
let fi (j : WalkingPair) : WalkingPair.casesOn j X Y ⟶ S := WalkingPair.casesOn j f g

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ Nonempty (IsColimit c')
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ limit.lift (D.diagramOverOpen U)
        { pt := (D.U i).presheaf.obj (op U), π := { app := fun j ↦ D.ιInvAppπApp U (unop j), naturality := ⋯ } } ≫
      D.diagramOverOpenπ U i =
    (D.U i).presheaf.map (eqToHom ⋯)

Tactic:
limit.lift_π

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ { pt := (D.U i).presheaf.obj (op U), π := { app := fun j ↦ D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app
      (op (WalkingMultispan.right i)) =
    (D.U i).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: 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
V : ↑Y.affineOpens
⊢ Q (f ∣_ ↑V)

Tactic:
induction V using of_affine_open_cover U hU with
  | basicOpen U r h =>
    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
  | openCover U s hs H =>
    apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
    intro ⟨r, hr⟩
    obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
  | hU i => exact hU' i

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

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

Tactic:
erw [D.ι_image_preimage_eq i j U]
      infer_instance

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
⊢ IsDominant g

Tactic:
isDominant_iff,

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : DenseRange ⇑(f ≫ g)
⊢ DenseRange ⇑g
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
inst✝ : IsOpenImmersion g
⊢ IsDominant f

Tactic:
isDominant_iff,

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : DenseRange ⇑(f ≫ g)
inst✝ : IsOpenImmersion g
⊢ DenseRange ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
⊢ P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)

Tactic:
refine ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
⊢ P.universally (𝒰.f i ≫ f)

case refine_2
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
⊢ P.universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
this : IsIso (Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE (e.hom ≫ f) ⊤ ↑U ⋯))

Tactic:
rw [← Scheme.Hom.appLE_comp_appLE _ _ ⊤ (e.hom ''ᵁ U) U.1 le_top (e.hom.preimage_image_eq _).ge,
      CommRingCat.hom_comp, h₁.cancel_right_isIso]

Goal state after:
case h₁
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝ : IsAffine Z
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
U : ↑X.affineOpens
this : IsIso (Scheme.Hom.appLE e.hom (e.hom ''ᵁ ↑U) ↑U ⋯)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (e.hom ''ᵁ ↑U) ⋯))
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: ⊢ @IsPreimmersion =
    @SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding

Tactic:
by
  ext
  rw [isPreimmersion_iff]
  rfl

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

Goal state before:
pp: case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯

Tactic:
· introv H h₁ h₂
    let g : pullback f₁ f₂ ⟶ X := pullback.fst _ _ ≫ f₁
    have e := g.isOpenEmbedding.isEmbedding.toHomeomorph
    rw [IsOpenImmersion.range_pullback_to_base_of_left] at e
    simp_rw [isCompact_iff_compactSpace] at H
    exact @Homeomorph.compactSpace _ _ _ _
        (H ⟨_, isAffineOpen_opensRange f₁⟩ ⟨_, isAffineOpen_opensRange f₂⟩) e.symm

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparatedSpace ↥Y
inst✝ : QuasiSeparated f
⊢ QuasiSeparatedSpace ↥X

Tactic:
quasiSeparatedSpace_iff_quasiSeparated

Goal state after:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (terminal.from X)