mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X : C
S : Presieve X
w✝ : C
hS : ∃ f, (S = ofArrows (fun x ↦ w✝) fun x ↦ f) ∧ EffectiveEpi f
this : S.regular
⊢ IsSheafFor (yoneda.obj W) S

Tactic:
obtain ⟨Y, f, rfl, hf⟩ := Presieve.regular.single_epi (R := S)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

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
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ (cylinder f g).sieve₁' i j ≤
    Sieve.pullback
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
      (E.sieve₁' i.fst j.fst)

Tactic:
sieve₁',

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ (Sieve.ofArrows (cylinder f g).Y fun j_1 ↦ (cylinder f g).toPullback j_1) ≤
    Sieve.pullback
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
      (E.sieve₁' i.fst j.fst)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ Sieve.pullback
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
      (E.sieve₁' i.fst j.fst) ≤
    (cylinder f g).sieve₁' i j

Tactic:
sieve₁',

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
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ Sieve.pullback
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
      (Sieve.ofArrows E.Y fun j_1 ↦ E.toPullback j_1) ≤
    (cylinder f g).sieve₁' i j
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
obj : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)
hom_comp :
  ∀ (i₁ i₂ i₃ : ι),
    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
        pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
      pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback
left✝¹ : φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁
left✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
⊢ ((F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
        (F.map φ.op.toLoc).toFunctor.map (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) ≫
          (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj i₂)) ≫
      (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc ⋯).hom.toNatTrans.app (obj i₂) ≫
        (F.map φ.op.toLoc).toFunctor.map (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ≫
          (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc ⋯).inv.toNatTrans.app (obj i₃) =
    (F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      (F.map φ.op.toLoc).toFunctor.map (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ≫
        (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc ⋯).inv.toNatTrans.app (obj i₃)

Tactic:
simp [← Functor.map_comp_assoc, hom_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i✝ j✝ : (cylinder f g).I₀
k : (cylinder f g).I₁ i✝ j✝
this : E.p₁ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst)
⊢ pullback.snd
        (pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (E.f i✝.fst) (E.f j✝.fst)
          (pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd))
          (pullback.fst (pullback.lift (f.h₀ j✝.fst) (g.h₀ j✝.fst) ⋯) (F.toPullback j✝.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst) =
    (cylinder f g).p₁ k ≫ pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd)

Tactic:
rw [← pullback.condition_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i✝ j✝ : (cylinder f g).I₀
k : (cylinder f g).I₁ i✝ j✝
this : E.p₁ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst)
⊢ pullback.fst
        (pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (E.f i✝.fst) (E.f j✝.fst)
          (pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd))
          (pullback.fst (pullback.lift (f.h₀ j✝.fst) (g.h₀ j✝.fst) ⋯) (F.toPullback j✝.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (E.f i✝.fst) (E.f j✝.fst)
          (pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd))
          (pullback.fst (pullback.lift (f.h₀ j✝.fst) (g.h₀ j✝.fst) ⋯) (F.toPullback j✝.snd)) (𝟙 S) ⋯ ⋯ ≫
        pullback.fst (E.f i✝.fst) (E.f j✝.fst) =
    (cylinder f g).p₁ k ≫ pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
this : E.p₂ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst)
⊢ pullback.snd
        (pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst) =
    (cylinder f g).p₂ k ≫ pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)

Tactic:
rw [← pullback.condition_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
this : E.p₂ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst)
⊢ pullback.fst
        (pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯ ≫
        pullback.snd (E.f p.fst) (E.f q.fst) =
    (cylinder f g).p₂ k ≫ pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
this : F.p₁ p.snd = pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
⊢ pullback.snd (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫
      pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst)) =
    ((cylinderHom f g).comp f).h₀ p

Tactic:
rw [← pullback.condition_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
this : F.p₁ p.snd = pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
⊢ pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫
      pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst)) =
    ((cylinderHom f g).comp f).h₀ p
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u_2
inst✝³ : Category.{v_2, u_2} A
S✝¹ : C
E✝¹ : PreZeroHypercover S✝¹
inst✝² : E✝¹.HasPullbacks
S✝ : C
E✝ : PreZeroHypercover S✝
inst✝¹ : E✝.HasPullbacks
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ A
⊢ PreOneHypercover.Homotopy (PreOneHypercover.Hom.id E.toPreOneHypercover)
    (PreOneHypercover.Hom.id E.toPreOneHypercover)

Tactic:
exact E.toPreOneHypercoverHomotopy

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f✝ : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f✝ (𝒰.f i))
i j : 𝒰.I₀
f : pullback (pullback.fst f✝ (𝒰.f i) ≫ f✝) (𝒰.f j) ⟶ pullback (𝒰.f i) (𝒰.f j) :=
  pullback.map (pullback.fst f✝ (𝒰.f i) ≫ f✝) (𝒰.f j) (𝒰.f i) (𝒰.f j) (pullback.snd f✝ (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯
⊢ pullback.fst (𝒰.f i) (𝒰.f j) ≫ inv (pullback.snd f✝ (𝒰.f i)) ≫ pullback.fst f✝ (𝒰.f i) =
    pullback.snd (𝒰.f i) (𝒰.f j) ≫ inv (pullback.snd f✝ (𝒰.f j)) ≫ pullback.fst f✝ (𝒰.f j)

Tactic:
← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ f)

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f✝ : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f✝ (𝒰.f i))
i j : 𝒰.I₀
f : pullback (pullback.fst f✝ (𝒰.f i) ≫ f✝) (𝒰.f j) ⟶ pullback (𝒰.f i) (𝒰.f j) :=
  pullback.map (pullback.fst f✝ (𝒰.f i) ≫ f✝) (𝒰.f j) (𝒰.f i) (𝒰.f j) (pullback.snd f✝ (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯
⊢ ((pullbackRightPullbackFstIso f✝ (𝒰.f j) (pullback.fst f✝ (𝒰.f i))).hom ≫ f) ≫
      pullback.fst (𝒰.f i) (𝒰.f j) ≫ inv (pullback.snd f✝ (𝒰.f i)) ≫ pullback.fst f✝ (𝒰.f i) =
    ((pullbackRightPullbackFstIso f✝ (𝒰.f j) (pullback.fst f✝ (𝒰.f i))).hom ≫ f) ≫
      pullback.snd (𝒰.f i) (𝒰.f j) ≫ inv (pullback.snd f✝ (𝒰.f j)) ≫ pullback.fst f✝ (𝒰.f j)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (pullback.fst fst (𝒰.f i)) (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯)
    (pullback.lift fst snd h) m
heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) = H'.isoPullback.inv ≫ ⋯.isoPullback.hom
⊢ IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))

Tactic:
heq

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (pullback.fst fst (𝒰.f i)) (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯)
    (pullback.lift fst snd h) m
heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) = H'.isoPullback.inv ≫ ⋯.isoPullback.hom
⊢ IsIso (H'.isoPullback.inv ≫ ⋯.isoPullback.hom)
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst✝³ : HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : ↑(F.obj { as := op S })
⊢ Presheaf.IsSheaf (J.toGrothendieck.over S) (F.presheafHom M N)

Tactic:
rw [isSheaf_iff_isSheaf_of_type,
      over_toGrothendieck_eq_toGrothendieck_comap_forget,
      ← Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck,
      Presieve.isSheaf_pretopology]
    intro X R hR
    simp only [Precoverage.toPretopology_toPrecoverage, Precoverage.mem_comap_iff,
      Over.forget_obj] at hR
    obtain ⟨R', hR'⟩ := (Sieve.overEquiv _).symm.surjective (Sieve.generate R)
    rw [Presieve.isSheafFor_iff_generate]
    apply IsPrestackFor.isSheafFor'
    simpa [Sieve.overEquiv_generate, ← Sieve.arrows_generate_map_eq_functorPushforward]
      using hF _ _ hR

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ PresheafIsGeneratedBy (yoneda.obj X) fun x ↦ 𝟙 X

Tactic:
simp only [Subfunctor.isGeneratedBy_iff]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ ⨆ i, Subfunctor.ofSection (𝟙 X) = ⊤
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
⊢ (Sieve.ofArrows X f).arrows (f' i')

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
⊢ (Sieve.ofArrows X' f').arrows (f' i')
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M N : ↑(F.obj { as := op S })
⊢ (⇑(DescentData.subtypeCompatibleHomEquiv F f) ∘
        Presieve.Arrows.toCompatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯) ∘
      ⇑F.presheafHomObjHomEquiv =
    (F.toDescentData f).map

Tactic:
ext φ : 1

Goal state after:
case e'_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
M N : ↑(F.obj { as := op S })
φ : M ⟶ N
⊢ ((⇑(DescentData.subtypeCompatibleHomEquiv F f) ∘
          Presieve.Arrows.toCompatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯) ∘
        ⇑F.presheafHomObjHomEquiv)
      φ =
    (F.toDescentData f).map φ
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
⊢ F.IsPrestackFor R.arrows ↔
    ∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := op S₀ })) (a : S ⟶ S₀),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows

Tactic:
rw [isPrestackFor_iff_isSheafFor]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
⊢ (∀ (M N : ↑(F.obj { as := op S })),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows) ↔
    ∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := op S₀ })) (a : S ⟶ S₀),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
a : F.obj (Opposite.op Y)
h : (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
⊢ (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤

Tactic:
h

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
a : F.obj (Opposite.op Y)
h : (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
⊢ (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (m.app (Opposite.op Y))) a) = ⊤
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
⊢ P.triangEnvelope ≤ Q

Tactic:
rw [triangEnvelope, iSup_le_iff]

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
⊢ ∀ (i : ℕ), P.triangEnvelopeIter i ≤ Q
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫ (t.eTruncGEToGEGE a b).app ((t.eTruncLT.obj c).obj X) =
    𝟙 ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)) ≫
      (t.eTruncGEπ b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
simp only [triangleω₁δ_obj_mor₂, eTruncGEToGEGE_app, Category.id_comp,
      ← t.eTruncGEπ_app_eTruncGE_map_app (homOfLE hab), ← NatTrans.naturality,
      eTruncGE_obj_map_eTruncGEπ_app]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝² : Preadditive A
inst✝¹ : ι.Full
inst✝ : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
⊢ HasCokernel f₁

Tactic:
by
  obtain ⟨X₃, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map f₁)
  obtain ⟨K, Q, α, β, γ, hT'⟩ := hf₁ f₂ f₃ hT
  exact hasCokernel hι hT hT'

Goal state after: