Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
l : 𝒰.I₀
gi : l ⟶ i
gj : l ⟶ j
y : ↥(𝒰.X l)
hxij :
  (𝒰.trans fi) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.trans fj) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
this :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
⊢ (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map gi)) y =
    (pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)

pp: case refine_2
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
l : 𝒰.I₀
gi : l ⟶ i
gj : l ⟶ j
y : ↥(𝒰.X l)
hxij :
  (𝒰.trans fi) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.trans fj) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
this :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
⊢ (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map gj)) y =
    (pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)

Tactic:
<;>

Goal state after:
case refine_1
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
l : 𝒰.I₀
gi : l ⟶ i
gj : l ⟶ j
y : ↥(𝒰.X l)
hxij :
  (𝒰.trans fi) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.trans fj) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
this :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
⊢ (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map gi)) y =
    (pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)

case refine_2
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
l : 𝒰.I₀
gi : l ⟶ i
gj : l ⟶ j
y : ↥(𝒰.X l)
hxij :
  (𝒰.trans fi) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.trans fj) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
this :
  (𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)) =
    (𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y))
⊢ (ConcreteCategory.hom ((𝒰.functorOfLocallyDirected ⋙ forget).map gj)) y =
    (pullback.snd (𝒰.f i) (𝒰.f j)) ((pullback.lift (𝒰.trans gi) (𝒰.trans gj) ⋯) y)