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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            ((β_ B (i.obj ((reflector i).obj A))).inv ≫
              uncurry
                ((unitCompPartialBijective A ⋯)
                  (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f ≫ i.map g)))))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            ((β_ B (i.obj ((reflector i).obj A))).inv ≫
              uncurry
                ((unitCompPartialBijective A ⋯)
                  (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f ≫ i.map g)))))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            ((β_ B (i.obj ((reflector i).obj A))).inv ≫
              uncurry
                ((unitCompPartialBijective A ⋯)
                  (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f ≫ i.map g)))))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            ((β_ B (i.obj ((reflector i).obj A))).inv ≫
              uncurry
                ((unitCompPartialBijective A ⋯)
                  (curry ((((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f) ≫ i.map g)))))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            ((β_ B (i.obj ((reflector i).obj A))).inv ≫
              uncurry
                  ((unitCompPartialBijective A ?hB)
                    (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f))) ≫
                i.map g))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

pp: case hB
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.essImage (B ⟹ i.obj X)

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            (((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ?hB)
                    (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f)))) ≫
              i.map g))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

case hB
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.essImage (B ⟹ i.obj X)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.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) ◁ Δ ≫ (α_ A A (A ⊗ A)).hom

pp: case a.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 A).inv

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 ▷ 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
| 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 (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
| μ ⊗ₘ μ

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:
← Category.assoc,

Goal state after:
case a.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) ◁ Δ) ≫ (α_ A A (A ⊗ A)).hom

case a.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 A).inv

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 ▷ 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
| 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 (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
| μ ⊗ₘ μ

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: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ 𝒮 ≫ Δ = Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮)

Tactic:
apply left_inv_eq_right_inv
    (M := Conv A (A ⊗ A))
    (a := Δ[A])
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [comp_whiskerRight, tensor_whiskerLeft, MonObj.tensorObj.mul_def, Category.assoc,
      MonObj.tensorObj.one_def]
    simp only [tensorμ]
    simp only [Category.assoc, Iso.inv_hom_id_assoc]
    exact antipode_comul₁ A
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [whiskerLeft_comp, tensor_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc,
      MonObj.tensorObj.mul_def, MonObj.tensorObj.one_def]
    simp only [tensorμ]
    simp only [Category.assoc, Iso.inv_hom_id_assoc]
    exact antipode_comul₂ A

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

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (λ_ (R.X ⊗ P.X)).inv

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| η ▷ (R.X ⊗ P.X)

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (α_ R.X R.X P.X).inv

Tactic:
← Category.assoc,

Goal state after:
case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (λ_ (R.X ⊗ P.X)).inv

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| η ▷ (R.X ⊗ P.X)

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (α_ R.X R.X P.X).inv
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X : C
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)

Tactic:
rw [CategoryTheory.Functor.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X : C
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)

Tactic:
rw [CategoryTheory.Functor.map_id]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
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)
j j' : J
i : I j
u : j ⟶ j'
inst✝¹ : IsFiltered (I j')
inst✝ : IsFinitelyPresentable ((P j).diag.obj i)
i' : I j'
q : (P j).diag.obj i ⟶ (P j').diag.obj i'
hq : q ≫ { pt := D.obj j', ι := (P j').ι }.ι.app i' = (P j).ι.app i ≫ D.map u
⊢ (P (mk P j i).fst).ι.app (mk P j i).snd ≫ D.map u = q ≫ (P (mk P j' i').fst).ι.app (mk P j' i').snd

Tactic:
by simp [← hq]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
⊢ ∃ c, Nonempty (f ⟶ p.toCostructuredArrow.obj c)

Tactic:
obtain ⟨j, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit f.hom
    exact ⟨j, ⟨CostructuredArrow.homMk (ObjectProperty.homMk g)⟩⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
j : J
g₁ g₂ : f ⟶ p.toCostructuredArrow.obj j
⊢ ∃ c' t, g₁ ≫ p.toCostructuredArrow.map t = g₂ ≫ p.toCostructuredArrow.map t

Tactic:
obtain ⟨k, a, h⟩ := IsCardinalPresentable.exists_eq_of_isColimit' κ p.isColimit
      g₁.left.hom g₂.left.hom ((CostructuredArrow.w g₁).trans (CostructuredArrow.w g₂).symm)
    exact ⟨k, a, by cat_disch⟩

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

Goal state before:
pp: case refine_1.of_iso
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✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
U : C
v : U ⟶ X'✝
i : (Precoverage.ZeroHypercover.pushforward (Arrow.Hom.left e.hom) ⋯ E).I₀
⊢ P (E.f i ≫ f ≫ Arrow.Hom.right e.hom)

Tactic:
← Category.assoc,

Goal state after:
case refine_1.of_iso
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✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
U : C
v : U ⟶ X'✝
i : (Precoverage.ZeroHypercover.pushforward (Arrow.Hom.left e.hom) ⋯ E).I₀
⊢ P ((E.f i ≫ f) ≫ Arrow.Hom.right e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.comp
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✝
hf : sourceLocalClosure K P f
R : Presieve X✝
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
U✝ : C
g : U✝ ⟶ X✝
hg : R g
S : Presieve X✝
hS : ∃ 𝒰, S = Presieve.ofArrows 𝒰.X 𝒰.f
h : ∀ (U : C) (g : U ⟶ X✝), S g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings U✝, ∀ (U : C) (g_1 : U ⟶ U✝), R g_1 → P (g_1 ≫ g ≫ f)

Tactic:
obtain ⟨E, rfl⟩ := hS

Goal state after:
case refine_1.comp
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✝
hf : sourceLocalClosure K P f
R : Presieve X✝
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
U✝ : C
g : U✝ ⟶ X✝
hg : R g
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings U✝, ∀ (U : C) (g_1 : U ⟶ U✝), R g_1 → P (g_1 ≫ g ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.comp
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✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (pullback.fst g (E.f i) ≫ g ≫ f)

Tactic:
rw [pullback.condition_assoc]

Goal state after:
case refine_1.comp
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✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (pullback.snd g (E.f i) ≫ E.f i ≫ f)
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ (MonoOver X)ᵒᵖ
⊢ IsFiltered.IsEventuallyConstant G

Tactic:
obtain ⟨n, hn⟩ := h ⟨_, (G ⋙ (Subobject.equivMonoOver X).inverse.op ⋙
      (orderDualEquivalence _).inverse).monotone⟩
    refine ⟨n, fun m hm ↦ ?_⟩
    rw [← isIso_unop_iff, MonoOver.isIso_iff_subobjectMk_eq]
    exact (hn m (leOfHom hm)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g✝¹ : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
w : Arrow V
g✝ : v ⟶ w
h : RightHomotopy (f ≫ g✝) 0
A✝ : RightFreyd V
g : (quotient V).obj v ⟶ A✝
hg : (quotient V).map f ≫ g = 0
⊢ Nonempty { l // (quotient V).map (π f) ≫ l = g }

Tactic:
obtain ⟨g, rfl⟩ := (quotient V).map_surjective g
      exact ⟨(quotient V).map (desc f g (homotopyOfEq _ _ hg)),
        by simp [← Functor.map_comp]⟩

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

Goal state before:
pp: case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : j' = j
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0

Tactic:
subst h
                simp

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

Goal state before:
pp: case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0

Tactic:
rw [dif_neg h, dif_neg (Ne.symm h)]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
⊢ F.map f =
    (additiveObjIsoBiproduct F M).hom ≫
      (biproduct.matrix fun i j ↦ F.map ((embedding C).map (f i j))) ≫ (additiveObjIsoBiproduct F N).inv

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
⊢ F.map f =
    ((additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j ↦ F.map ((embedding C).map (f i j))) ≫
      (additiveObjIsoBiproduct F N).inv