Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case e'_3
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₀
e_2✝ :
  pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) =
    pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom 𝒰 f i) ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom 𝒰 f i)
⊢ (pullbackDiagonalMapIso f (𝒰.f i) ((𝒰' i).f j) ((𝒰' i).f k)).inv ≫
      pullback.snd (pullback.diagonal f)
        (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.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
ext1

Goal state after:
case e'_3.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₀
e_2✝ :
  pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) =
    pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom 𝒰 f i) ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom 𝒰 f i)
⊢ ((pullbackDiagonalMapIso f (𝒰.f i) ((𝒰' i).f j) ((𝒰' i).f k)).inv ≫
        pullback.snd (pullback.diagonal f)
          (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.fst ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) =
    pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i) ≫
      pullback.fst ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))

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₀
e_2✝ :
  pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) =
    pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom 𝒰 f i) ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom 𝒰 f i)
⊢ ((pullbackDiagonalMapIso f (𝒰.f i) ((𝒰' i).f j) ((𝒰' i).f k)).inv ≫
        pullback.snd (pullback.diagonal f)
          (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.snd ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) =
    pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i) ≫
      pullback.snd ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))