mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_2
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
Q : CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right) = L.map va₂ ≫ j₁.hom
⊢ ∃ W h, h ≫ u = h ≫ v

Tactic:
obtain ⟨i₀, α, β, hα, hβ⟩ := IsCofiltered.bowtie u.left (va₂ ≫ v.left) (𝟙 _) va₂

Goal state after:
case refine_2
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
Q : CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right) = L.map va₂ ≫ j₁.hom
i₀ : A
α : i₀ ⟶ j₁.left
β : i₀ ⟶ ia
hα : α ≫ u.left = β ≫ va₂ ≫ v.left
hβ : α ≫ 𝟙 j₁.left = β ≫ va₂
⊢ ∃ W h, h ≫ u = h ≫ v
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms

Tactic:
by
  rw [injective_iff_preservesEpimorphisms_yoneda_obj]
  refine
    ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrpCat)).PreservesEpimorphisms => ?_, ?_⟩
  · exact
      Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)
  · intro
    exact (inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex)

Tactic:
by
  apply descHomotopy (𝟙 X) <;> simp

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 : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extMk f m hm hf - R.extMk g m hm hg = R.extMk (f - g) m hm ⋯

Tactic:
dsimp [extMk]
  simp only [Preadditive.sub_comp]
  rw [Cocycle.fromSingleMk_sub _ _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hg])]
  simp

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

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✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization G.kernel.isoModSerre

Tactic:
isoModSerre_kernel_eq_inverseImage_isomorphisms G

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
inst✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization ((isomorphisms C).inverseImage G)
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 G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
⊢ (NatTrans.rightDerivedToHomotopyCategory α).app X =
    (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (P.isoRightDerivedToHomotopyCategoryObj G).inv

Tactic:
rw [← cancel_mono (P.isoRightDerivedToHomotopyCategoryObj G).hom, assoc, assoc,
      Iso.inv_hom_id, comp_id]
  dsimp [isoRightDerivedToHomotopyCategoryObj, Functor.mapHomotopyCategoryFactors,
    NatTrans.rightDerivedToHomotopyCategory]
  rw [assoc]
  erw [id_comp, comp_id]
  obtain ⟨β, hβ⟩ := (HomotopyCategory.quotient _ _).map_surjective (iso P).hom
  rw [← hβ]
  dsimp
  simp only [← Functor.map_comp, NatTrans.mapHomologicalComplex_naturality]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
X✝ Y✝ Z✝ : SingleObj M
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (↾fun x ↦ f ≫ g • x) = (↾fun x ↦ f • x) ≫ ↾fun x ↦ g • x

Tactic:
ext x

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
X✝ Y✝ Z✝ : SingleObj M
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : X
⊢ (ConcreteCategory.hom (↾fun x ↦ f ≫ g • x)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ f • x) ≫ ↾fun x ↦ g • x)).toFun x
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (F g).right = g
X✝ Y✝ Z✝ : ActionCategory G X
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (F ↑(f ≫ g)).left Z✝.back = (F ↑f).left Y✝.back ≫ (F ↑g).left Z✝.back

Tactic:
by
    cases g using ActionCategory.cases
    simp [SingleObj.comp_as_mul, sane]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
g : G
⊢ (s.pt.ρ g ≫ ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x) =
    (↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x) ≫
      { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt.ρ
        g

Tactic:
ext x

Goal state after:
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
g : G
x : s.pt.V
⊢ (ConcreteCategory.hom (s.pt.ρ g ≫ ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x)).toFun x =
    (ConcreteCategory.hom
          ((↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x) ≫
            { pt := ofMulAction G ((i : ι) → F i),
                    π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt.ρ
              g)).toFun
      x
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h :
  ∀ (j : Discrete ι),
    f ≫
        { pt := ofMulAction G ((i : ι) → F i),
                π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.π.app
          j =
      s.π.app j
⊢ f = { hom := ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x, comm := ⋯ }

Tactic:
ext x

Goal state after:
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h :
  ∀ (j : Discrete ι),
    f ≫
        { pt := ofMulAction G ((i : ι) → F i),
                π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.π.app
          j =
      s.π.app j
x : s.pt.V
⊢ (ConcreteCategory.hom f.hom).toFun x =
    (ConcreteCategory.hom { hom := ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x, comm := ⋯ }.hom).toFun
      x
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 : D
f : X ⟶ Y
⊢ Mono f ↔ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
have := preservesMonomorphisms L P
  have := Localization.essSurj_mapArrow L P.isoModSerre
  refine ⟨fun _ ↦ ?_, ?_⟩
  · suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Mono (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Mono f'),
          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
        let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
        obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.monomorphisms D).arrow_iso_iff e).2 (.infer_property f))
        exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩
    intro X Y f hf
    rw [mono_map_iff L P] at hf
    refine ⟨_, _, Abelian.image.ι f, inferInstance, ⟨Iso.symm ?_⟩⟩
    have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_factorThruImage
    exact Arrow.isoMk (asIso (L.map (Abelian.factorThruImage f))) (Iso.refl _)
      (by simp [← L.map_comp])
  · rintro ⟨X', Y', f', _, ⟨e⟩⟩
    exact ((MorphismProperty.monomorphisms D).arrow_mk_iso_iff e).1
      (by simpa using inferInstanceAs (Mono (L.map f')))

Goal state after:
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ { hom := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.hom, ⋯⟩, comm := ⋯ } = x✝

Tactic:
ext; simp [ConcreteCategory.ofHom_hom]

Goal state after:
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✝ : D
f : X✝ ⟶ Y✝
g : Arrow C
e : L.mapArrow.obj g ≅ Arrow.mk f
⊢ HasKernel f

Tactic:
have := preservesKernel L P g.hom

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✝ : D
f : X✝ ⟶ Y✝
g : Arrow C
e : L.mapArrow.obj g ≅ Arrow.mk f
this : PreservesLimit (parallelPair g.hom 0) L
⊢ HasKernel f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ exactFunctor D E (Localization.lift F.obj hF L)

Tactic:
rw [← exactFunctor_comp_iff L P]

Goal state after:
case refine_2
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ exactFunctor C E (L ⋙ Localization.lift F.obj hF L)
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℕ
g : G
f : Fin n → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f

Tactic:
induction n generalizing g with

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
⊢ (fun f ↦ { app := fun x ↦ Sigma.desc fun h ↦ f ≫ F.map h, naturality := ⋯ })
      ((fun f ↦ Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c) f) =
    f

Tactic:
ext x

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : (evaluationLeftAdjoint D c).obj d ⟶ F
x : C
⊢ ((fun f ↦ { app := fun x ↦ Sigma.desc fun h ↦ f ≫ F.map h, naturality := ⋯ })
          ((fun f ↦ Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c) f)).app
      x =
    f.app x
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η ↔ ∀ (c : C), Mono (η.app c)

Tactic:
by
  constructor
  · intro h c
    exact (inferInstance : Mono (((evaluation _ _).obj c).map η))
  · intro _
    apply NatTrans.mono_of_mono_app

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
⊢ (fun f ↦ { app := fun x ↦ Pi.lift fun g ↦ F.map g ≫ f, naturality := ⋯ })
      ((fun f ↦ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c)) f) =
    f

Tactic:
ext x

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : F ⟶ (evaluationRightAdjoint D c).obj d
x : C
⊢ ((fun f ↦ { app := fun x ↦ Pi.lift fun g ↦ F.map g ≫ f, naturality := ⋯ })
          ((fun f ↦ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c)) f)).app
      x =
    f.app x
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f ≫ g = f' ≫ g

Tactic:
by rw [h]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f' ≫ g' = f ≫ g'

Tactic:
by rw [h]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f ≫ g = f ≫ g'

Tactic:
by rw [h]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f' ≫ g' = f' ≫ g

Tactic:
by rw [h]

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : X ⟶ Y),
    (𝟭 (a ⟶ b)).map f ≫ ((λ_ Y).symm ≪≫ normalizeIso nil Y).hom =
      ((λ_ X).symm ≪≫ normalizeIso nil X).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map f

Tactic:
intro f g η
      erw [leftUnitor_inv_naturality_assoc, assoc]
      congr 1
      exact normalize_naturality nil η

Goal state after:
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) =
    StructuredArrow.hom (t.whisker h)

Tactic:
rw [← cancel_mono (α_ h _ _).hom]
    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.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 : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β

Tactic:
by
      rw [θ.naturality_naturality]
      bicategory

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

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫
          η.app a ◁ θ.naturality g ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫
          η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 _ := by
      rw [η.naturality_naturality]
      bicategory
    _ = _ := by
      rw [θ.naturality_naturality]
      bicategory

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
hfg : f = g
⊢ ∃ (hfg : f.base = g.base), eqToHom ⋯ ≫ f.fiber = g.fiber

Tactic:
subst hfg

Goal state after:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ ∃ (hfg : f.base = f.base), eqToHom ⋯ ≫ f.fiber = f.fiber
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
⊢ { iso := (EquivFunctor.mapEquiv m (𝟙 α).iso.toEquiv).toIso } = 𝟙 { of := m α.of }

Tactic:
ext x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
x : { of := m α.of }.of
⊢ (ConcreteCategory.hom { iso := (EquivFunctor.mapEquiv m (𝟙 α).iso.toEquiv).toIso }.iso.hom).toFun x =
    (ConcreteCategory.hom (𝟙 { of := m α.of }).iso.hom).toFun x
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
⊢ StructuredArrow.Hom.right τ₀ =
    StructuredArrow.Hom.right (homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯)

Tactic:
have hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit := by
      simpa [bicategoricalComp] using LeftExtension.w τ₀

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ StructuredArrow.Hom.right τ₀ =
    StructuredArrow.Hom.right (homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ τ = 𝟙 (u ≫ h) ⊗≫ rightZigzag adj.unit adj.counit ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension

Tactic:
rw [adj.right_triangle]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ τ = 𝟙 (u ≫ h) ⊗≫ ((ρ_ u).hom ≫ (λ_ u).inv) ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u) = s.unit

Tactic:
rw [adj.right_triangle]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ s.unit ⊗≫ s.lift ◁ ((ρ_ u).hom ≫ (λ_ u).inv) ⊗≫ 𝟙 (s.lift ≫ u) = s.unit
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝ : Cat
⊢ ↾(𝟙 x✝).toFunctor.mapConnectedComponents = 𝟙 (ConnectedComponents ↑x✝)

Tactic:
ext x

Goal state after:
X : Type u
C : Cat
x✝ : Cat
x : ConnectedComponents ↑x✝
⊢ (ConcreteCategory.hom (↾(𝟙 x✝).toFunctor.mapConnectedComponents)).toFun x =
    (ConcreteCategory.hom (𝟙 (ConnectedComponents ↑x✝))).toFun x
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
X✝ Y✝ Z✝ : Cat
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾(x✝¹ ≫ x✝).toFunctor.mapConnectedComponents =
    ↾x✝¹.toFunctor.mapConnectedComponents ≫ ↾x✝.toFunctor.mapConnectedComponents

Tactic:
ext x

Goal state after:
X : Type u
C : Cat
X✝ Y✝ Z✝ : Cat
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
x : ConnectedComponents ↑X✝
⊢ (ConcreteCategory.hom (↾(x✝¹ ≫ x✝).toFunctor.mapConnectedComponents)).toFun x =
    (ConcreteCategory.hom (↾x✝¹.toFunctor.mapConnectedComponents ≫ ↾x✝.toFunctor.mapConnectedComponents)).toFun x
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X✝ Y✝ : Type u_1
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : typeToPartialFun.map a₁✝ = typeToPartialFun.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext x

Goal state after:
X✝ Y✝ : Type u_1
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : typeToPartialFun.map a₁✝ = typeToPartialFun.map a₂✝
x : X✝
⊢ (ConcreteCategory.hom a₁✝).toFun x = (ConcreteCategory.hom a₂✝).toFun x
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (res f s).core t = sᶜ ∪ f ⁻¹' t

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
rw [mem_core_res]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f).core s = f ⁻¹' s

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x : α
⊢ x ∈ (↑f).core s ↔ x ∈ f ⁻¹' s
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : ↑f.Dom
⊢ x ∈ f.asSubtype ⁻¹' s ↔ x ∈ Subtype.val ⁻¹' f.preimage s
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h.left
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ↾f ≫ ↾g = 𝟙 X

Tactic:
ext x

Goal state after:
case h.left
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
x : X
⊢ (ConcreteCategory.hom (↾f ≫ ↾g)).toFun x = (ConcreteCategory.hom (𝟙 X)).toFun x