mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case mp
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ∃ v, v ≠ 0 ∧ ∀ (w : X ⟶ Y), ∃ c, c • v = w
⊢ Nonempty (X ≅ Y)

Tactic:
obtain ⟨f, nz, -⟩ := h

Goal state after:
case mp
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : f ≠ 0
⊢ Nonempty (X ≅ Y)
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : F.Additive
X : Mat_ C
⊢ (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) = 𝟙 (⨁ fun i ↦ F.obj (X.X i))

Tactic:
ext i j

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : F.Additive
X : Mat_ C
i j : X.ι
⊢ biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫
      (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i =
    biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫ 𝟙 (⨁ fun i ↦ F.obj (X.X i)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i
Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : P.FullSubcategory ≌ SmallModel.{w, v, u} P.FullSubcategory := equivSmallModel P.FullSubcategory
ι : Type (w + 1) := (J : Type w) × (x : SmallCategory J) × { F // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun x ↦
    match x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
x✝ : ⊤ X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : J ⥤ P.FullSubcategory := P.lift p.diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
this✝ : HasColimit p.diag
this : HasColimit ((G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι)
⊢ (ofObj φ).isoClosure X

Tactic:
let i : ι := ⟨J, inferInstance, G ⋙ e.functor, inferInstance⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : P.FullSubcategory ≌ SmallModel.{w, v, u} P.FullSubcategory := equivSmallModel P.FullSubcategory
ι : Type (w + 1) := (J : Type w) × (x : SmallCategory J) × { F // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun x ↦
    match x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
x✝ : ⊤ X
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : J ⥤ P.FullSubcategory := P.lift p.diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
this✝ : HasColimit p.diag
this : HasColimit ((G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι)
i : ι := ⟨J, ⟨inferInstance, ⟨G ⋙ e.functor, ⋯⟩⟩⟩
⊢ (ofObj φ).isoClosure X
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_3
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
h : __Diagram✝.W x✝
⊢ ∃ li lj, __Diagram✝.W li ∧ __Diagram✝.W lj ∧ x✝ ≫ lj = li

Tactic:
· obtain ⟨⟨⟩⟩ := h
      exact ⟨𝟙 _, 𝟙 _, ⟨⟨⟩⟩, ⟨⟨⟩⟩, by simp⟩

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

Goal state before:
pp: 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)
⊢ IsIso (toSucc W Z) ↔ W.isLocal Z

Tactic:
refine ⟨fun _ X Y f hf ↦ ?_, fun hZ ↦ ?_⟩

Goal state after:
case refine_1
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)
x✝ : IsIso (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective fun g ↦ f ≫ g

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)
hZ : W.isLocal Z
⊢ IsIso (toSucc W Z)
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
H : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
g₁ g₂ : Y ⟶ reflectionObj W Z κ
h : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
⊢ ∃ j g₁' g₂', g₁' ≫ H.incl.app j = g₁ ∧ g₂' ≫ H.incl.app j = g₂

Tactic:
by
      obtain ⟨j₁, g₁, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g₁
      obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g₂
      exact ⟨max j₁ j₂, g₁ ≫ H.F.map (homOfLE (le_max_left _ _)),
        g₂ ≫ H.F.map (homOfLE (le_max_right _ _)), by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝³ : Fact κ₁.IsRegular
inst✝² : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
X : Type w
inst✝¹ : PartialOrder X
inst✝ : IsCardinalFiltered X κ₁
A : Set X
hA : HasCardinalLT (↑A) κ₂
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
hY'' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), ∀ C ∈ Y B hB, ∃ m, ∀ b ∈ ↑C, ↑b ≤ m
⊢ ∃ B, A ⊆ B ∧ IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂

Tactic:
choose m hm using hY''

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝³ : Fact κ₁.IsRegular
inst✝² : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
X : Type w
inst✝¹ : PartialOrder X
inst✝ : IsCardinalFiltered X κ₁
A : Set X
hA : HasCardinalLT (↑A) κ₂
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
⊢ ∃ B, A ⊆ B ∧ IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl
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
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
i : ι
hi : (D i).P j
⊢ j = m

Tactic:
exfalso
            exact (hm₀ i).false (hj.lift (by simp) ≫ (D i).isTerminal.lift hi)

Goal state after:
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
⊢ Mono (coequalizer.desc f ⋯)

Tactic:
by
  -- It suffices to show that the two projections from the kernel pair are equal:
  apply (IsKernelPair.of_hasPullback _).mono_of_eq_fst_snd
  /- We fill in the kernel pair square of `f` as follows:
  ```
                  g₁                   fst
  pullback f f------->pullback e k₁----------> X
        |                 |                    |
      g₂|                 |snd                 |e
        v        fst      v            k₁      v
  pullback k₂ e------>pullback m m---------->coeq
        |                                      |
     snd|                                      |m
        v              e ≫ m = f               v
        X------------------------------------->Y
  ```
  Where `m`, `e`, `k₁`, `k₂`, `g₁`, `g₂` are defined below, `fst` and `snd` denote the projections
  in the pullbacks indicated as the source of those morphisms, and `coeq` is the coequalizer of the
  two projections in from the kernel pair of `f`.
  -/
  let m := (coequalizer.desc f pullback.condition)
  let e := coequalizer.π (pullback.fst f f) (pullback.snd f f)
  let k₁ := pullback.fst m m
  let k₂ := pullback.snd m m
  let d : pullback f f ⟶ (pullback m m) :=
    pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) (by simp [m, e, pullback.condition])
  let g₁ : pullback f f ⟶ (pullback e k₁) := pullback.lift (pullback.fst f f) d (by simp [d, k₁])
  let g₂ : pullback f f ⟶ (pullback k₂ e) := pullback.lift d (pullback.snd f f) (by simp [d, k₂])
  /-
  Since the big square, the bottom square, and the top right square above are pullback squares,
  the top left square is also a pullback square.
  -/
  have h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e) := by
    refine .of_right ?_ (by simp [g₁, g₂]) (.of_hasPullback e k₁)
    refine .of_bot ?_ ?_ (.paste_horiz (.of_hasPullback k₂ e) (.of_hasPullback m m))
    · simpa [g₁, g₂, e, m, pullback.lift_fst, pullback.lift_snd] using .of_hasPullback f f
    · simp [g₁, g₂, k₁, d]
  /-
  Since `g₁` is the base change of a regular epi (the map `fst` in the middle row of the diagram
  above, which itself is a regular epi because it is a base change of the regular epi `e`),
  it is a regular epi.
  -/
  have : IsRegularEpi g₁ := by
    apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback h.flip
    dsimp [MorphismProperty.regularEpi]
    infer_instance
  -- We precompose with the epimorphism `g₁ ≫ pullback.snd e k₁`, and finish
  rw [← cancel_epi (g₁ ≫ pullback.snd e k₁)]
  convert! coequalizer.condition (pullback.fst f f) (pullback.snd f f) using 1
  all_goals cat_disch

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

Goal state before:
pp: case hR
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (coherentCoverage C).coverings X

Tactic:
exact ⟨_, inferInstance, Y, π, rfl, hπ.1⟩

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 : ι
Y₁ : Over (X i)
⊢ ∀ ⦃Y₂ Z : Over (X i)⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))⦄ ⦃f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))⦄
    (h₁ : (sieve f f' i).arrows f₁) (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)

Tactic:
Y₂

Goal state after:
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 : ι
Y₁ Y₂ : Over (X i)
⊢ ∀ ⦃Z : Over (X i)⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))⦄ ⦃f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))⦄
    (h₁ : (sieve f f' i).arrows f₁) (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Cᵒᵖ ⥤ Type u_3
⊢ Function.Bijective (E.saturate.multifork F).toSections ↔ Presieve.IsSheafFor F E.presieve₀

Tactic:
Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Cᵒᵖ ⥤ Type u_3
⊢ Function.Bijective (E.saturate.multifork F).toSections ↔ Function.Bijective (Presieve.Arrows.toCompatible F E.f)
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
i₁ i₂ i₃ : ι
⊢ pullHom (D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₁₂ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
        ⋯ ≫
      pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁
      (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯

Tactic:
pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,

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
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
i₁ i₂ i₃ : ι
⊢ pullHom (D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₁₂ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
        ⋯ ≫
      pullHom (D.hom (sq i₂ i₃).p (sq i₂ i₃).p₁ (sq i₂ i₃).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₂₃ (sq₃ i₁ i₂ i₃).p₂
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁
      (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ (f.hom.app W ≫ invMap) ≫ F.obj.map I.f.op = 𝟙 (F.obj.obj W) ≫ F.obj.map I.f.op

Tactic:
simp only [op_unop, Category.assoc, Category.id_comp]

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ f.hom.app W ≫ invMap ≫ F.obj.map I.f.op = F.obj.map I.f.op
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ (invMap ≫ f.hom.app W) ≫ G.obj.map I.f.op = 𝟙 (G.obj.obj W) ≫ G.obj.map I.f.op

Tactic:
simp only [op_unop, Category.assoc, Category.id_comp]

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ invMap ≫ f.hom.app W ≫ G.obj.map I.f.op = G.obj.map I.f.op
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
φ : (Over.forget (unop (op X))).op ⋙ F ⟶ (Over.forget (unop (op X))).op ⋙ G
Y : Over (unop (op X))
⊢ ((ConcreteCategory.hom (↾(Over.map (𝟙 (op X)).unop).op.whiskerLeft)).toFun φ).app (op Y) =
    ((ConcreteCategory.hom (𝟙 ((Over.forget (unop (op X))).op ⋙ F ⟶ (Over.forget (unop (op X))).op ⋙ G))).toFun φ).app
      (op Y)

Tactic:
simpa [Over.mapId] using φ.naturality ((Over.mapId X).hom.app Y).op

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac : a ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ a = b

Tactic:
simpa only [← cancel_mono sq.f₂₄] using fac

Goal state after:
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
⊢ ∀ {x y z : OneCocycle G U}, x.IsCohomologous y → y.IsCohomologous z → x.IsCohomologous z

Tactic:
rintro γ₁ γ₂ γ₂ ⟨α, h⟩ ⟨β, h'⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂✝ γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂✝.toOneCochain α
β : ZeroCochain G U
h' : OneCohomologyRelation γ₂✝.toOneCochain γ₂.toOneCochain β
⊢ γ₁.IsCohomologous γ₂
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
U : Over X
R : Sieve U
hR : R ∈ (J.over X) U
u : (Over.forget X ⋙ Φ.fiber).obj U
hu : u ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f)) y = ⟨u, hu⟩

Tactic:
obtain ⟨R, rfl⟩ := (Sieve.overEquiv _).symm.surjective R

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
U : Over X
u : (Over.forget X ⋙ Φ.fiber).obj U
hu : u ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
R : Sieve U.left
hR : (Sieve.overEquiv U).symm R ∈ (J.over X) U
⊢ ∃ Y f,
    ∃ (_ : ((Sieve.overEquiv U).symm R).arrows f),
      ∃ y, (ConcreteCategory.hom ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f)) y = ⟨u, hu⟩
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
p : M ⟶ M'
S : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.map (MonCat.Hom.hom (p.app V✝)) (Submonoid.map (MonCat.Hom.hom (M.map i)) (S.obj U✝)) ≤
    Submonoid.map (MonCat.Hom.hom (p.app V✝)) (S.obj V✝)

Tactic:
grw [S.map_le]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
h : A ≤ B
⊢ { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
    { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B

Tactic:
exact leOfHom (((equivalenceMonoOver F).trans
        (ThinSkeleton.equivalence _).symm).functor.map (homOfLE h))

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
M N : ↑(F.obj { as := op S })
⊢ Function.Bijective (F.toDescentData f).map ↔
    Presieve.IsSheafFor (F.presheafHom M N) (Presieve.ofArrows (fun i ↦ Over.mk (f i)) fun i ↦ Over.homMk (f i) ⋯)

Tactic:
Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,

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
M N : ↑(F.obj { as := op S })
⊢ Function.Bijective (F.toDescentData f).map ↔
    Function.Bijective (Presieve.Arrows.toCompatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯)