mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (HomRel.CompClosure redStep) (p ≫ Path.reverse p) = Quot.mk (HomRel.CompClosure redStep) (𝟙 X)

Tactic:
by
  apply Quot.eqvGen_sound
  induction p with
  | nil => apply EqvGen.refl
  | cons q f ih =>
    simp only [Quiver.Path.reverse]
    fapply EqvGen.trans
    -- Porting note: dot notation for `Quiver.Path.*` and `Quiver.Hom.*` not working
    · exact q ≫ Quiver.Path.reverse q
    · apply EqvGen.symm
      apply EqvGen.rel
      have : HomRel.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
          (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫
            Quiver.Path.reverse q) := by
        apply HomRel.CompClosure.intro
        apply redStep.step
      simp only [Category.assoc, Category.id_comp] at this ⊢
      -- Porting note: `simp` cannot see how `Quiver.Path.comp_assoc` is relevant, so change to
      -- category notation
      change HomRel.CompClosure redStep (q ≫ Quiver.Path.reverse q)
        (Quiver.Path.cons q f ≫ (Quiver.Hom.toPath (Quiver.reverse f)) ≫ (Quiver.Path.reverse q))
      simp only [← Category.assoc] at this ⊢
      exact this
    · exact ih

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : HasPullbacks C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom (t.from X) ↔ HasLiftingProperty g ((MonoidalClosed.pre f).app X)

Tactic:
rw [hasLiftingProperty_mk_iff]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : HasPullbacks C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal Y
⊢ HasLiftingProperty g (Opposite.op (Arrow.mk f) ⋔ Arrow.mk (t.from X)).hom ↔
    HasLiftingProperty g ((MonoidalClosed.pre f).app X)
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ r • (ConcreteCategory.hom (F.map i ≫ F.map (IsFiltered.toSup {j, j', j''} {⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩} ⋯))) x = 0

Tactic:
ModuleCat.comp_apply,

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ r •
      (ConcreteCategory.hom (F.map (IsFiltered.toSup {j, j', j''} {⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩} ⋯)))
        ((ConcreteCategory.hom (F.map i)) x) =
    0
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (λ_ f).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C (𝟙 a).toFunctor f.toFunctor)).hom ≫
        (Cat.Hom.isoMk mapPairId).hom ▷ (mapPair (𝟭 C) f.toFunctor).toCatHom ≫
          (λ_ (mapPair (𝟭 C) f.toFunctor).toCatHom).hom

Tactic:
by intros; exact congr($(mapWhiskerLeft_leftUnitor_hom C _).toCatHom₂)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case mk
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : (F.obj (op j'✝)).obj j✝
⊢ (hom (Multicofork.π s ⟨j✝, (Hom.hom ((F.map f.op).app j✝)) x⟩.fst)) ⟨j✝, (Hom.hom ((F.map f.op).app j✝)) x⟩.snd =
    (hom (Multicofork.π s ⟨j'✝, (Hom.hom ((F.obj (op j'✝)).map f)) x⟩.fst))
      ⟨j'✝, (Hom.hom ((F.obj (op j'✝)).map f)) x⟩.snd

Tactic:
exact ConcreteCategory.congr_hom (Cowedge.condition s f) _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasWeakPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasWeakPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ (fst f₁ f₂ ≫ i₁) ≫ g₁ = (snd f₁ f₂ ≫ i₂) ≫ g₂

Tactic:
simp only [Category.assoc, ← eq₁, ← eq₂, weakPullback.condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case triangle
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((α_hom X✝ unit Y✝).comp (Hom.whiskerLeft X✝ (l_hom Y✝))) =
    projectMapAux f✝ ((ρ_hom X✝).whiskerRight Y✝)

Tactic:
dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.triangle]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ Yoneda.fullyFaithful.preimage
        { app := fun X ↦ ↾fun x ↦ h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H), naturality := ⋯ } ≫
      φ =
    G ◁ φ ≫ conj G

Tactic:
refine yoneda.map_injective ?_

Goal state after:
case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ yoneda.map
      (Yoneda.fullyFaithful.preimage
          { app := fun X ↦ ↾fun x ↦ h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H), naturality := ⋯ } ≫
        φ) =
    yoneda.map (G ◁ φ ≫ conj G)
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)

Tactic:
IsSubterminal.def

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (ε ≫ η) ▷ A

pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ

Tactic:
simp only [comp_whiskerRight]

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (ε ▷ A ≫ η ▷ A)

case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (ε ≫ η) ▷ A

pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮

Tactic:
simp only [comp_whiskerRight]

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (ε ▷ A ≫ η ▷ A)

case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (ε ≫ η) ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ ε

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (ρ_ A).hom

Tactic:
simp only [comp_whiskerRight]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| ε ▷ A ≫ η ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ ε

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (ρ_ A).hom
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ ((ε ⊗ₘ ε) ≫ η ▷ 𝟙_ C) ≫ (ρ_ A).hom = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 2 3 =>
    rw [rightUnitor_naturality]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (ε ⊗ₘ ε) ≫ (ρ_ (𝟙_ C)).hom ≫ η = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ * (𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ = 1

Tactic:
· rw [Conv.mul_eq, Conv.one_eq]
    simp only [Comon.tensorObj_comul, whiskerRight_tensor,
      BraidedCategory.braiding_naturality_assoc, whiskerLeft_comp, Category.assoc,
      Comon.tensorObj_counit]
    simp only [tensorμ]
    simp only [Category.assoc, pentagon_hom_inv_inv_inv_inv_assoc]
    exact mul_antipode₂ A

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

Goal state before:
pp: case refine_1
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)
H : ∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
⊢ ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

Tactic:
obtain ⟨W, u, v, huv, hW⟩ := H (CategoryTheory.Under.homMk (U := CategoryTheory.Under.mk p)
        (V := CategoryTheory.Under.mk f) g hpg)

Goal state after:
case refine_1
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)
H : ∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
W : Under X
u : CategoryTheory.Under.mk p ⟶ W
v : W ⟶ CategoryTheory.Under.mk f
huv : u ≫ v = CategoryTheory.Under.homMk g hpg
hW : P.underObj W
⊢ ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j : J
g : X ⟶ p.diag.obj j
⊢ ∃ a, (fun g ↦ f ≫ g) a = g ≫ { pt := Z, ι := p.ι }.ι.app j

Tactic:
obtain ⟨g, rfl⟩ := (p.prop_diag_obj j _ hf).2 g

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j : J
g : Y ⟶ p.diag.obj j
⊢ ∃ a, (fun g ↦ f ≫ g) a = (fun g ↦ f ≫ g) g ≫ { pt := Z, ι := p.ι }.ι.app j
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
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
A : Set X
hA : HasCardinalLT (↑A) κ₂
this :
  ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → ↑(transfiniteIterate (φ Y m) j A)),
    HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
⊢ IsCardinalFiltered (↑(⋃ j, transfiniteIterate (φ Y m) j A)) κ₁

Tactic:
refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_)
    rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK
    have (k : K) : ∃ (j : κ₁.ord.ToType), (f k).val ∈ transfiniteIterate (φ Y m) j A := by
      simpa only [Set.mem_iUnion] using (f k).prop
    choose a ha using this
    obtain ⟨⟨z, hz⟩, hz'⟩ := this (IsCardinalFiltered.max a hK) (fun k ↦
      ⟨(f k).val, monotone_transfiniteIterate_φ Y hY' m A
          (leOfHom (IsCardinalFiltered.toMax a hK k)) (ha k)⟩) hK
    exact ⟨⟨z, Set.subset_iUnion _ _ hz⟩, hz'⟩

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:
by simp [φ]

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

Goal state before:
pp: case refine_1.of
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T : Presieve Y
hT : T ∈ (extensiveCoverage C ⊔ regularCoverage C).coverings Y
⊢ generate T ∈ (coherentTopology C) Y

Tactic:
| of Y T hT =>

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

Goal state before:
pp: case refine_2.of
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T : Presieve Y
hT : T ∈ (coherentCoverage C).coverings Y
⊢ generate T ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck Y

Tactic:
| of Y T hT =>

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

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.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
this : Precoherent C
⊢ S ∈ (coherentTopology C) X ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
← coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily S

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
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
this : Precoherent C
⊢ S ∈ (coherentTopology C) X ↔ S ∈ (coherentTopology C) X
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
⊢ (ConcreteCategory.hom (f.app (op (∐ Z)))) ((ConcreteCategory.hom i'.hom) x) =
    (ConcreteCategory.hom (G.map (Sigma.desc π).op)) y

Tactic:
have := preservesLimitsOfShape_of_equiv (Discrete.opposite α).symm G

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
⊢ (ConcreteCategory.hom (f.app (op (∐ Z)))) ((ConcreteCategory.hom i'.hom) x) =
    (ConcreteCategory.hom (G.map (Sigma.desc π).op)) y
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)
⊢ f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d

Tactic:
refine Multifork.IsLimit.hom_ext hc fun a ↦ ?_
  have heq := d.condition ⟨⟨(f.s₀ a), (g.s₀ a)⟩, H.H a⟩
  simp only [multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
    multicospanIndex_fst, multicospanShape_snd, multicospanIndex_snd] at heq
  simp [-Homotopy.wl, -Homotopy.wr, ← H.wl, ← H.wr, reassoc_of% heq]

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'
j : ι'
g : Y ⟶ X' j
hg : g ≫ f' j = q
⊢ pullFunctorObjHom w D (g ≫ f' j) g g ⋯ ⋯ =
    𝟙 ((F.map g.op.toLoc).toFunctor.obj ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))))

Tactic:
pullFunctorObjHom_eq _ _ _ _ _ _ _ _ rfl rfl rfl rfl rfl,

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'
j : ι'
g : Y ⟶ X' j
hg : g ≫ f' j = q
⊢ (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j)) ≫
      D.hom ((g ≫ f' j) ≫ p) (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫
        (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j)) =
    𝟙 ((F.map g.op.toLoc).toFunctor.obj ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))))