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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst

Tactic:
refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun x => ?_

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base = s.fst.base

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑X)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.fst.c.app x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd

Tactic:
refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun x => ?_

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).base = s.snd.base

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.snd.c.app x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w.none
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ ((forget C).mapCone (pullbackConeOfLeft f g)).π.app none ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none =
    (limit.cone (cospan f.base g.base)).π.app none

Tactic:
simp only [limit.cone_x, cospan_one, Functor.mapCone_π_app, PullbackCone.condition_one,
        forget_map,
          comp_base, cospan_left, cospan_right, Functor.comp_map, cospan_map_inl, cospan_map_inr,
          diagramIsoCospan_hom_app, PullbackCone.fst_limit_cone]
        tauto

Goal state after:
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
f : R
⊢ ∀ (x : ↥(Submonoid.powers f)),
    IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) ↑x)

Tactic:
by
    simp only [Subtype.forall]
    exact Submonoid.powers_le (P := (IsUnit.submonoid _).comap (algebraMap R _)).mpr
      (isUnit_basicOpen_end ..)

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
⊢ f ∈ (⊥.colon {d • a - b • c}).radical

Tactic:
simp only [toBasicOpenₗ_mk] at h_eq

Goal state after:
case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : const a (↑b) (basicOpen f) ⋯ = const c (↑d) (basicOpen f) ⋯
⊢ f ∈ (⊥.colon {d • a - b • c}).radical
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ ((asIso t).hom ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (pullback.snd f g)).hom ≫ e.hom

Tactic:
asIso_hom,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (pullback.snd f g)).hom ≫ e.hom
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f

Tactic:
asIso_hom,

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ (Scheme.ΓSpecIso B).inv ≫ Scheme.Hom.appTop ((ΓSpec.adjunction.homEquiv X (op B)) φ.op) = φ

Tactic:
ΓSpecIso_inv_ΓSpec_adjunction_homEquiv

Goal state after:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ φ = φ
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑X.isoSpec.inv '' PrimeSpectrum.zeroLocus s = X.zeroLocus s

Tactic:
rw [← isoSpec_inv_preimage_zeroLocus, Set.image_preimage_eq]

Goal state after:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ Function.Surjective ⇑X.isoSpec.inv
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i)) =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹'
      (Set.range ⇑(ConcreteCategory.hom (D.ι j)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι i)))

Tactic:
Set.preimage_range_inter

Goal state after:
D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i)) =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i))
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:
by
  apply pullback.hom_ext <;> simp

Goal state after:
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 j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        invApp (D.f j i) ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))) ≫
          (D.U j).presheaf.map (eqToHom ⋯).op ≫ (D.f j k).c.app (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)

Tactic:
(D.f j k).c.naturality,

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        invApp (D.f j i) ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))) ≫
          (D.f j k).c.app
              (op
                ((opensFunctor (D.f j i)).obj
                  ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U)))))) ≫
            ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯).op =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ?w)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case 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.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (j, k)))

Tactic:
refine
      D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ ≫ (D.V (j, k)).presheaf.map (eqToHom ?_)

Goal state after:
case 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
⊢ (Opens.map (D.f j k).base).op.obj (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) =
    op
      ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj
        (⋯.functor.obj U))
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 : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
this✝ : IsOpenImmersion α
this : α y = x
⊢ (Hom.opensRange α).ι ≫
      pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
        (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
    (Hom.opensRange α).ι ≫
      pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
        (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2

Tactic:
← cancel_epi α.isoOpensRange.hom

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
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
this✝ : IsOpenImmersion α
this : α y = x
⊢ (Hom.isoOpensRange α).hom ≫
      (Hom.opensRange α).ι ≫
        pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
    (Hom.isoOpensRange α).hom ≫
      (Hom.opensRange α).ι ≫
        pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2
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:
← cancel_epi α.isoOpensRange.hom

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.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)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (D.ι i).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
⊢ x = y

Tactic:
delta ι Multicoequalizer.π at h2

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)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
⊢ x = y
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine ↑(e.hom ⁻¹ᵁ U)
⊢ P (f ∣_ e.hom ⁻¹ᵁ U ≫ e.hom ∣_ U)

Tactic:
P.cancel_right_of_respectsIso

Goal state after:
case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine ↑(e.hom ⁻¹ᵁ U)
⊢ P (f ∣_ e.hom ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
⊢ IsPullback fWX fWY fXZ fYZ

Tactic:
have h : fWX ≫ fXZ = fWY ≫ fYZ :=
    Scheme.Cover.hom_ext (𝒰.pullback₁ fWX) _ _ fun i ↦ by simpa using (H i).w
  suffices IsIso (lift fWX fWY h) from .of_iso_pullback ⟨h⟩ (asIso (lift _ _ h)) (by simp) (by simp)
  have H₁ (i : _) : IsIso ((openCoverOfLeft 𝒰 fXZ fYZ).pullbackHom (lift fWX fWY h) i) := by
    let f := map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp)
    have : IsPullback (fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (fst _ _) := by
      simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), f] using .of_hasPullback _ _
    have H' : IsPullback (fst fWX (𝒰.f i)) (lift (snd _ _) (fst _ _ ≫ fWY) (by simp [← h]))
        (lift fWX fWY h) f := by
      rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])]
      simpa using .of_hasPullback _ _
    convert! (inferInstance : IsIso (H'.isoPullback.inv ≫ (H i).isoPullback.hom))
    aesop (add simp [Iso.eq_inv_comp, Scheme.Cover.pullbackHom])
  exact MorphismProperty.of_zeroHypercover_target (P := .isomorphisms Scheme)
    (Scheme.Pullback.openCoverOfLeft 𝒰 fXZ fYZ) H₁

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

Goal state before:
pp: case h₁
P : AffineTargetMorphismProperty
inst✝⁵ : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝⁴ : IsAffine Z
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝³ : IsAffine U₁
inst✝² : IsAffine U₂
inst✝¹ : IsOpenImmersion f₁
inst✝ : IsOpenImmersion f₂
⊢ P (pullback.mapDesc (f₁ ≫ e.hom) (f₂ ≫ e.hom) f ≫ (pullback.congrHom ⋯ ⋯).hom)

Tactic:
P.cancel_right_of_respectsIso

Goal state after:
case h₁
P : AffineTargetMorphismProperty
inst✝⁵ : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst✝⁴ : IsAffine Z
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝³ : IsAffine U₁
inst✝² : IsAffine U₂
inst✝¹ : IsOpenImmersion f₁
inst✝ : IsOpenImmersion f₂
⊢ P (pullback.mapDesc (f₁ ≫ e.hom) (f₂ ≫ e.hom) f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case h₂
P : AffineTargetMorphismProperty
inst✝⁵ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst✝⁴ : IsAffine Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝³ : IsAffine U₁
inst✝² : IsAffine U₂
inst✝¹ : IsOpenImmersion f₁
inst✝ : IsOpenImmersion f₂
⊢ P (pullback.mapDesc f₁ f₂ f ≫ pullback.mapDesc (f₁ ≫ f) (f₂ ≫ f) e.hom ≫ (pullback.congrHom ⋯ ⋯).hom)

Tactic:
P.cancel_right_of_respectsIso

Goal state after:
case h₂
P : AffineTargetMorphismProperty
inst✝⁵ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst✝⁴ : IsAffine Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝³ : IsAffine U₁
inst✝² : IsAffine U₂
inst✝¹ : IsOpenImmersion f₁
inst✝ : IsOpenImmersion f₂
⊢ P (pullback.mapDesc f₁ f₂ f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ P ((algebraMap T (Localization.Away ((algebraMap S T) a))).comp ((algebraMap S T).comp f))

Tactic:
rw [← comp_assoc, ← this, comp_assoc]

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ P
    ((algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      ((algebraMap S (Localization.Away a)).comp 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
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this✝ : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
this :
  ∀ (a : ↑s),
    IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H : ∀ (a : ↑s), Submonoid.powers (f r) ≤ Submonoid.comap (algebraMap S (Localization.Away ↑a)) (Submonoid.powers (rₐ a))
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.Away.map R' S' f r))

Tactic:
let (a : s) : Algebra S' (Sₐ a) :=
    (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away a.val)) (H a)).toAlgebra

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this✝¹ : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
this✝ :
  ∀ (a : ↑s),
    IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H : ∀ (a : ↑s), Submonoid.powers (f r) ≤ Submonoid.comap (algebraMap S (Localization.Away ↑a)) (Submonoid.powers (rₐ a))
this : (a : ↑s) → Algebra S' (Sₐ a) :=
  fun a ↦ (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).toAlgebra
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap S' (Sₜ i)).comp (IsLocalization.Away.map R' S' f r))