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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.EffectivelyEnough
inst✝² : Precoherent D
inst✝¹ : F.Full
inst✝ : F.Faithful
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
x✝ : EffectiveEpiFamily X₁ π₁
⊢ ∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
by
    obtain ⟨β, _, Y₂, τ₂, H, i, ι, hh⟩ := Precoherent.pullback (F.map f) _ _
      (fun a ↦ F.map (π₁ a)) inferInstance
    refine ⟨β, inferInstance, _, fun b ↦ F.preimage (F.effectiveEpiOver (Y₂ b) ≫ τ₂ b),
      F.finite_effectiveEpiFamily_of_map _ _ ?_,
        ⟨i, fun b ↦ F.preimage (F.effectiveEpiOver (Y₂ b) ≫ ι b), ?_⟩⟩
    · simp only [Functor.map_preimage]
      infer_instance
    · intro b
      apply F.map_injective
      simp [hh b]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ S ∈ (regularTopology C) X

Tactic:
have h_le : Sieve.generate (Presieve.ofArrows (fun () ↦ Y) (fun _ ↦ π)) ≤ S := by
    rw [Sieve.generate_le_iff (Presieve.ofArrows _ _) S]
    apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows _ _) S _
    intro W g f
    refine ⟨W, 𝟙 W, ?_⟩
    cases f
    exact ⟨π, ⟨h.2, Category.id_comp π⟩⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ≤ S
⊢ S ∈ (regularTopology C) X
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ PreservesFiniteProducts F

Tactic:
refine ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
Q E : C
e : Q ⟶ E
r : E ⟶ ∐ X
hq : Presieve.ofArrows X (fun i ↦ Sigma.ι X i) r
⊢ Presieve.ofArrows X f (r ≫ Sigma.desc f)

Tactic:
cases hq

Goal state after:
case mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝¹ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
Q : C
i✝ : I
e : Q ⟶ X i✝
⊢ Presieve.ofArrows X f (Sigma.ι X i✝ ≫ Sigma.desc f)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)
hc : IsColimit c
⊢ Presheaf.IsSheaf (extensiveTopology C) c.pt

Tactic:
let i : c.pt ≅ (G ⋙ sheafToPresheaf _ _).flip ⋙ colim :=
      hc.coconePointUniqueUpToIso (pointwiseIsColimit _)

Goal state after:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)
hc : IsColimit c
i : c.pt ≅ (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim :=
  hc.coconePointUniqueUpToIso (pointwiseIsColimit (G ⋙ sheafToPresheaf (extensiveTopology C) A))
⊢ Presheaf.IsSheaf (extensiveTopology C) c.pt
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj.obj (op X)
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).hom.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op n)).obj.map φ.op)) y

Tactic:
have := hF n

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj.obj (op X)
this : Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).hom.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op n)).obj.map φ.op)) y
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι (P.map π.op) ⋯) ≃ IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)

Tactic:
let S := (Sieve.ofArrows (fun (_ : Unit) => X) (fun _ => π)).arrows

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
S : Presieve B := (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows
⊢ IsLimit (Fork.ofι (P.map π.op) ⋯) ≃ IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Sieve.ofArrows X f ∈ J S
⊢ F.IsStackFor (Presieve.ofArrows X f)

Tactic:
← IsStackFor_generate_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Sieve.ofArrows X f ∈ J S
⊢ F.IsStackFor (Sieve.generate (Presieve.ofArrows X f)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
E F : PreOneHypercover S
f g : E.Hom F
H : Homotopy f g
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
a : E.multicospanShape.L
heq :
  d.ι (F.multicospanShape.fst ⟨(f.s₀ a, g.s₀ a), H.H a⟩) ≫ (F.multicospanIndex P).fst ⟨(f.s₀ a, g.s₀ a), H.H a⟩ =
    d.ι (F.multicospanShape.snd ⟨(f.s₀ a, g.s₀ a), H.H a⟩) ≫ (F.multicospanIndex P).snd ⟨(f.s₀ a, g.s₀ a), H.H a⟩
⊢ f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = g.mapMultiforkOfIsLimit P hc d ≫ c.ι a

Tactic:
simp only [multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
    multicospanIndex_fst, multicospanShape_snd, multicospanIndex_snd] at heq

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
E F : PreOneHypercover S
f g : E.Hom F
H : Homotopy f g
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
a : E.multicospanShape.L
heq : d.ι (f.s₀ a) ≫ P.map (F.p₁ (H.H a)).op = d.ι (g.s₀ a) ≫ P.map (F.p₂ (H.H a)).op
⊢ f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = g.mapMultiforkOfIsLimit P hc d ≫ c.ι a
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₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ pullHom (D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) p f₁ f₂ ⋯ ⋯ = D.hom q f₁ f₂ hf₁ hf₂

Tactic:
rw [D.pullHom_hom _ _ _ (by rw [← (sq i₁ i₂).hp₁, reassoc_of% h₁, hf₁]) _ _
    (by simp) (by simp) _ _ h₁ h₂]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op

Tactic:
erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc,
              ← op_comp, Over.w f]

Goal state after:
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 })
X : Over S
R : Presieve X
hR : R ∈ (Precoverage.toPretopology (Over S) (Precoverage.comap (Over.forget S) J)).coverings X
⊢ Presieve.IsSheafFor (F.presheafHom M N) R

Tactic:
simp only [Precoverage.toPretopology_toPrecoverage, Precoverage.mem_comap_iff,
      Over.forget_obj] at hR

Goal state after:
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 })
X : Over S
R : Presieve X
hR : Presieve.map (Over.forget S) R ∈ J.coverings X.left
⊢ Presieve.IsSheafFor (F.presheafHom M N) R
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
x✝ : Cᵒᵖ ⥤ A
⊢ (ρ_ (Φ.presheafFiber.obj x✝)).inv =
    Φ.presheafFiber.map (ρ_ x✝).inv ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x x✝ ⊗ₘ Φ.toPresheafFiber X x (𝟙_ (Cᵒᵖ ⥤ A))) ⋯ ≫
        Φ.presheafFiber.obj x✝ ◁ Φ.presheafFiberDesc (fun x x_1 ↦ 𝟙 ((𝟙_ (Cᵒᵖ ⥤ A)).obj (Opposite.op x))) ⋯

Tactic:
by
    ext
    simp [tensorHom_def, ← MonoidalCategory.whiskerLeft_comp]

Goal state after:
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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S
⊢ ∀ ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : f₁ ≫ f i₁ = q) (hf₂ : f₂ ≫ f i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₁)) })).app (D.obj ((fun x ↦ x) i₁))).hom ≫
        ((𝟭 (F.DescentData f)).obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F ⋯).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₂)) })).app (D.obj ((fun x ↦ x) i₂))).hom

Tactic:
i₁

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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ : ι
⊢ ∀ ⦃i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : f₁ ≫ f i₁ = q) (hf₂ : f₂ ≫ f i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₁)) })).app (D.obj ((fun x ↦ x) i₁))).hom ≫
        ((𝟭 (F.DescentData f)).obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F ⋯).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₂)) })).app (D.obj ((fun x ↦ x) i₂))).hom
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
⊢ S.map f ≫ (evalEquiv S hs (unop β)).toIso.hom =
    (evalEquiv S hs (unop α)).toIso.hom ≫ (yoneda.obj (S.obj (op PUnit.{u + 1}))).map f

Tactic:
dsimp
      ext
      exact eval_map S (unop α) (unop β) f.unop _ _

Goal state after:
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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
⊢ (pullFunctor F w).map
        (((pullFunctorIdIso F S).symm ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ (pullFunctorCompIso F w w' (𝟙 S) ⋯ ⋯).symm).hom.app
          D) ≫
      (pullFunctorCompIso F w' w (𝟙 S') ⋯ ⋯ ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ pullFunctorIdIso F S').hom.app
        ((pullFunctor F w).obj D) =
    𝟙 ((pullFunctor F w).obj D)

Tactic:
ext j
    dsimp
    simp only [Category.id_comp, Functor.map_comp, Category.assoc]
    rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ (p' _ ≫ f _) (p' _ ≫ q' _ ≫ p' _) (p' _) (by simp)
        (by simp [w', reassoc_of% w]),
      map_eq_pullHom_assoc _ (p' j) (p' j) (p' _ ≫ q' _ ≫ p' _) (by simp) (by simp),
      D.pullHom_hom _ _ (p' j ≫ f _) (by simp) _ _ (by simp)
        (by simp [w, reassoc_of% w']) _ _ (by simp) rfl]
    dsimp
    rw [← F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc _ _ _ _ _ _ rfl rfl (by simp),
      mapComp'_comp_id_hom_app, mapComp'_id_comp_inv_app_assoc, ← Functor.map_comp_assoc,
      Cat.Hom.inv_hom_id_toNatTrans_app]
    simp [D.hom_self _ _ rfl]

Goal state after:
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'
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence

Tactic:
obtain ⟨e, ⟨iso⟩⟩ := DescentData.exists_equivalence_of_sieve_eq F f f' h
  rw [← Functor.isEquivalence_iff_of_iso iso]
  exact ⟨fun _ ↦ inferInstance,
    fun _ ↦ Functor.isEquivalence_of_comp_right _ e.functor⟩

Goal state after:
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
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
⊢ Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows

Tactic:
convert! h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
⊢ (Sieve.overEquiv (Over.mk a)).symm R =
    Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
      (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ ∀ {χ₀' : F ⟶ Ω₀} {χ' : G ⟶ Ω}, IsPullback m χ₀' χ' t → χ' = 𝒞.χ m ≫ eΩ.hom

Tactic:
by
    intro χ₀' χ' hχ'
    have : χ' ≫ eΩ.inv = 𝒞.χ m := by
      apply 𝒞.uniq m (χ₀' := χ₀' ≫ eΩ₀.inv)
      exact hχ'.paste_vert (IsPullback.of_vert_isIso_mono (by simp [ht]))
    simpa using this =≫ eΩ.hom

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
ψ : P✝ ⟶ G.obj T.obj₂
hφ : (ψ ≫ f) ≫ (adj.homEquiv Z T.obj₃) h = 0
α : F.obj P✝ ⟶ T.obj₁
hα : (adj.homEquiv P✝ T.obj₂).symm ψ = α ≫ T.mor₁
eq : ψ = adj.unit.app P✝ ≫ G.map α ≫ G.map T.mor₁
eq' : G.map T.mor₁ ≫ f = 0
⊢ adj.unit.app P✝ ≫ G.map α ≫ G.map T.mor₁ ≫ f = 0

Tactic:
eq',

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
ψ : P✝ ⟶ G.obj T.obj₂
hφ : (ψ ≫ f) ≫ (adj.homEquiv Z T.obj₃) h = 0
α : F.obj P✝ ⟶ T.obj₁
hα : (adj.homEquiv P✝ T.obj₂).symm ψ = α ≫ T.mor₁
eq : ψ = adj.unit.app P✝ ≫ G.map α ≫ G.map T.mor₁
eq' : G.map T.mor₁ ≫ f = 0
⊢ adj.unit.app P✝ ≫ G.map α ≫ 0 = 0
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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = 0
⊢ (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = (shiftFunctor C 1).map 0

Tactic:
by rw [hm, Functor.map_zero]

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
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι π
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₁
β : X₁ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
hQ : 𝟙 Q = 0
this : IsIso α
⊢ Triangle.mk (ι.map (-ιK f₃ α)) (ι.map π) (f₂ ≫ inv α) ∈ distinguishedTriangles

Tactic:
rotate_distinguished_triangle

Goal state after:
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
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι π
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₁
β : X₁ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
hQ : 𝟙 Q = 0
this : IsIso α
⊢ (Triangle.mk (ι.map (-ιK f₃ α)) (ι.map π) (f₂ ≫ inv α)).rotate ∈ distinguishedTriangles