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

Goal state before:
pp: case h₀
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ ≫ pullback.fst f g =
    ((pullbackSymmetry f (𝒰.f i ≫ g)).hom ≫
        pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯ ≫ (pullbackSymmetry g f).hom) ≫
      pullback.fst f g

Tactic:
simp

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✝ Y✝ Z✝ : Scheme
e✝ : X✝ ≅ Y✝
f✝ : Y✝ ⟶ Z✝
inst✝ : IsAffine Z✝
⊢ of P f✝ → of P (e✝.hom ≫ f✝)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ ≫ pullback.snd f g =
    ((pullbackSymmetry f (𝒰.f i ≫ g)).hom ≫
        pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯ ≫ (pullbackSymmetry g f).hom) ≫
      pullback.snd f g

Tactic:
simp

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 : 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✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
f✝ : X✝ ⟶ Y✝
inst✝ : IsAffine Y✝
⊢ of P f✝ → of P (f✝ ≫ e✝.hom)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰X : X.OpenCover
𝒰Y : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰X.I₀
j : 𝒰Y.I₀
⊢ pullback.map (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) f g (𝒰X.f (i, j).1) (𝒰Y.f (i, j).2) (𝟙 Z) ⋯ ⋯ ≫
      pullback.fst f g =
    ((Iso.refl (pullback (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g))).hom ≫
        (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun x ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
          ((Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀).symm (i, j))) ≫
      pullback.fst f g

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰X : X.OpenCover
𝒰Y : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰X.I₀
j : 𝒰Y.I₀
⊢ pullback.map (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) f g (𝒰X.f (i, j).1) (𝒰Y.f (i, j).2) (𝟙 Z) ⋯ ⋯ ≫
      pullback.snd f g =
    ((Iso.refl (pullback (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g))).hom ≫
        (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun x ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
          ((Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀).symm (i, j))) ≫
      pullback.snd f g

Tactic:
simp

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
pf✝⁵ : 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)
pf✝⁴ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝³ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝² : IsOpenImmersion (F.map fi)
pf✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
pf✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : 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)
this : 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)

Tactic:
exact (Scheme.homOfLE_ι _ _).symm

Goal state after:
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
h : fWX ≫ fXZ = fWY ≫ fYZ
this : IsIso (pullback.lift fWX fWY h)
⊢ (asIso (pullback.lift fWX fWY h)).hom ≫ pullback.fst fXZ fYZ = fWX

Tactic:
simp

Goal state after:
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
h : fWX ≫ fXZ = fWY ≫ fYZ
this : IsIso (pullback.lift fWX fWY h)
⊢ (asIso (pullback.lift fWX fWY h)).hom ≫ pullback.snd fXZ fYZ = fWY

Tactic:
simp

Goal state after:
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
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
⊢ (𝒰.f i ≫ fXZ) ≫ 𝟙 Z = 𝒰.f i ≫ fXZ

Tactic:
simp

Goal state after:
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
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
⊢ fYZ ≫ 𝟙 Z = 𝟙 Y ≫ fYZ

Tactic:
simp

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
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

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
s : Cocone F
i j : (glueData F).J
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ ((𝒱 I.fst).f I.snd.1 ≫ Cover.pullbackHom 𝒰 f I.fst) ≫ 𝒰.f I.fst =
    ((𝒱 I.fst).f I.snd.1 ≫ pullback.fst f (𝒰.f I.fst)) ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ ((𝒱 I.fst).f I.snd.2 ≫ Cover.pullbackHom 𝒰 f I.fst) ≫ 𝒰.f I.fst =
    ((𝒱 I.fst).f I.snd.2 ≫ pullback.fst f (𝒰.f I.fst)) ≫ f

Tactic:
simp

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
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g
s : PullbackCone f✝ g
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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
⊢ Set.range ⇑(Scheme.Hom.opensRange g).ι = Set.range ⇑g

Tactic:
simp

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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h : ((glueData F).ι i) xi = ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x
⊢ i = (equivShrink J) ↓i

Tactic:
simp

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

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
H : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
⊢ (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f

Tactic:
hf

Goal state after:
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
H : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hf : ∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)
⊢ Function.Surjective f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case convert_1
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
⊢ pullback.diagonal f ≫ 𝟙 (pullback.diagonalObj f) = 𝟙 X ≫ pullback.diagonal f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (x ⊗ₜ[R] 1)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↑(of S)
⊢ x = (lmul' R) (1 ⊗ₜ[R] x)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝ : M.Over S
f : T ⟶ S
⊢ pullback.snd (M ↘ S) (𝟙 S) ≫ 𝟙 S = pullback (M ↘ S) (𝟙 S) ↘ S

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid S

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid S

Tactic:
simp

Goal state after:
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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
hf

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
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.1 ≫ f) ≫ 𝟙 Y = 𝒰.f i.1 ≫ f

Tactic:
simp

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.2 ≫ f) ≫ 𝟙 Y = 𝒰.f i.2 ≫ f

Tactic:
simp

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y) = 𝟙 (𝒰.X i.1) ≫ 𝒰.f i.1

Tactic:
simp

Goal state after: