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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ ((P.actRight ≫ (ρ_ P.X).inv) ≫ P.X ◁ η) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ))

Tactic:
slice_lhs 1 2 => rw [rightUnitor_inv_naturality]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (((ρ_ (P.X ⊗ S.X)).inv ≫ P.actRight ▷ 𝟙_ C) ≫ P.X ◁ η) ≫
      coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (P.X ⊗ S.X) ◁ η ≫
        ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ))

Tactic:
slice_lhs 2 3 => rw [associator_naturality_right]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (((α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ S.X ◁ η) ≫ P.X ◁ μ) ≫
        coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ))
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
P : ObjectProperty C
w✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ P ≤ (isCardinalPresentable C κ).isoClosure

Tactic:
ObjectProperty.isoClosure_eq_self

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
P : ObjectProperty C
w✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ P ≤ isCardinalPresentable C κ
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
X : C
⊢ (isCardinalPresentable C κ).ι.isDenseAt X

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ :=
      (isCardinalFilteredGenerator_isCardinalPresentable C κ).exists_colimitsOfShape X
    exact ⟨(Functor.Final.isColimitWhiskerEquiv (F := p.toCostructuredArrow) _).1
      (IsColimit.ofIsoColimit p.isColimit (Cocone.ext (Iso.refl _)))⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
f : X ⟶ Y
hf : sourceLocalClosure K P f
⊢ Q f

Tactic:
induction hf with

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

Goal state before:
pp: C✝ : Type u₁
inst✝¹³ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹² : Category.{v₂, u₂} V✝
inst✝¹¹ : MonoidalCategory C✝
inst✝¹⁰ : MonoidalCategory V✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
inst✝³ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this✝¹ : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
d₁ d₂ d₃ : D
x₁ x₂ x₃ : C
this✝ : DayConvolution ((ι C V D).obj d₁) ((ι C V D).obj d₂ ⊛ (ι C V D).obj d₃) :=
  convolutions C V d₁ (tensorObj C V d₂ d₃)
this : DayConvolution ((ι C V D).obj d₁ ⊛ (ι C V D).obj d₂) ((ι C V D).obj d₃) :=
  convolutions C V (tensorObj C V d₁ d₂) d₃
⊢ (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₂)).app (x₁, x₂) ▷ ((ι C V D).obj d₃).obj x₃ ≫
      (DayConvolution.unit ((ι C V D).obj (d₁ ⊗ d₂)) ((ι C V D).obj d₃)).app (x₁ ⊗ x₂, x₃) ≫
        (DayConvolution.associator ((ι C V D).obj d₁) ((ι C V D).obj d₂) ((ι C V D).obj d₃)).hom.app ((x₁ ⊗ x₂) ⊗ x₃) =
    (α_ (((ι C V D).obj d₁).obj x₁) (((ι C V D).obj d₂).obj x₂) (((ι C V D).obj d₃).obj x₃)).hom ≫
      ((ι C V D).obj d₁).obj x₁ ◁ (DayConvolution.unit ((ι C V D).obj d₂) ((ι C V D).obj d₃)).app (x₂, x₃) ≫
        (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj (d₂ ⊗ d₃))).app (x₁, x₂ ⊗ x₃) ≫
          ((ι C V D).obj (d₁ ⊗ d₂ ⊗ d₃)).map (α_ x₁ x₂ x₃).inv

Tactic:
apply DayConvolution.associator_hom_unit_unit

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

Goal state before:
pp: case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
F : (i : E.I₀) → K.ZeroHypercover (E.X i)
hF : ∀ (i : E.I₀), S i = Presieve.ofArrows (F i).X (F i).f
U : C
g : U ⟶ X✝
x✝ : (E.bind F).presieve₀ g
j : (E.bind F).I₀
⊢ P ((F j.fst).f j.snd ≫ E.f j.fst ≫ f)

Tactic:
exact h' _ _ _ (by simp [hF])

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
⊢ (c : ι) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})

Tactic:
intro c

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
⊢ ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition i.inv c * o.matrixDecomposition i.hom c = 1

Tactic:
rw [← o.matrixDecomposition_comp]
        simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition i.hom c * o.matrixDecomposition i.inv c = 1

Tactic:
rw [← o.matrixDecomposition_comp]
        simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)

Tactic:
leftAdd,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) ≫ biprod.desc (𝟙 Y) (𝟙 Y) =
    rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
f : End X
hf : f ≠ 0
⊢ inv f ≫ f = 𝟙 X

Tactic:
have := isIso_of_hom_simple hf

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
f : End X
hf : f ≠ 0
this : IsIso f
⊢ inv f ≫ f = 𝟙 X
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ x_1,
      if h : x_1.fst = j then
        if h_1 : ⋯ ▸ x_1.snd = x then
          if h_2 : x_1.fst = j' then if h_3 : ⋯ ▸ x_1.snd = y then eqToHom ⋯ ≫ eqToHom ⋯ else eqToHom ⋯ ≫ 0
          else eqToHom ⋯ ≫ 0
        else if h : x_1.fst = j' then if h_2 : ⋯ ▸ x_1.snd = y then 0 ≫ eqToHom ⋯ else 0 ≫ 0 else 0 ≫ 0
      else if h : x_1.fst = j' then if h_1 : ⋯ ▸ x_1.snd = y then 0 ≫ eqToHom ⋯ else 0 ≫ 0 else 0 ≫ 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
