mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
⊢ IsColimit { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }

Tactic:
by
  suffices IsIso (colimMap (pullback.snd c.ι ((Functor.const J).map f))) from
    Cocone.isColimitOfIsIsoColimMapι _
  have hpull := colim.map_isPullback (IsPullback.of_hasPullback c.ι ((Functor.const J).map f))
  dsimp only [colim_obj, colim_map] at hpull
  have := hc.isIso_colimMap_ι
  apply hpull.isIso_snd_of_isIso

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
this : HasDerivedCategory C
x y : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x + CohomologyClass.mk y)).hom =
    (R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm (CohomologyClass.mk y)).hom

Tactic:
simp [← CohomologyClass.mk_add, extEquivCohomologyClass_symm_mk_hom, ShiftedHom.map]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫ d (Injective.ι Z) = 0

Tactic:
cokernel.condition_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ 0 ≫ Injective.ι (cokernel (Injective.ι Z)) = 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
a b : Over P
x✝ : a ≈ b
R : C
p : R ⟶ a.left
q : R ⟶ b.left
ep : Epi p
Eq : Epi q
comm : p ≫ a.hom = q ≫ b.hom
⊢ p ≫ a.hom ≫ f = q ≫ b.hom ≫ f

Tactic:
reassoc_of% comm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
a b : Over P
x✝ : a ≈ b
R : C
p : R ⟶ a.left
q : R ⟶ b.left
ep : Epi p
Eq : Epi q
comm : p ≫ a.hom = q ≫ b.hom
⊢ q ≫ b.hom ≫ f = q ≫ b.hom ≫ f
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
this : HasDerivedCategory C
x y : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x + CohomologyClass.mk y)).hom =
    (R.extEquivCohomologyClass.symm (CohomologyClass.mk x) + R.extEquivCohomologyClass.symm (CohomologyClass.mk y)).hom

Tactic:
simp [← CohomologyClass.mk_add, extEquivCohomologyClass_symm_mk_hom, ShiftedHom.map]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n

Tactic:
(HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ ((CochainComplex.single₀ C).map f ≫ Q.ι).f 0 = f ≫ Q.ι.f 0

Tactic:
HomologicalComplex.comp_f,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ ((CochainComplex.single₀ C).map f).f 0 ≫ Q.ι.f 0 = f ≫ Q.ι.f 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
inst✝⁴ : L.IsLocalization P.isoModSerre
inst✝³ : Preadditive D
inst✝² : L.Additive
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
⊢ L.map (f ≫ g) = 0 ↔ P Z

Tactic:
map_eq_zero_iff L P

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
inst✝⁴ : L.IsLocalization P.isoModSerre
inst✝³ : Preadditive D
inst✝² : L.Additive
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst✝¹ : Epi f
inst✝ : Mono g
⊢ P (Abelian.image (f ≫ g)) ↔ P Z
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
this : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s
⊢ L.map f ≫ z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = 0

Tactic:
reassoc_of% hz,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
this : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s
⊢ 0 ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = 0
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing (G.obj ᘁ(F.obj X)) X

Tactic:
by
    letI := exactPairingCongrLeft (X := F.obj (G.obj ᘁ(F.obj X)))
      (X' := ᘁ(F.obj X)) (Y := F.obj X) (adj.toEquivalence.counitIso.app ᘁ(F.obj X))
    apply ExactPairing.ofFullyFaithful F

Goal state after:
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
X : B
⊢ F'.map (𝟙 (U.obj X)) = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))

Tactic:
apply F'.map_id

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝⁵ : L.Full
inst✝⁴ : L.Faithful
inst✝³ : G.Full
inst✝² : G.Faithful
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts D
⊢ (∀ (k : C), Epi (q.leftTriple.leftToRight.app k)) ↔ ∀ (k : D), Mono (q.rightTriple.rightToLeft.app k)

Tactic:
exact q.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.whiskerLeft t.leftToRight = t.adj₁.counit ≫ t.adj₂.unit

Tactic:
by
  ext X; exact t.leftToRight_app_obj

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
⊢ Quot.map (Hom₂.whisker_left (𝟙 a)) ⋯ (Quot.mk Rel η) =
    { hom := Quot.mk Rel (Hom₂.left_unitor f), inv := Quot.mk Rel (Hom₂.left_unitor_inv f), hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      Quot.mk Rel η ≫
        { hom := Quot.mk Rel (Hom₂.left_unitor g), inv := Quot.mk Rel (Hom₂.left_unitor_inv g), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.inv

Tactic:
exact Quot.sound (Rel.id_whisker_left η)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    Quot.map (Hom₂.whisker_right h) ⋯ (Quot.map (Hom₂.whisker_left f) ⋯ η) =
      { hom := Quot.mk Rel (Hom₂.associator f g h), inv := Quot.mk Rel (Hom₂.associator_inv f g h), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        Quot.map (Hom₂.whisker_left f) ⋯ (Quot.map (Hom₂.whisker_right h) ⋯ η) ≫
          { hom := Quot.mk Rel (Hom₂.associator f g' h), inv := Quot.mk Rel (Hom₂.associator_inv f g' h),
              hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv

Tactic:
by
    rintro a b c d f g g' ⟨η⟩ h
    exact Quot.sound (Rel.whisker_assoc f η h)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a ⟶ b
g : G.obj b ⟶ a'
⊢ Γ.app a ▷ G.map f ▷ g ≫ θ.naturality f ▷ g = η.naturality f ▷ g ≫ (F.map f ◁ Γ.app b) ▷ g

Tactic:
simp_rw [← comp_whiskerRight, naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv

Tactic:
θ.naturality_id

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ (ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

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
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)

Tactic:
Γ.as.naturality

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
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map f ◁ Γ.as.app b) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

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
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)

Tactic:
Γ.as.naturality

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
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map f ◁ Γ.as.app b) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

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
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫ θ.naturality f) ▷ ι.app b) ⊗≫
        𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    ((α_ (η.app a) (ι.app a) (H.map f)).hom ≫
        η.app a ◁ ι.naturality f ≫
          (α_ (η.app a) (G.map f) (ι.app b)).inv ≫ η.naturality f ▷ ι.app b ≫ (α_ (F.map f) (η.app b) (ι.app b)).hom) ≫
      F.map f ◁ Γ.as.app b ▷ ι.app b

Tactic:
Γ.as.naturality

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
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ⊗≫ (η.naturality f ≫ F.map f ◁ Γ.as.app b) ▷ ι.app b) ⊗≫
        𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    ((α_ (η.app a) (ι.app a) (H.map f)).hom ≫
        η.app a ◁ ι.naturality f ≫
          (α_ (η.app a) (G.map f) (ι.app b)).inv ≫ η.naturality f ▷ ι.app b ≫ (α_ (F.map f) (η.app b) (ι.app b)).hom) ≫
      F.map f ◁ Γ.as.app b ▷ ι.app b
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫
                η.naturality f ▷ ι.app b ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality f ⊗≫ ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫
              η.naturality f ▷ ι.app b) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [whisker_exchange]
          bicategory

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

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
⊢ Γ.as.app a ▷ ι.app a ▷ H.map f ≫ (θ ≫ ι).naturality f = (η ≫ ι).naturality f ≫ F.map f ◁ Γ.as.app b ▷ ι.app b

Tactic:
dsimp only [comp_app, comp_naturality]
      calc
        _ = 𝟙 _ ⊗≫ (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
              θ.naturality f ▷ ι.app b ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ (η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫
              θ.naturality f) ▷ ι.app b) ⊗≫ 𝟙 _ := by
          rw [← whisker_exchange]
          bicategory
        _ = _ := by
          rw [Γ.as.naturality]
          bicategory

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

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
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫ θ.naturality f) ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    ((α_ (η.app a) (ι.app a) (H.map f)).hom ≫
        η.app a ◁ ι.naturality f ≫
          (α_ (η.app a) (G.map f) (ι.app b)).inv ≫ η.naturality f ▷ ι.app b ≫ (α_ (F.map f) (η.app b) (ι.app b)).hom) ≫
      F.map f ◁ Γ.as.app b ▷ ι.app b

Tactic:
Γ.as.naturality

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
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      η.app a ◁ ι.naturality f ⊗≫ (η.naturality f ≫ F.map f ◁ Γ.as.app b) ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    ((α_ (η.app a) (ι.app a) (H.map f)).hom ≫
        η.app a ◁ ι.naturality f ≫
          (α_ (η.app a) (G.map f) (ι.app b)).inv ≫ η.naturality f ▷ ι.app b ≫ (α_ (F.map f) (η.app b) (ι.app b)).hom) ≫
      F.map f ◁ Γ.as.app b ▷ ι.app b
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a

Tactic:
θ.naturality_id

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ ((λ_ (θ.app a)).hom ≫ (ρ_ (θ.app a)).inv ≫ θ.app a ◁ H.mapId a) ⊗≫
        𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

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 ≫ η.app b ≫ θ.app b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫
        η.app a ◁ (G.map f ◁ Γ.as.app b ≫ ι.naturality f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        η.naturality f ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
Γ.as.naturality

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 ≫ η.app b ≫ θ.app b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫
        η.app a ◁ (θ.naturality f ≫ Γ.as.app a ▷ H.map f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        η.naturality f ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

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 ≫ η.app b ≫ ι.app b) ⊗≫
      (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
        θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)

Tactic:
Γ.as.naturality

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 ≫ η.app b ≫ ι.app b) ⊗≫
      (η.naturality f ≫ Γ.as.app a ▷ G.map f) ▷ ι.app b ⊗≫
        θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
        F.mapId { as := { as := () } } ▷ F.map (𝟙 { as := { as := () } }) =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
rw [F.mapComp_id_left, unitors_equal, F.map₂_inv_hom_assoc]

Goal state after:
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
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
F.mapComp_id_left_hom f,

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} D₁
inst✝⁴ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
this : (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)
⊢ (L₁.prod L₂).IsLocalization (W₁.prod W₂)

Tactic:
exact of_equivalence_target (W₁.Q.prod W₂.Q) (W₁.prod W₂) (L₁.prod L₂)
    ((uniq W₁.Q L₁ W₁).prod (uniq W₂.Q L₂ W₂))
    (NatIso.prod (compUniqFunctor W₁.Q L₁ W₁) (compUniqFunctor W₂.Q L₂ W₂))

Goal state after: