Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: case h₀.h₀
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
        pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.fst f (𝒰.f i) =
    ((pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
            (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
          iso.inv) ≫
        pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.fst f (𝒰.f i)

pp: case h₁
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
        pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.snd f (𝒰.f i) =
    ((pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
            (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
          iso.inv) ≫
        pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.snd f (𝒰.f i)

pp: case h₁.h₀
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
        pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.fst f (𝒰.f j) =
    ((pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
            (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
          iso.inv) ≫
        pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.fst f (𝒰.f j)

pp: case h₁
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
        pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.snd f (𝒰.f j) =
    ((pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
            (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
          iso.inv) ≫
        pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.snd f (𝒰.f j)

Tactic:
<;>

Goal state after:
case h₀.h₀
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
        pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.fst f (𝒰.f i) =
    ((pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
            (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
          iso.inv) ≫
        pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.fst f (𝒰.f i)

case h₁
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
        pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.snd f (𝒰.f i) =
    ((pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
            (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
          iso.inv) ≫
        pullback.fst (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.snd f (𝒰.f i)

case h₁.h₀
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
        pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.fst f (𝒰.f j) =
    ((pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
            (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
          iso.inv) ≫
        pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.fst f (𝒰.f j)

case h₁
P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅
  pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) := ⋯
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ (pullback.lift (pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯)
          (pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯) ⋯ ≫
        pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.snd f (𝒰.f j) =
    ((pullback.map f (𝒰.f k) f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) (𝟙 Y)
            (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯) (𝟙 X) ⋯ ⋯ ≫
          iso.inv) ≫
        pullback.snd (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j))) ≫
      pullback.snd f (𝒰.f j)