simp only [ite_self, dite_eq_ite, Limits.comp_zero, Limits.zero_comp,
                eqToHom_trans]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ x_1,
      if h : x_1.fst = j then
        if h_1 : ⋯ ▸ x_1.snd = x then if h_2 : x_1.fst = j' then if h_3 : ⋯ ▸ x_1.snd = y then eqToHom ⋯ else 0 else 0
        else 0
      else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
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₂
⊢ g₁ = g₂

Tactic:
obtain ⟨j, g₁, g₂, rfl, rfl⟩ :
      ∃ (j : κ.ord.ToType) (g₁' g₂' : Y ⟶ H.F.obj j), g₁' ≫ H.incl.app j = g₁ ∧
        g₂' ≫ H.incl.app j = g₂ := 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:
case refine_1
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 κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.F.obj j
h : (fun g ↦ f ≫ g) (g₁ ≫ H.incl.app j) = (fun g ↦ f ≫ g) (g₂ ≫ H.incl.app j)
⊢ g₁ ≫ H.incl.app j = g₂ ≫ H.incl.app j
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf : (D₂ D hι u).W f
⊢ f = 𝟙 m

Tactic:
simp only [D₂_W] at hf
  obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
  · simp only [MorphismProperty.iSup_iff] at hf
    obtain ⟨i, hi⟩ := hf
    exact (hD ((D i).src hi)).elim
  · rfl
  · rw [MorphismProperty.ofHoms_iff] at hf
    obtain ⟨⟨i, j, hj⟩, hi⟩ := hf
    obtain rfl : m = j := congr_arg Arrow.leftFunc.obj hi
    exact (hD hj).elim

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

Goal state before:
pp: case inr
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
i : ι
X Y : J
i' : ι
j : J
hj' : (D i').P j
hj : (D i).P ↑⟨i', ⟨j, hj'⟩⟩.snd
⊢ (D ⟨i', ⟨j, hj'⟩⟩.fst).isTerminal.lift ⋯ ≫ u ⟨i', ⟨j, hj'⟩⟩.fst = φ ⟨i, ⟨↑⟨i', ⟨j, hj'⟩⟩.snd, hj⟩⟩

Tactic:
apply hm

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
⊢ (M.associatorBimod (regular Y) N).hom ≫ M.whiskerLeft N.leftUnitorBimod.hom = whiskerRight M.rightUnitorBimod.hom N

Tactic:
dsimp [associatorBimod, leftUnitorBimod, rightUnitorBimod]

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
⊢ (isoOfIso
          { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }
          ⋯ ⋯).hom ≫
      M.whiskerLeft
        (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom =
    whiskerRight
      (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯).hom
      N
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ Type u_4
W X B : C
f : X ⟶ B
g₁ g₂ : W ⟶ X
w : g₁ ≫ f = g₂ ≫ f
t : P.obj (op B)
⊢ (ConcreteCategory.hom (P.map f.op)) t ∈
    {x | (ConcreteCategory.hom (P.map g₁.op)) x = (ConcreteCategory.hom (P.map g₂.op)) x}

Tactic:
simp only [Set.mem_ofPred_eq, ← comp_apply, ← Functor.map_comp, ← op_comp, w]

Goal state after:
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
i : J
⊢ Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Tactic:
exact (G.obj i).property

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 ↔ S ∈ (F.inducedTopology (coherentTopology D)) X

Tactic:
rw [← exists_effectiveEpiFamily_iff_mem_induced F X]

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 ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
⊢ ∃ a,
    op i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧
      op j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a

Tactic:
have hi := Over.w i.hom

Goal state after:
case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
hi :
  Over.Hom.left i.hom ≫ (unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))).obj.hom =
    (unop (op Z)).obj.hom
⊢ ∃ a,
    op i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧
      op j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)) → SingleEqualizerCondition P π

Tactic:
intro ⟨h⟩
    exact fun c hc ↦ ⟨(isLimit_forkOfι_equiv _ _ _ hc).symm 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
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₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ (f₁ ≫ p' j₁) ≫ f (α j₁) = q ≫ p

Tactic:
simp [w, reassoc_of% hf₁]

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)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ pullHom' (ofDescentData sq sq₃ D).hom q f₁ f₂ hf₁ hf₂ = D.hom q f₁ f₂ hf₁ hf₂

Tactic:
obtain ⟨p, h₁, h₂⟩ := (sq i₁ i₂).isPullback.exists_lift f₁ f₂ (by cat_disch)
  rw [pullHom'_eq_pullHom _ _ _ _ p]
  dsimp
  rw [D.pullHom_hom _ _ _ (by rw [← (sq i₁ i₂).hp₁, reassoc_of% h₁, hf₁]) _ _
    (by simp) (by simp) _ _ h₁ h₂]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
| Φ.toPresheafFiber X x ((P₁ ⊗ P₂) ⊗ P₃) ≫
    Φ.presheafFiber.map (α_ P₁ P₂ P₃).hom ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x (P₂ ⊗ P₃)) ⋯ ≫
        Φ.presheafFiber.obj P₁ ◁ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃) ⋯

Tactic:
simp only [toPresheafFiber_naturality_assoc, toPresheafFiber_presheafFiberDesc_assoc,
        tensorHom_def_assoc, ← MonoidalCategory.whiskerLeft_comp,
        toPresheafFiber_presheafFiberDesc]
      rw [← tensorHom_def]
      dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
| (α_ (P₁.obj (Opposite.op X)) (P₂.obj (Opposite.op X)) (P₃.obj (Opposite.op X))).hom ≫
    (Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃)
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
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
S : Sieve (Over.mk f)
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ S ∈ (J.over X) (Over.mk f)

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

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
S : Sieve (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm S).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ (Sieve.overEquiv (Over.mk f)).symm S ∈ (J.over X) (Over.mk f)