mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2.h₀
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
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ ((((Sigma.ι D₁.obj₂ d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z)) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit) ≫
          f) ≫
        toStep W Z) ≫
      fromStep W Z =
    (Sigma.ι D₁.obj₂ d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z)) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit

Tactic:
refine D₂.condition _ d.1.2 ?_

Goal state after:
case refine_2.h₀
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
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ (↑d.fst).hom ≫
      (((Sigma.ι D₁.obj₂ d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z)) ≫
            Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit) ≫
          f) ≫
        toStep W Z =
    (↑d.fst).hom ≫ Sigma.ι D₁.obj₂ d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z)
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_1
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : ((coyoneda.obj (op X)).mapCocone c).pt
⊢ ∃ i xi, f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app i)) xi

Tactic:
dsimp at f
        choose j g hg using fun x ↦ Types.jointly_surjective_of_isColimit hc (f x)
        refine ⟨IsCardinalFiltered.max j hX,
          ↾fun x ↦ F.map (IsCardinalFiltered.toMax j hX x) (g x), ?_⟩
        dsimp
        ext x
        dsimp at j g hg x ⊢
        rw [← hg]
        exact congr_hom (c.w (IsCardinalFiltered.toMax j hX x)).symm (g x)

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsSmall.{w, v, u} W
inst✝¹ : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
inst✝ : HasColimitsOfSize.{w, w, v, u} C
this✝¹ : Nonempty κ.ord.ToType
this✝ : OrderBot κ.ord.ToType
this : ∀ (Z : C) [IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] [HasCoproducts C], HasCoproductsOfShape (D₁ W Z) C
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
have := D₂.hasColimitsOfShape.{w} W

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsSmall.{w, v, u} W
inst✝¹ : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
inst✝ : HasColimitsOfSize.{w, w, v, u} C
this✝² : Nonempty κ.ord.ToType
this✝¹ : OrderBot κ.ord.ToType
this✝ : ∀ (Z : C) [IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] [HasCoproducts C], HasCoproductsOfShape (D₁ W Z) C
this :
  ∀ (Z : C) [inst : HasCoproduct D₁.obj₁] [inst_1 : HasCoproduct D₁.obj₂] [inst_2 : HasPushouts C] [IsSmall.{w, v, u} W]
    [LocallySmall.{w, v, u} C] [HasColimitsOfSize.{w, w, v, u} C],
    HasColimitsOfShape (WalkingMultispan (D₂.multispanShape W Z)) C
⊢ W.isLocal.ι.IsRightAdjoint
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X✝ X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
this✝ : Fact κ.IsRegular
this : IsCardinalPresentable X κ
⊢ IsPresentable.{u, u, u + 1} X

Tactic:
exact isPresentable_of_isCardinalPresentable X κ

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

Goal state before:
pp: case refine_2.mk.refl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
Z : C
π : Z ⟶ X
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.singleton π π

Tactic:
exact Presieve.singleton.mk

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
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).W ≤ ((fun i ↦ (D i).toDiagram) i).W

Tactic:
by rfl

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:
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.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
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).P ≤ ((fun i ↦ (D i).toDiagram) i).P

Tactic:
by rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ AssociatorBimod.homAux M (regular Y) N ≫
      colimMap
        (parallelPairHom (M.actRight ▷ TensorBimod.X (regular Y) N)
          ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N) (M.actRight ▷ N.X)
          ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ LeftUnitorBimod.hom N) (M.X ◁ LeftUnitorBimod.hom N) ⋯
          ⋯) =
    coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
        ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) ≫
      colimMap
        (parallelPairHom (TensorBimod.actRight M (regular Y) ▷ N.X)
          ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) (M.actRight ▷ N.X)
          ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) (RightUnitorBimod.hom M ▷ Y.X ▷ N.X) (RightUnitorBimod.hom M ▷ N.X) ⋯
          ⋯)

Tactic:
dsimp [AssociatorBimod.homAux]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ ((PreservesCoequalizer.iso (tensorRight N.X) (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ μ)).inv ≫
        coequalizer.desc
          ((α_ M.X Y.X N.X).hom ≫
            M.X ◁ coequalizer.π (μ ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
              coequalizer.π (M.actRight ▷ TensorBimod.X (regular Y) N)
                ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N))
          ⋯) ≫
      colimMap
        (parallelPairHom (M.actRight ▷ TensorBimod.X (regular Y) N)
          ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N) (M.actRight ▷ N.X)
          ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ LeftUnitorBimod.hom N) (M.X ◁ LeftUnitorBimod.hom N) ⋯
          ⋯) =
    coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
        ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) ≫
      colimMap
        (parallelPairHom (TensorBimod.actRight M (regular Y) ▷ N.X)
          ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) (M.actRight ▷ N.X)
          ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) (RightUnitorBimod.hom M ▷ Y.X ▷ N.X) (RightUnitorBimod.hom M ▷ N.X) ⋯
          ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ ((PreservesCoequalizer.iso (tensorRight N.X) (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ μ)).inv ≫
        coequalizer.desc
          ((α_ M.X Y.X N.X).hom ≫
            M.X ◁ coequalizer.π (μ ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
              coequalizer.π (M.actRight ▷ TensorBimod.X (regular Y) N)
                ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N))
          ⋯) ≫
      colimMap
        (parallelPairHom (M.actRight ▷ TensorBimod.X (regular Y) N)
          ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N) (M.actRight ▷ N.X)
          ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ LeftUnitorBimod.hom N) (M.X ◁ LeftUnitorBimod.hom N) ⋯
          ⋯) =
    coequalizer.desc M.actRight ⋯ ▷ N.X ≫
      colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ (tensorRight N.X).map
        (coequalizer.π (M.actRight ▷ (regular Y).X) ((α_ M.X Y.X (regular Y).X).hom ≫ M.X ◁ (regular Y).actLeft)) ≫
      ((PreservesCoequalizer.iso (tensorRight N.X) (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ μ)).inv ≫
          coequalizer.desc
            ((α_ M.X Y.X N.X).hom ≫
              M.X ◁ coequalizer.π (μ ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
                coequalizer.π (M.actRight ▷ TensorBimod.X (regular Y) N)
                  ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N))
            ⋯) ≫
        colimMap
          (parallelPairHom (M.actRight ▷ TensorBimod.X (regular Y) N)
            ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N)
            (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ LeftUnitorBimod.hom N)
            (M.X ◁ LeftUnitorBimod.hom N) ⋯ ⋯) =
    (tensorRight N.X).map
        (coequalizer.π (M.actRight ▷ (regular Y).X) ((α_ M.X Y.X (regular Y).X).hom ≫ M.X ◁ (regular Y).actLeft)) ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one
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
⊢ PreservesColimit G (sheafToPresheaf (extensiveTopology C) A)

Tactic:
suffices CreatesColimit G (sheafToPresheaf (extensiveTopology C) A) from inferInstance

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
⊢ CreatesColimit G (sheafToPresheaf (extensiveTopology C) A)
Module: Mathlib.CategoryTheory.Sites.Finite

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
hs : s ∈ (Precoverage.finite C).coverings X
ht : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : s f), t f H ∈ (Precoverage.finite C).coverings Y
⊢ s.bind t ∈ (Precoverage.finite C).coverings X

Tactic:
simpa using hs.biUnion' fun _ _ ↦ (ht _ _).image _

Goal state after:
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)
Y✝ Y : C
k : E.I₁ i.fst j.fst
⊢ ((cylinder f g).sieve₁' i j).arrows
    (pullback.snd (E.toPullback k)
      (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) ⋯ ⋯))

Tactic:
simp_rw [← pullbackSymmetry_inv_comp_fst]

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)
Y✝ Y : C
k : E.I₁ i.fst j.fst
⊢ ((cylinder f g).sieve₁' i j).arrows
    ((pullbackSymmetry
          (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.toPullback k)).inv ≫
      pullback.fst
        (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.toPullback k))
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: 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)
⊢ IsIso f

Tactic:
by
  rw [← ObjectProperty.isIso_hom_iff, NatTrans.isIso_iff_isIso_app]
  have hiso (Z : C) (i : ι) (g : Z ⟶ X i) : IsIso (f.hom.app (op Z)) :=
    (NatTrans.isIso_iff_isIso_app ((K.overPullback A (X i)).map f).hom).mp inferInstance
      (op (Over.mk g))
  intro W
  let S : K.Cover W.unop := hX.cover W.unop
  have harrow (I : S.Arrow) : IsIso (f.hom.app (op I.Y)) := by
    obtain ⟨i, ⟨g⟩⟩ := I.hf
    exact hiso I.Y i g
  let invMap : G.obj.obj (op W.unop) ⟶ F.obj.obj (op W.unop) :=
    F.property.amalgamate S (fun I => G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) (by
      intro I₁ I₂ r
      have hZ : IsIso (f.hom.app (op r.Z)) := by
        obtain ⟨i, ⟨g⟩⟩ := I₁.hf
        exact hiso r.Z i (r.g₁ ≫ g)
      simp only [Category.assoc, f.hom.naturality_inv]
      rw [← Category.assoc, ← Category.assoc, ← G.obj.map_comp, ← G.obj.map_comp,
        ← op_comp, ← op_comp, r.w])
  refine ⟨⟨invMap, ?_, ?_⟩⟩
  · refine F.property.hom_ext S _ _ fun I => ?_
    simp only [op_unop, Category.assoc, Category.id_comp]
    rw [Presheaf.IsSheaf.amalgamate_map, ← f.hom.naturality_assoc]
    simp
  · refine G.property.hom_ext S _ _ fun I => ?_
    simp only [op_unop, Category.assoc, Category.id_comp]
    rw [← f.hom.naturality, Presheaf.IsSheaf.amalgamate_map_assoc]
    simp

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

Goal state before:
pp: case hunique
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₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₁.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
hy₂ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : Over X
Z : Over Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
⊢ ((Over.forget (unop (op X))).op ⋙ F).map φ.op ≫ y₁.app (op (Over.mk (Z.hom ≫ Y.hom))) =
    ((Over.forget (unop (op X))).op ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))

Tactic:
rw [(hy₁ _ _ hZ), ← ((hy₂ _ _ hZ))]

Goal state after:
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✝
inst✝³ : J.HasEnoughPoints
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
X : C
inst✝ : HasSheafify (J.over X) (Type w)
P : ObjectProperty J.Point
left✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
hP : P.IsConservativeFamilyOfPoints
⊢ (J.over X).HasEnoughPoints

Tactic:
exact ⟨_, inferInstance, hP.over X⟩

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

Goal state before:
pp: S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
⊢ (𝟭 (Sheaf typesGrothendieckTopology (Type u))).map f ≫ (equivYoneda' S₂).hom =
    (equivYoneda' S₁).hom ≫
      ((sheafToPresheaf typesGrothendieckTopology (Type u) ⋙ (evaluation Type uᵒᵖ (Type u)).obj (op PUnit.{u + 1})) ⋙
            yoneda').map
        f

Tactic:
ext ⟨α⟩ s

Goal state after:
S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
α : Type u
s : ((𝟭 (Sheaf typesGrothendieckTopology (Type u))).obj S₁).obj.obj (op α)
⊢ (ConcreteCategory.hom
          (((𝟭 (Sheaf typesGrothendieckTopology (Type u))).map f ≫ (equivYoneda' S₂).hom).hom.app (op α))).toFun
      s =
    (ConcreteCategory.hom
          (((equivYoneda' S₁).hom ≫
                  ((sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
                          (evaluation Type uᵒᵖ (Type u)).obj (op PUnit.{u + 1})) ⋙
                        yoneda').map
                    f).hom.app
            (op α))).toFun
      s
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M M' M'' : C ⥤ MonCat
p : M ⟶ M'
S'' : SubmonoidFunctor M''
p' : M' ⟶ M''
⊢ comap (p ≫ p') S'' = comap p (comap p' S'')

Tactic:
by 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
M N : ↑(F.obj { as := op S })
φ : M ⟶ N
i : ι
⊢ ((subtypeCompatibleHomEquiv F f)
          (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun i ↦ Over.homMk (f i) ⋯)
            (F.presheafHomObjHomEquiv φ))).hom
      i =
    ((F.toDescentData f).map φ).hom i

Tactic:
simp [subtypeCompatibleHomEquiv, presheafHomObjHomEquiv, pullHom,
    ← Functor.map_comp, Pseudofunctor.mapComp'_id_comp_hom_app_assoc,
    Pseudofunctor.mapComp'_id_comp_inv_app]

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
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows
S✝ : C
M N : ↑(F.obj { as := op S✝ })
U : C
u : U ⟶ S✝
S : Sieve (Over.mk u)
hS : S ∈ (J.over S✝) (Over.mk u)
⊢ Presieve.IsSheafFor (F.presheafHom M N) S.arrows

Tactic:
apply (hF _ _ hS).isSheafFor'

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✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ IsZero (ι.obj 0)

Tactic:
rw [IsZero.iff_id_eq_zero, ← ι.map_id, id_zero, ι.map_zero]

Goal state after:
Module: Mathlib.Combinatorics.Additive.CovBySMul

Goal state before:
pp: M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A₁ A₂ B : Set X
hA : A₁ ⊆ A₂
hAB : CovBySMul M K A₂ B
⊢ CovBySMul M K A₁ B

Tactic:
simpa using (CovBySMul.of_subset (M := M) hA).trans hAB

Goal state after: