mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ g =
    (whiskerRight (ψ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i

Tactic:
simpa using! i.hom.2.w.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ C
F : C ⥤ Type u₂
inst✝¹ : HasColimit (D.op ⋙ coyoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        (((colimitHomIsoLimitYoneda' (D.op ⋙ coyoneda) F).hom ≫ limit.π ((D.op ⋙ coyoneda).rightOp ⋙ yoneda.obj F) i) ≫
          ((D ⋙ Prod.sectL C F).isoWhiskerLeft (coyonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i))) (𝟙 (D.obj i))) }

Tactic:
colimitHomIsoLimitYoneda'_hom_comp_π

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ C
F : C ⥤ Type u₂
inst✝¹ : HasColimit (D.op ⋙ coyoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((yoneda.obj F).map (colimit.ι (D.op ⋙ coyoneda) (op i)).op ≫
          ((D ⋙ Prod.sectL C F).isoWhiskerLeft (coyonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i))) (𝟙 (D.obj i))) }
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        (((colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F).hom ≫
            limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ yoneda.obj F) i) ≫
          ((D ⋙ Prod.sectL Cᵒᵖ F).isoWhiskerLeft (yonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }

Tactic:
colimitHomIsoLimitYoneda'_hom_comp_π

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((yoneda.obj F).map (colimit.ι (D.leftOp ⋙ yoneda) (op i)).op ≫
          ((D ⋙ Prod.sectL Cᵒᵖ F).isoWhiskerLeft (yonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1).inv.f 0 ≫
      (HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat).f 0 =
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv

Tactic:
HomologicalComplex.extendMap_f _ _ (i := 0) (by simp),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1).inv.f 0 ≫
      (((HomologicalComplex.single C (ComplexShape.up ℕ) 0).obj X).extendXIso ComplexShape.embeddingUpNat ⋯).hom ≫
        R.ι.f 0 ≫ (HomologicalComplex.extendXIso R.cocomplex ComplexShape.embeddingUpNat ⋯).inv =
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
this : ∑ x ∈ F.attach, r x • (ModuleCat.Hom.hom f) (↑x).as = 0
⊢ ∑ x ∈ F.attach,
      h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun a ↦ G) x ≫ (ModuleCat.Hom.hom f) (↑x).as =
    0

Tactic:
by simpa [End.smul_left, r] using this

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ (HomologicalComplex.extendMap R.π ComplexShape.embeddingDownNat).f 0 ≫
      (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1).hom.f 0 =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv

Tactic:
HomologicalComplex.extendMap_f _ _ (i := 0) (by simp),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ ((HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat ⋯).hom ≫
        R.π.f 0 ≫
          (HomologicalComplex.extendXIso ((ChainComplex.single₀ C).obj X) ComplexShape.embeddingDownNat ⋯).inv) ≫
      (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1).hom.f 0 =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1) + 0 -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0

Tactic:
add_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
⊢ ⟦Over.mk (a.hom ≫ f)⟧ = ⟦Over.mk (a'.hom ≫ f)⟧

Tactic:
convert!
    ha

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ X' s, ∃ (_ : P.isoModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)

Tactic:
refine ⟨?_, fun hf ↦ ?_⟩
  · rintro ⟨Y', s, hs, eq⟩
    rw [← exists_epiModSerre_comp_eq_zero_iff P]
    exact ⟨Y', s, hs.2, eq⟩
  · refine ⟨_, kernel.ι f, ?_, by simp⟩
    simpa only [isoModSerre_iff_of_mono] using!
      P.prop_of_iso (Abelian.coimageIsoImage f).symm hf

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt},
    (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }

Tactic:
intro m

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
⊢ (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)

Tactic:
by
  induction n with
  | zero => exact Prod.ext rfl (funext fun x => Fin.elim0 x)
  | succ n hn =>
    refine Prod.ext rfl (funext fun x => ?_)
    induction x using Fin.cases
    <;> simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]
    <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: case refine_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ ∀ {m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt},
    (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π → m = ↑((h X).desc' s.π ⋯)

Tactic:
intro m

Goal state after:
case refine_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt
⊢ (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π → m = ↑((h X).desc' s.π ⋯)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: case refine_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt},
    m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = ↑((h X).lift' s.ι ⋯)

Tactic:
intro m

Goal state after:
case refine_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt
⊢ m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = ↑((h X).lift' s.ι ⋯)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ { f // F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f } ≃
    { g // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g }

Tactic:
apply (adj₂.homEquiv _ _).subtypeEquiv _

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ ∀ (a : F'.obj (U.obj X) ⟶ Y),
    F'.map (U.map (adj₁.counit.app X)) ≫ a = otherMap R F' adj₁ adj₂ X ≫ a ↔
      U.map (F.map ((adj₂.homEquiv (U.obj X) Y) a) ≫ adj₁.counit.app (R.obj Y)) =
        U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) a
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom

Tactic:
calc
      _ = h ◁ (unit s ≫ i.right ▷ f) := by simp [-LeftLift.w]
      _ = h ◁ unit t := congrArg (h ◁ ·) (LeftLift.w i)
      _ = _ := by simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵖ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        (η.naturality f).hom ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
simp_rw [Category.assoc, ← associator_inv_naturality_left, whisker_exchange_assoc]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵖ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
      (η.naturality f).hom ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
by
  subst h₀₂ h₁₃ hf
  simp [mapComp_assoc_right_hom, Strict.associator_eqToIso, mapComp']

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
F : typeToCat.obj X ⟶ C
x✝¹ x✝ : ↑(of (Discrete ((fun X ↦ X) X)))
as✝¹ as✝ : X
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((fun f ↦ (Discrete.functor ⇑(ConcreteCategory.hom f)).toCatHom)
            ((fun F ↦ ↾fun x ↦ F.toFunctor.obj { as := x }) F)).toFunctor.map
      f =
    eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯

Tactic:
obtain rfl := Discrete.eq_of_hom f

Goal state after:
X : Type u
C : Cat
F : typeToCat.obj X ⟶ C
x✝¹ x✝ : ↑(of (Discrete ((fun X ↦ X) X)))
as✝ : X
f : { as := as✝ } ⟶ { as := { as := as✝ }.as }
⊢ ((fun f ↦ (Discrete.functor ⇑(ConcreteCategory.hom f)).toCatHom)
            ((fun F ↦ ↾fun x ↦ F.toFunctor.obj { as := x }) F)).toFunctor.map
      f =
    eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
as✝¹ as✝ : objects.obj x✝²
f : { as := as✝¹ } ⟶ { as := as✝ }
⊢ ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
    (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f

Tactic:
obtain rfl := Discrete.eq_of_hom f

Goal state after:
X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
as✝ : objects.obj x✝²
f : { as := as✝ } ⟶ { as := { as := as✝ }.as }
⊢ ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
    (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf✝¹ : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a
pf✝ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a pf✝
⊢ C a

Tactic:
induction ‹Acc (Sum.inr · ∈ f ·) a› with

Goal state after:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a✝ : α
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf✝ : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a
a : α
ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun x y ↦ Sum.inr x ∈ f y) y
IH :
  (y : α) →
    (a : Sum.inr y ∈ f a) →
      b ∈
          WellFounded.fixF
            (fun a IH ↦
              Part.assert (f a).Dom fun hf ↦
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            y ⋯ →
        C y
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯
⊢ C a
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ (∃ h, ⟨f a, h⟩ = b) ↔ ↑b = f a

Tactic:
exists_subtype_mk_eq_iff,

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ f a = ↑b ↔ ↑b = f a
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : limit (homDiagram X✝ Y✝)
⊢ Types.Limit.mk (homDiagram X✝ Y✝)
      (fun j ↦
        (hom (limit.π (homDiagram X✝ X✝) j))
            (Types.Limit.mk (homDiagram X✝ X✝) (fun x ↦ 𝟙 ((hom (limit.π (F ⋙ objects) x)) X✝)) ⋯) ≫
          (hom (limit.π (homDiagram X✝ Y✝) j)) x✝)
      ⋯ =
    x✝

Tactic:
by
    apply Types.limit_ext.{v, v}
    simp [-homDiagram_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : limit (homDiagram X✝ Y✝)
⊢ Types.Limit.mk (homDiagram X✝ Y✝)
      (fun j ↦
        (hom (limit.π (homDiagram X✝ Y✝) j)) x✝ ≫
          (hom (limit.π (homDiagram Y✝ Y✝) j))
            (Types.Limit.mk (homDiagram Y✝ Y✝) (fun x ↦ 𝟙 ((hom (limit.π (F ⋙ objects) x)) Y✝)) ⋯))
      ⋯ =
    x✝

Tactic:
by
    apply Types.limit_ext.{v, v}
    simp [-homDiagram_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
W✝ X✝ Y✝ Z✝ : limit (F ⋙ objects)
x✝² : limit (homDiagram W✝ X✝)
x✝¹ : limit (homDiagram X✝ Y✝)
x✝ : limit (homDiagram Y✝ Z✝)
⊢ Types.Limit.mk (homDiagram W✝ Z✝)
      (fun j ↦
        (hom (limit.π (homDiagram W✝ Y✝) j))
            (Types.Limit.mk (homDiagram W✝ Y✝)
              (fun j ↦ (hom (limit.π (homDiagram W✝ X✝) j)) x✝² ≫ (hom (limit.π (homDiagram X✝ Y✝) j)) x✝¹) ⋯) ≫
          (hom (limit.π (homDiagram Y✝ Z✝) j)) x✝)
      ⋯ =
    Types.Limit.mk (homDiagram W✝ Z✝)
      (fun j ↦
        (hom (limit.π (homDiagram W✝ X✝) j)) x✝² ≫
          (hom (limit.π (homDiagram X✝ Z✝) j))
            (Types.Limit.mk (homDiagram X✝ Z✝)
              (fun j ↦ (hom (limit.π (homDiagram X✝ Y✝) j)) x✝¹ ≫ (hom (limit.π (homDiagram Y✝ Z✝) j)) x✝) ⋯))
      ⋯

Tactic:
by
    apply Types.limit_ext.{v, v}
    simp [-homDiagram_obj]

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  ((tensorBifunctor L W ε).obj (((tensorBifunctor L W ε).obj Y₁).obj Y₂)).map f₃ ≫
      (((associator L W ε).hom.app Y₁).app Y₂).app Y₃ =
    (((associator L W ε).hom.app Y₁).app Y₂).app X₃ ≫
      ((tensorBifunctor L W ε).obj Y₁).map (((tensorBifunctor L W ε).obj Y₂).map f₃)
h₂ :
  ((tensorBifunctor L W ε).map (((tensorBifunctor L W ε).obj Y₁).map f₂)).app X₃ ≫
      (((associator L W ε).hom.app Y₁).app Y₂).app X₃ =
    (((associator L W ε).hom.app Y₁).app X₂).app X₃ ≫
      ((tensorBifunctor L W ε).obj Y₁).map (((tensorBifunctor L W ε).map f₂).app X₃)
h₃ :
  ((tensorBifunctor L W ε).map (((tensorBifunctor L W ε).map f₁).app X₂)).app X₃ ≫
      (((associator L W ε).hom.app Y₁).app X₂).app X₃ =
    (((associator L W ε).hom.app X₁).app X₂).app X₃ ≫
      ((tensorBifunctor L W ε).map f₁).app (((tensorBifunctor L W ε).obj X₂).obj X₃)
⊢ (((tensorBifunctor L W ε).map (((tensorBifunctor L W ε).map f₁).app X₂)).app X₃ ≫
        ((tensorBifunctor L W ε).map (((tensorBifunctor L W ε).obj Y₁).map f₂)).app X₃) ≫
      ((tensorBifunctor L W ε).obj (((tensorBifunctor L W ε).obj Y₁).obj Y₂)).map f₃ ≫
        (((associator L W ε).hom.app Y₁).app Y₂).app Y₃ =
    (((associator L W ε).hom.app X₁).app X₂).app X₃ ≫
      ((tensorBifunctor L W ε).map f₁).app (((tensorBifunctor L W ε).obj X₂).obj X₃) ≫
        ((tensorBifunctor L W ε).obj Y₁).map (((tensorBifunctor L W ε).map f₂).app X₃) ≫
          ((tensorBifunctor L W ε).obj Y₁).map (((tensorBifunctor L W ε).obj Y₂).map f₃)

Tactic:
rw [h₁, assoc, reassoc_of% h₂, reassoc_of% h₃]

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

Goal state before:
pp: case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F = prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F

Tactic:
(rw [← Category.assoc]; congr 1; simp)

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

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F = prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F

Tactic:
(rw [← Category.assoc]; congr 1; simp)

Goal state after: