mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Functor

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : RightRigidCategory C
X : C
⊢ 𝟙 Xᘁ.op.mop = 𝟙 { unmop := op Xᘁ }

Tactic:
by simp [rightAdjointMate_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalCategory V
U : C ⥤ V
inst✝³ : DayConvolutionUnit U
F : C ⥤ V
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ : DayConvolution U F
G : C ⥤ V
inst✝ : DayConvolution U G
f : F ⟶ G
x✝ : Discrete PUnit.{1} × C
⊢ (extensionUnitLeft U (φ U) F ≫
          ((fromPUnit (𝟙_ C)).prod (𝟭 C)).whiskerLeft
            (DayConvolution.unit U F ≫ (tensor C).whiskerLeft (DayConvolution.map (𝟙 U) f ≫ (leftUnitor U G).hom))).app
      x✝ =
    (extensionUnitLeft U (φ U) F ≫
          ((fromPUnit (𝟙_ C)).prod (𝟭 C)).whiskerLeft
            (DayConvolution.unit U F ≫ (tensor C).whiskerLeft ((leftUnitor U F).hom ≫ f))).app
      x✝

Tactic:
simp [← whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ P.underObj ≤ ObjectProperty.isFinitelyPresentable (Under X)

Tactic:
intro Y

Goal state after:
case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y✝ : C
f : X ⟶ Y✝
inst✝ : IsFinitelyAccessibleCategory (Under X)
Y : Under X
⊢ P.underObj Y ≤ ObjectProperty.isFinitelyPresentable (Under X) Y
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
⊢ P.isoClosure.localEpi = P.localEpi

Tactic:
by
  refine le_antisymm (localEpi_antitone <| le_isoClosure P) ?_
  intro X Y f hf Z ⟨T, hT, ⟨e⟩⟩ u v huv
  rw [← cancel_mono e.hom]
  apply hf hT
  simpa

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
i : ι
⊢ o.matrixDecomposition (𝟙 (⨁ fun a ↦ s (f a))) i = 1

Tactic:
by
  ext ⟨b, ⟨⟩⟩ ⟨a, j_property⟩
  simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property
  simp only [Category.comp_id, Category.id_comp, End.one_def, eqToHom_refl,
    Matrix.one_apply, HomOrthogonal.matrixDecomposition_apply, biproduct.components]
  split_ifs with h
  · cases h
    simp
  · simp only [Subtype.mk.injEq] at h
    convert! comp_zero
    simpa using biproduct.ι_π_ne _ (Ne.symm h)

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
f : X ⟶ Y
⊢ biprod.inr ≫ biprod.desc f 0 = biprod.inr ≫ biprod.fst ≫ f

Tactic:
simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
x : ↑J.obj
⊢ (ConcreteCategory.hom f) x =
    (ConcreteCategory.hom (c.ι.app m)) ((ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x))

Tactic:
rw [← hg, ← ConcreteCategory.comp_apply, c.w]

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
x : ↑J.obj
⊢ (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
    (ConcreteCategory.hom (c.ι.app (j x))) (g x)
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ __Diagram✝.IsTerminal j

Tactic:
refine .ofExistsUnique ⟨⟨⟩⟩ (fun _ h ↦ ?_) (fun _ h₁ _ _ h₂ h₃ ↦ ?_) (fun _ _ _ h ↦ ?_)
    · simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h
      subst h
      exact ⟨𝟙 _, ⟨⟨⟩⟩⟩
    · simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h₁
      subst h₁
      obtain ⟨⟨⟩⟩ := h₂
      obtain ⟨⟨⟩⟩ := h₃
      simp
    · obtain ⟨⟨⟩⟩ := h
      exact ⟨𝟙 _, 𝟙 _, ⟨⟨⟩⟩, ⟨⟨⟩⟩, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
g : Z ⟶ T
f : (d : D₁ W Z) → (↑d.fst).right ⟶ T
hf : ∀ (d : D₁ W Z), (fun g ↦ (↑d.fst).hom ≫ g) (f d) = d.snd ≫ g
⊢ ∃ a, (fun g ↦ toSucc W Z ≫ g) a = g

Tactic:
exact ⟨Multicoequalizer.desc _ _ (fun ⟨⟩ ↦ pushout.desc (Sigma.desc f) g)
      (fun d ↦ (hT d.1.1.hom d.1.2).1 (by simp [reassoc_of% d.2.2])), by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ ((D ⟨i, ⟨j, hj⟩⟩.fst).isTerminal.lift ⋯ ≫ u ⟨i, ⟨j, hj⟩⟩.fst) ≫ 𝟙 m = φ ⟨i, ⟨j, hj⟩⟩

Tactic:
simp [φ]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x ↦
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x ↦
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ Nonempty
    (Limits.IsColimit
      (Sieve.generate (Presieve.ofArrows (fun c ↦ Y_n c.fst c.snd) fun c ↦ π_n c.fst c.snd ≫ π c.fst)).arrows.cocone)

Tactic:
← Sieve.forallYonedaIsSheaf_iff_colimit

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x ↦
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x ↦
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ ∀ (W : C),
    Presieve.IsSheafFor (yoneda.obj W)
      (Sieve.generate (Presieve.ofArrows (fun c ↦ Y_n c.fst c.snd) fun c ↦ π_n c.fst c.snd ≫ π c.fst)).arrows
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 Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
h₂ : Sieve.generate (Presieve.ofArrows ?m.50 ?m.51) ∈ (regularTopology C) X
⊢ Nonempty (IsColimit (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)).arrows.cocone)

Tactic:
← Sieve.forallYonedaIsSheaf_iff_colimit

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
h₂ : Sieve.generate (Presieve.ofArrows ?m.50 ?m.51) ∈ (regularTopology C) X
⊢ ∀ (W : C), Presieve.IsSheafFor (yoneda.obj W) (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)).arrows
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ (regularCoverage C).coverings Y
⊢ ∃ Y_1 π, EffectiveEpi π ∧ (Sieve.generate T).arrows π

Tactic:
rcases hS with ⟨Y', π, h'⟩

Goal state after:
case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
T : Presieve Y
Y' : C
π : Y' ⟶ Y
h' : (T = Presieve.ofArrows (fun x ↦ Y') fun x ↦ π) ∧ EffectiveEpi π
⊢ ∃ Y_1 π, EffectiveEpi π ∧ (Sieve.generate T).arrows π
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
a : ∃ Y_1 π, EffectiveEpi π ∧ R.arrows π
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
⊢ ∃ Y_1 π, EffectiveEpi π ∧ S.arrows π

