mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
this : IsIso (L.map w)
⊢ IsIso (e.hom.app X₁ ≫ G.map (L.map w) ≫ e.inv.app X₂)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst✝¹ : HasLimit G
inst✝ : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
e : ((F i).mapCone c).pt ≅ ((F i).mapCone (limit.cone G)).pt := (hc i).conePointUniqueUpToIso H
this : e.hom = (F i).map (limit.lift G c)
⊢ IsIso e.hom

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst✝¹ : HasColimit G
inst✝ : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
e : ((F i).mapCocone (colimit.cocone G)).pt ≅ ((F i).mapCocone c).pt := H.coconePointUniqueUpToIso (hc i)
this : e.hom = (F i).map (colimit.desc G c)
⊢ IsIso e.hom

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
F : C ⥤ H
LF : D ⥤ H
α : L ⋙ LF ⟶ F
hF : W.IsInvertedBy F
inst✝ : LF.IsLeftDerivedFunctor α W
this :
  α =
    L.whiskerLeft (LF.leftDerivedUnique (Localization.lift F hF L) (Localization.fac F hF L).hom α W).inv ≫
      (Localization.fac F hF L).hom
⊢ IsIso
    (L.whiskerLeft (LF.leftDerivedUnique (Localization.lift F hF L) (Localization.fac F hF L).hom α W).inv ≫
      (Localization.fac F hF L).hom)

Tactic:
infer_instance

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

Goal state before:
pp: J : Type
inst✝ : SmallCategory J
K : J ⥤ FintypeCat
j : J
⊢ Finite (K.obj j).obj

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this : IsIso (equalizer.ι (F.map f) (F.map g))
⊢ IsIso (F.map (equalizer.ι f g))

Tactic:
← equalizerComparison_comp_π f g F

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this : IsIso (equalizer.ι (F.map f) (F.map g))
⊢ IsIso (equalizerComparison f g F ≫ equalizer.ι (F.map f) (F.map g))
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
⊢ IsGalois X

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∀ (y : Aut B),
    (fun τ ↦ f ≫ τ.hom = σ.hom ≫ f) y →
      y =
        (evaluationEquivOfIsGalois F B ((ConcreteCategory.hom (F.map f)) a)).symm
          ((ConcreteCategory.hom (F.map (σ.hom ≫ f))) a)

Tactic:
· intro τ hτ
    apply evaluation_aut_injective_of_isConnected F B (F.map f a)
    simpa using ConcreteCategory.congr_hom (F.congr_map hτ) a

Goal state after:
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
⊢ Function.Surjective (autMap f)

Tactic:
by
  intro σ
  let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  obtain ⟨a', ha'⟩ := surjective_of_nonempty_fiber_of_isConnected F f (F.map σ.hom (F.map f a))
  obtain ⟨τ, (hτ : F.map τ.hom a = a')⟩ := MulAction.exists_smul_eq (Aut A) a a'
  use τ
  apply evaluation_aut_injective_of_isConnected F B (F.map f a)
  simp [hτ, ha']

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso (𝟙 ((functorToAction F).obj X))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this✝ : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this : IsIso ((functorToAction F).map ψ)
⊢ ∃ a, (functorToAction F).map a = f

Tactic:
have : IsIso ψ := isIso_of_reflects_iso ψ (functorToAction F)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this✝¹ : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this✝ : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
⊢ ∃ a, (functorToAction F).map a = f
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝² : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝¹ : IsGalois B
u : A ⟶ X
v : B ⟶ X
h : (ConcreteCategory.hom (F.map u)) a = (ConcreteCategory.hom (F.map v)) b
Z : C
z : (F.obj Z).obj
isGalois✝ : IsGalois Z
f :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj
hf :
  (ConcreteCategory.hom (F.map f)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).pt
h✝ : True
g :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).obj
hg :
  (ConcreteCategory.hom (F.map g)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).pt
⊢ ∃ k f g,
    (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) u =
      (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) v

Tactic:
refine ⟨⟨{ obj := Z, pt := z }⟩, ⟨f, hf⟩, ⟨g, hg⟩, ?_⟩

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝² : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝¹ : IsGalois B
u : A ⟶ X
v : B ⟶ X
h : (ConcreteCategory.hom (F.map u)) a = (ConcreteCategory.hom (F.map v)) b
Z : C
z : (F.obj Z).obj
isGalois✝ : IsGalois Z
f :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj
hf :
  (ConcreteCategory.hom (F.map f)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).pt
h✝ : True
g :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).obj
hg :
  (ConcreteCategory.hom (F.map g)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).pt
⊢ (ConcreteCategory.hom
        ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map (Opposite.op { val := f, comp := hf })))
      u =
    (ConcreteCategory.hom
        ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map (Opposite.op { val := g, comp := hg })))
      v
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
m : SingleObj.star (↥V ⧸ (↑U).subgroupOf ↑V) ⟶ SingleObj.star (↥V ⧸ (↑U).subgroupOf ↑V)
⊢ (functorToAction F).map ((quotientToEndObjectHom V h u) m) = u.hom ≫ (quotientToEndHom ↑V ↑U) m ≫ u.inv

Tactic:
simp [← cancel_epi u.inv, ← cancel_mono u.hom, ← Iso.conj_apply, quotientToEndObjectHom]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ ⋂ S ∈ s, S.arrows c✝ d✝
x✝ : d✝ ⟶ e✝
hq : x✝ ∈ ⋂ S ∈ s, S.arrows d✝ e✝
⊢ p✝ ≫ x✝ ∈ ⋂ S ∈ s, S.arrows c✝ e✝

Tactic:
rw [mem_iInter₂] at hp hq ⊢

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
hp : ∀ i ∈ s, p✝ ∈ i.arrows c✝ d✝
x✝ : d✝ ⟶ e✝
hq : ∀ i ∈ s, x✝ ∈ i.arrows d✝ e✝
⊢ ∀ i ∈ s, p✝ ≫ x✝ ∈ i.arrows c✝ e✝
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
    whiskerLeft X (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i k ⋯) k ≫
      (associator X Z Y).inv k ≫
        whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) Y k

Tactic:
rw [ιTensorObj₃_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc, ι_tensorHom_assoc,
    ← MonoidalCategory.id_tensorHom,
    MonoidalCategory.tensorHom_comp_tensorHom_assoc, id_comp, ι_tensorObjDesc,
    categoryOfGradedObjects_id, MonoidalCategory.id_tensor_comp, assoc,
    MonoidalCategory.id_tensorHom, MonoidalCategory.id_tensorHom,
    ← ιTensorObj₃_eq_assoc X Z Y i₁ i₃ i₂ k
      (by rw [add_assoc, add_comm i₃, ← add_assoc, h]) (i₂ + i₃) (add_comm _ _),
    ιTensorObj₃_associator_inv_assoc,
    ιTensorObj₃'_eq X Z Y i₁ i₃ i₂ k (by rw [add_assoc, add_comm i₃, ← add_assoc, h]) _ rfl,
    assoc, ι_tensorHom, categoryOfGradedObjects_id, ← MonoidalCategory.tensorHom_id,
    ← MonoidalCategory.comp_tensor_id_assoc,
    ι_tensorObjDesc, MonoidalCategory.comp_tensor_id, assoc,
    MonoidalCategory.tensorHom_id, MonoidalCategory.tensorHom_id,
    ← ιTensorObj₃'_eq Z X Y i₃ i₁ i₂ k (by rw [add_assoc, add_comm i₃, h])
      (i₁ + i₃) (add_comm _ _)]

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.whiskerLeft (X i₁) (β_ (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Z i₃) (Y i₂)).inv ≫
      MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Z i₃)).hom (Y i₂) ≫ ιTensorObj₃' Z X Y i₃ i₁ i₂ k ⋯
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : HasPullbacks C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom (t.from X) ↔ HasLiftingProperty g ((MonoidalClosed.pre f).app X)

Tactic:
by
  rw [hasLiftingProperty_mk_iff]
  exact HasLiftingProperty.iff_of_arrow_iso_right g (PullbackHom.isTerminalIso _ t)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f✝ : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f✝ i = (F.obj (op j)).map g ≫ f✝ j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
⊢ (F.map φ.op).app j ≫ (f.app (op j)).app j ≫ ι G j = (F.obj (op j')).map φ ≫ (f.app (op j')).app j' ≫ ι G j'

Tactic:
simp [chosenCoend.condition]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x y z : C ⋆ D
f : x ⟶ y
g : y ⟶ z
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (f ≫ g) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) f ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) g

Tactic:
by
    cases f <;> cases g
    · simp [← Functor.map_comp]
    · case left.edge f d => simpa using! (α.naturality <| (Prod.sectL _ d).map f).symm
    · simp [← Functor.map_comp]
    · case edge.right c _ _ f => simpa using! α.naturality <| (Prod.sectR c _).map f

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (left c) = 𝟙 (left (Gₗ.obj (Fₗ.obj c)))

Tactic:
dsimp [mapPairComp]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ 𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫
      𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫
        𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫ 𝟙 (left (Gₗ.obj (Fₗ.obj c))) ≫ (mapPair Gₗ Gᵣ).map (𝟙 (left (Fₗ.obj c))) =
    𝟙 (left (Gₗ.obj (Fₗ.obj c)))
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (right d) = 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))

Tactic:
dsimp [mapPairComp]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫
      𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫
        𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫ 𝟙 (right (Gᵣ.obj (Fᵣ.obj d))) ≫ (mapPair Gₗ Gᵣ).map (𝟙 (right (Fᵣ.obj d))) =
    𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (left c) = 𝟙 (left (Gₗ.obj (Fₗ.obj c)))

Tactic:
dsimp [mapPairComp]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ (mkNatTrans
          ((((whiskerRight (mapPairLeft Fₗ Fᵣ).hom (mapPair Gₗ Gᵣ) ≫
                  (Fₗ.associator (inclLeft E E') (mapPair Gₗ Gᵣ)).hom) ≫
                Fₗ.whiskerLeft (mapPairLeft Gₗ Gᵣ).hom) ≫
              (Fₗ.associator Gₗ (inclLeft J K)).inv) ≫
            (mapPairLeft (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).inv)
          ((((whiskerRight (mapPairRight Fₗ Fᵣ).hom (mapPair Gₗ Gᵣ) ≫
                  (Fᵣ.associator (inclRight E E') (mapPair Gₗ Gᵣ)).hom) ≫
                Fᵣ.whiskerLeft (mapPairRight Gₗ Gᵣ).hom) ≫
              (Fᵣ.associator Gᵣ (inclRight J K)).inv) ≫
            (mapPairRight (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).inv)
          ⋯).app
      (left c) =
    𝟙 (left (Gₗ.obj (Fₗ.obj c)))
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (right d) = 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))

Tactic:
dsimp [mapPairComp]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ (mkNatTrans
          ((((whiskerRight (mapPairLeft Fₗ Fᵣ).hom (mapPair Gₗ Gᵣ) ≫
                  (Fₗ.associator (inclLeft E E') (mapPair Gₗ Gᵣ)).hom) ≫
                Fₗ.whiskerLeft (mapPairLeft Gₗ Gᵣ).hom) ≫
              (Fₗ.associator Gₗ (inclLeft J K)).inv) ≫
            (mapPairLeft (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).inv)
          ((((whiskerRight (mapPairRight Fₗ Fᵣ).hom (mapPair Gₗ Gᵣ) ≫
                  (Fᵣ.associator (inclRight E E') (mapPair Gₗ Gᵣ)).hom) ≫
                Fᵣ.whiskerLeft (mapPairRight Gₗ Gᵣ).hom) ≫
              (Fᵣ.associator Gᵣ (inclRight J K)).inv) ≫
            (mapPairRight (Fₗ ⋙ Gₗ) (Fᵣ ⋙ Gᵣ)).inv)
          ⋯).app
      (right d) =
    𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inl ≫ (binaryCoproductIso F G).hom = coprod.inl

Tactic:
by
  simp only [binaryCoproductIso]
  aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂ ≫ f₂ = h.p

Tactic:
rw [← p₂₃_p₂_assoc, h₂₃.condition, ← w₃, p₂₃_p₃_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout b.inl 0 b.snd 0

Tactic:
apply flip
  refine of_left ?_ (by simp) (of_isBilimit h)
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case inst.isTrue
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
h✝ : ↑⟨val✝, property✝⟩ < n
⊢ Epi (eqToHom ⋯)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case inst.isFalse
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : val✝ < n + 1
h✝ : ¬↑⟨val✝, property✝⟩ < n
⊢ Epi (eqToHom ⋯ ≫ f ↑⟨val✝, property✝⟩ ≫ eqToHom ⋯)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case inst.isTrue
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n val✝ : ℕ
property✝ : ¬val✝ < n + 1
h✝ : ↑⟨val✝, property✝⟩ < n
⊢ IsIso (eqToHom ⋯)

Tactic:
infer_instance

Goal state after: