mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (Δ ▷ A ≫ (A ⊗ A) ◁ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  ((α_ A A (A ⊗ A)).hom ≫ A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
rw [pentagon_inv_inv_hom_hom_inv_assoc]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ▷ A ≫ (A ⊗ A) ◁ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            A ◁ (α_ A A A).hom ≫
              (α_ A A (A ⊗ A)).inv ≫
                ((α_ A A (A ⊗ A)).hom ≫ A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                  (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
r : R
a : ↑A
⊢ (Hom.hom η) r * a = a * (Hom.hom η) r

Tactic:
have h₁ := LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A)) (r ⊗ₜ a)

Goal state after:
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
r : R
a : ↑A
h₁ :
  (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ)) (r ⊗ₜ[R] a) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor A).hom) (r ⊗ₜ[R] a)
⊢ (Hom.hom η) r * a = a * (Hom.hom η) r
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (β_ Y X).inv ▷ Y ⊗≫ Y ◁ (β_ X Y).hom =
    𝟙 ((X ⊗ Y) ⊗ Y) ⊗≫ X ◁ (β_ Y Y).hom ⊗≫ (β_ X Y).hom ▷ Y ⊗≫ Y ◁ (β_ Y X).inv ⊗≫ (β_ Y Y).inv ▷ X ⊗≫ 𝟙 (Y ⊗ Y ⊗ X)

Tactic:
simp only [monoidalComp, MonoidalCoherence.assoc_iso, MonoidalCoherence.whiskerRight_iso,
        MonoidalCoherence.refl_iso, whiskerRightIso_refl, Iso.trans_refl,
        MonoidalCoherence.assoc'_iso, Iso.refl_trans, Iso.symm_hom, comp_id, id_comp]

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (β_ Y X).inv ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ X Y).hom =
    (α_ X Y Y).hom ≫
      X ◁ (β_ Y Y).hom ≫
        (α_ X Y Y).inv ≫
          (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
⊢ Function.Surjective fun i ↦ ⟨Arrow.mk (f i), ⋯⟩

Tactic:
rintro ⟨f, hf⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f✝ : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow C
hf : f ∈ (ofHoms f✝).toSet
⊢ ∃ a, (fun i ↦ ⟨Arrow.mk (f✝ i), ⋯⟩) a = ⟨f, hf⟩
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    (M.actLeft ≫ f.hom) ≫ (λ_ N.X).inv ≫ η ▷ N.X ≫ coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

Tactic:
slice_rhs 1 2 => rw [Hom.left_act_hom]

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 : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    (((X.X ◁ f.hom ≫ N.actLeft) ≫ (λ_ N.X).inv) ≫ η ▷ N.X) ≫
      coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
⊢ (f.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app
        (Total.mk P (IsFiltered.coeq f.base g.base) a').snd =
    (g.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app (Total.mk P (IsFiltered.coeq f.base g.base) a').snd

Tactic:
simp only [Category.assoc, Functor.const_obj_obj, ← u.w, ← f.w_assoc, ← g.w_assoc]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
⊢ (P k.fst).ι.app k.snd ≫ D.map f.base ≫ D.map u.base = (P k.fst).ι.app k.snd ≫ D.map g.base ≫ D.map u.base
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
⊢ ∀ ⦃X Y : Arrow V⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y),
    rightHomotopic V f₁ f₂ → rightHomotopic V g₁ g₂ → rightHomotopic V (f₁ + g₁) (f₂ + g₂)

Tactic:
rintro _ _ _ _ _ _ ⟨h⟩ ⟨h'⟩

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
X✝ Y✝ : Arrow V
f₁✝ f₂✝ g₁✝ g₂✝ : X✝ ⟶ Y✝
h : RightHomotopy f₁✝ f₂✝
h' : RightHomotopy g₁✝ g₂✝
⊢ rightHomotopic V (f₁✝ + g₁✝) (f₂✝ + g₂✝)
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b c : X
⊢ m₂ (m₂ a b) c = m₂ a (m₂ b c)

Tactic:
by simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib a b e₂ c

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ Function.Surjective fun x ↦ ⟨Arrow.mk (𝟙 j), ⋯⟩

Tactic:
rintro ⟨f, hf⟩

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
f : Arrow J
hf : f ∈ (MorphismProperty.ofHoms fun x ↦ 𝟙 j).toSet
⊢ ∃ a, (fun x ↦ ⟨Arrow.mk (𝟙 j), ⋯⟩) a = ⟨f, hf⟩
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_1
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝ : J
h : __Diagram✝.P x✝
⊢ ∃ lift, __Diagram✝.W lift

pp: case refine_2
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝² : J
h₁ : __Diagram✝.P x✝²
x✝¹ x✝ : x✝² ⟶ j
h₂ : __Diagram✝.W x✝¹
h₃ : __Diagram✝.W x✝
⊢ x✝¹ = x✝

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:
· simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h
      subst h
      exact ⟨𝟙 _, ⟨⟨⟩⟩⟩

Goal state after:
case refine_2
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝² : J
h₁ : __Diagram✝.P x✝²
x✝¹ x✝ : x✝² ⟶ j
h₂ : __Diagram✝.W x✝¹
h₃ : __Diagram✝.W x✝
⊢ x✝¹ = x✝

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
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 Y : J
⊢ ∃ li lj, __Diagram✝.W li ∧ __Diagram✝.W lj ∧ 𝟙 j ≫ lj = li

Tactic:
exact ⟨𝟙 _, 𝟙 _, ⟨⟨⟩⟩, ⟨⟨⟩⟩, 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
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
⊢ ∃ m u,
    (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
      ∀ (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₂

Tactic:
let t₁ (i : ι) : m₀ i ⟶ m₁ := IsCardinalFiltered.toMax m₀ hι i

Goal state after:
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
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
⊢ ∃ m u,
    (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
      ∀ (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₂
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
⊢ ∀ {i j : J} {f : i ⟶ j},
    ((D₁ D hι m).W ⊔ MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst) f → (D₁ D hι m).P i

Tactic:
simp only [D₁_W, D₁_P]
    rintro _ _ _ ((hf | ⟨⟨⟩⟩) | ⟨i, j, hj⟩)
    · simp only [MorphismProperty.iSup_iff] at hf
      obtain ⟨i, hf⟩ := hf
      exact Or.inl ⟨i, (D i).src hf⟩
    · exact Or.inr rfl
    · exact Or.inl ⟨i, hj⟩

Goal state after:
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Cᵒᵖ ⥤ Type w
e : F ≅ F'
⊢ F'.IsRepresentedBy ((ConcreteCategory.hom (e.hom.app (op X))) x)

Tactic:
rw [iff_exists_representableBy]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Cᵒᵖ ⥤ Type w
e : F ≅ F'
⊢ ∃ R, R.homEquiv (𝟙 X) = (ConcreteCategory.hom (e.hom.app (op X))) x
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
e : Y ≅ X
⊢ F.IsRepresentedBy ((ConcreteCategory.hom (F.map e.hom.op)) x)

Tactic:
rw [iff_exists_representableBy]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
Y : C
e : Y ≅ X
⊢ ∃ R, R.homEquiv (𝟙 Y) = (ConcreteCategory.hom (F.map e.hom.op)) x
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
A B : C
f : A ⟶ B
A' : Subobject A
B' : Subobject B
⊢ MorphismProperty.regularEpi C (imageFactorisation f A').F.e

Tactic:
have := strongEpi_of_strongEpiMonoFactorisation (strongEpiMonoFactorisation (A'.arrow ≫ f))
    (imageFactorisation f A').isImage

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f✝ : X ⟶ Y
A B : C
f : A ⟶ B
A' : Subobject A
B' : Subobject B
this : StrongEpi (imageFactorisation f A').F.e
⊢ MorphismProperty.regularEpi C (imageFactorisation f A').F.e
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ pullHom (pullHom φ g gf₁ gf₂ hgf₁ hgf₂) g' g'f₁ g'f₂ hg'f₁ hg'f₂ = pullHom φ (g' ≫ g) g'f₁ g'f₂ ⋯ ⋯

Tactic:
dsimp [pullHom]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' gf₁.op.toLoc g'.op.toLoc g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map g'.op.toLoc).toFunctor.map
          ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
            (F.map g.op.toLoc).toFunctor.map φ ≫
              (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app M₂) ≫
        (F.mapComp' gf₂.op.toLoc g'.op.toLoc g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ (ConcreteCategory.hom
          (((Over.map q).op ⋙ F.presheafHom M N).map (op f) ≫
            (((Cat.Hom.toNatIso
                            (F.mapComp' q.op.toLoc (unop (op T₂)).hom.op.toLoc
                              ((Over.map q).obj (unop (op T₂))).hom.op.toLoc ⋯)).app
                        M).homFromEquiv.trans
                  ((Cat.Hom.toNatIso
                          (F.mapComp' q.op.toLoc (unop (op T₂)).hom.op.toLoc
                            ((Over.map q).obj (unop (op T₂))).hom.op.toLoc ⋯)).app
                      N).homToEquiv).toIso.hom)).toFun
      g =
    (ConcreteCategory.hom
          ((((Cat.Hom.toNatIso
                            (F.mapComp' q.op.toLoc (unop (op T₁)).hom.op.toLoc
                              ((Over.map q).obj (unop (op T₁))).hom.op.toLoc ⋯)).app
                        M).homFromEquiv.trans
                  ((Cat.Hom.toNatIso
                          (F.mapComp' q.op.toLoc (unop (op T₁)).hom.op.toLoc
                            ((Over.map q).obj (unop (op T₁))).hom.op.toLoc ⋯)).app
                      N).homToEquiv).toIso.hom ≫
            (F.presheafHom ((F.map q.op.toLoc).toFunctor.obj M) ((F.map q.op.toLoc).toFunctor.obj N)).map (op f))).toFun
      g

Tactic:
dsimp [pullHom]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ ((F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                    ⋯).hom.toNatTrans.app
            M ≫
          (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
            (F.mapComp' (q.op.toLoc ≫ T₁.hom.op.toLoc) (Over.Hom.left f).op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc)
                      ⋯).inv.toNatTrans.app
              N) ≫
      (F.mapComp' q.op.toLoc T₂.hom.op.toLoc (q.op.toLoc ≫ T₂.hom.op.toLoc) ⋯).hom.toNatTrans.app N =
    (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map q.op.toLoc).toFunctor.obj M) ≫
      (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
          (((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).inv.toNatTrans.app M ≫ g) ≫
            (F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).hom.toNatTrans.app N) ≫
        (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).inv.toNatTrans.app
          ((F.map q.op.toLoc).toFunctor.obj N)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₂.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).inv) =
    (e i₁).inv ≫ D₁.hom i₁ i₂

Tactic:
by
    rw [← cancel_epi (e i₁).hom, ← reassoc_of% (comm i₁ i₂), ← Functor.map_comp, ← Functor.map_comp]
    simp

Goal state after:
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)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ pullHom (pullHom (hom i₁ i₂) p f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ = pullHom (hom i₁ i₂) (g ≫ p) gf₁ gf₂ ⋯ ⋯

Tactic:
dsimp [pullHom]

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)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ (F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      (F.map g.op.toLoc).toFunctor.map
          ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
            (F.map p.op.toLoc).toFunctor.map (hom i₁ i₂) ≫
              (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)) ≫
        (F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂) =
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc (p.op.toLoc ≫ g.op.toLoc) gf₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      (F.map (p.op.toLoc ≫ g.op.toLoc)).toFunctor.map (hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc (p.op.toLoc ≫ g.op.toLoc) gf₂.op.toLoc ⋯).inv.toNatTrans.app (obj' i₂)
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₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
q' : Y ⟶ S
f₁' : Y ⟶ X (α j₁)
f₂' : Y ⟶ X (α j₂)
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
hq' : q ≫ p = q'
hf₁' : f₁ ≫ p' j₁ = f₁'
hf₂' : f₂ ≫ p' j₂ = f₂'
⊢ pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc f₁'.op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom q' f₁' f₂' ⋯ ⋯ ≫ (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc f₂'.op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))

Tactic:
subst hq' hf₁' hf₂'
  simp [mapComp'_eq_mapComp, pullFunctorObjHom]

Goal state after: