Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    f

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    f
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
hab : a ≫ b = f
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f

Tactic:
· refine ⟨pullback p ((E.inter F).toPullback k), pullback.lift f a ?_,
        pullback.fst _ _, ?_, ?_, ?_⟩
    · apply pullback.hom_ext
      · apply pullback.hom_ext <;> simp [p, h₁, toPullback]
      · apply pullback.hom_ext <;> simp [p, h₂, toPullback]
    · refine ⟨k.1, pullback.snd _ _ ≫ pullback.fst _ _, ?_, ?_⟩
      · have : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = p ≫ pullback.fst _ _ ≫ pullback.fst _ _ := by
          simp [p]
        simp [this, pullback.condition_assoc, toPullback]
      · have : p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = p ≫ pullback.snd _ _ ≫ pullback.fst _ _ := by
          simp [p]
        simp [this, pullback.condition_assoc, toPullback]
    · exact ⟨k.2, a ≫ pullback.snd _ _, by simp [reassoc_of% h₁], by simp [reassoc_of% h₂]⟩
    · simp

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    f
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
hab : a ≫ b = f
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f