Tactic:
rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩

Goal state after:
case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
⊢ ∃ Y_1 π, EffectiveEpi π ∧ S.arrows π
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✝ : Preadditive A
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) colim

Tactic:
apply +allowSynthFailures preservesProductsOfShape_of_preservesBiproductsOfShape
    apply preservesBiproductsOfShape_of_preservesCoproductsOfShape

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

Goal state before:
pp: case mp.top
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), ⊤.arrows (π a)

Tactic:
| top X =>

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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
q' : Z ⟶ S
a' : Z ⟶ X (α j)
hq' : q ≫ f i = q'
ha' : a ≫ p' j = a'
⊢ mor w φ q a fac = D₁.hom q' q a' ⋯ ⋯ ≫ pullHom (φ.hom j) a a' a' ⋯ ⋯ ≫ D₂.hom q' a' q ⋯ ⋯

Tactic:
subst hq' ha'
  rfl

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
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
⊢ IsLimit (F.multifork G)

Tactic:
refine Multifork.IsLimit.mk _ ?_ ?_ ?_
  · intro t
    refine Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ?_
    intro b
    dsimp
    simp only [Category.assoc, ← Functor.map_comp, ← op_comp]
    rw [← f.w₁₁, ← f.w₁₂]
    simp only [op_comp, Functor.map_comp]
    exact t.condition_assoc ⟨(f.s₀ b.1.1, f.s₀ b.1.2), f.s₁ b.2⟩ _
  · intro t i
    simp only [multicospanIndex_left, multicospanShape_L, multifork_ι]
    have h1 := hgf.wl i
    have h2 := t.condition ⟨⟨_, _⟩, hgf.H i⟩
    dsimp at h1 h2
    rw [← g.w₀, op_comp, Functor.map_comp, ← E.multifork_ι, Multifork.IsLimit.fac_assoc,
      Category.assoc, ← Functor.map_comp, ← op_comp, ← h1, op_comp, Functor.map_comp,
      reassoc_of% h2, ← Functor.map_comp, ← op_comp, hgf.wr i]
    simp
  · intro t m hm
    refine Multifork.IsLimit.hom_ext hE fun i ↦ ?_
    rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]

Goal state after:
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
⊢ Sieve.ofArrows (cylinder f g).X (cylinder f g).f ≤
    Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun i ↦
        (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)

Tactic:
Sieve.generate_le_iff

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
⊢ Presieve.ofArrows (cylinder f g).X (cylinder f g).f ≤
    (Sieve.generate
        (Presieve.bindOfArrows E.X E.f fun i ↦
          (Sieve.pullback (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)).arrows
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)
⊢ Sieve.generate (Presieve.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)

Tactic:
Sieve.generate_le_iff

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)
⊢ (Presieve.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)).arrows
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.generate
      (Presieve.pullbackArrows
        (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) ⋯ ⋯)
        (Presieve.ofArrows E.Y fun j_1 ↦ E.toPullback j_1)) ≤
    (cylinder f g).sieve₁' i j

Tactic:
Sieve.generate_le_iff

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)
⊢ Presieve.pullbackArrows
      (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) ⋯ ⋯)
      (Presieve.ofArrows E.Y fun j_1 ↦ E.toPullback j_1) ≤
    ((cylinder f g).sieve₁' i j).arrows
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : Over (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
⊢ (sieve f f' i).arrows (Over.homMk Z.hom ⋯)

Tactic:
convert! hq

Goal state after:
case e'_6
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : Over (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
e_5✝ : Over.mk Z.hom = Z
⊢ Over.homMk Z.hom ⋯ = q
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
⊢ (isomorphisms C).IsLocalAtTarget J

Tactic:
refine .mk_of_isStableUnderBaseChange fun {X Y} f 𝒰 (H : ∀ i, IsIso _) ↦ ⟨?_, ?_, ?_⟩
  · refine 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst _ _) fun i j ↦ ?_
    let f := pullback.map (pullback.fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (pullback.snd _ _)
      (𝟙 _) (𝟙 _) (by simp [pullback.condition]) (by simp)
    rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ f)]
    simp [pullback.condition, f]
  · exact (𝒰.pullback₁ f).hom_ext fun i ↦ by simp [pullback.condition_assoc]
  · exact 𝒰.hom_ext fun i ↦ by simp [pullback.condition]

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₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫ D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫ (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂))
⊢ (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫
        D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₁.obj (α j₂)) ≫
          (F.map f₂.op.toLoc).toFunctor.map ((F.map (p' j₂).op.toLoc).toFunctor.map (φ.hom (α j₂)))

Tactic:
← mapComp'_hom_naturality,

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₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫ D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫ (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂))
⊢ (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫
        D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂)) ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂))
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i : I
T : C
a : T ⟶ U i
⊢ γ.ev i i a a = 1

Tactic:
simpa using γ.ev_trans i i i a a a

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

Goal state before:
pp: case hex
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
hx : x.Compatible
⊢ ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    { app := fun Y ↦ app hG x hx (unop Y).hom, naturality := ⋯ }.app (op (Over.mk g)) =
      (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
intro Y

Goal state after:
case hex
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
hx : x.Compatible
Y : C
⊢ ∀ (g : Y ⟶ X) (hg : S.arrows g),
    { app := fun Y ↦ app hG x hx (unop Y).hom, naturality := ⋯ }.app (op (Over.mk g)) =
      (x g hg).app (op (Over.mk (𝟙 Y)))