mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ IsIso ((F i).map (colimit.desc G c))

Tactic:
have : e.hom = (F i).map (colimit.desc G c) :=
    H.hom_ext (fun j ↦ by
      simpa [← Functor.map_comp] using
        IsColimit.comp_coconePointUniqueUpToIso_hom H (hc i) j)

Goal state after:
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 ((F i).map (colimit.desc G c))
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: G : Type v
inst✝¹ : Group G
inst✝ : Finite G
⊢ PreservesColimitsOfShape (SingleObj G) FintypeCat.incl

Tactic:
choose G' hg hf e using Finite.exists_type_univ_nonempty_mulEquiv G

Goal state after:
G : Type v
inst✝¹ : Group G
inst✝ : Finite G
G' : Type ?u.14
hg : Group G'
hf : Fintype G'
e : Nonempty (G ≃* G')
⊢ PreservesColimitsOfShape (SingleObj G) FintypeCat.incl
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
⊢ Nat.card (F.obj (Y ⨿ Z)).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj

Tactic:
exact card_fiber_coprod_eq_sum F Y Z

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b

Tactic:
by
  /- We consider the fiber product of A and B over X. This is a non-empty (because of `h`)
  subobject of `A` and `B` and hence isomorphic to `A` and `B` by connectedness. -/
  let Y : C := pullback i j
  let u : Y ⟶ A := pullback.fst i j
  let v : Y ⟶ B := pullback.snd i j
  let G := F ⋙ FintypeCat.incl
  let e : F.obj Y ≃ { p : F.obj A × F.obj B // F.map i p.1 = F.map j p.2 } :=
    fiberPullbackEquiv F i j
  let y : F.obj Y := e.symm ⟨(a, b), h⟩
  have hn : IsInitial Y → False := not_initial_of_inhabited F y
  have : IsIso u := IsConnected.noTrivialComponent Y u hn
  have : IsIso v := IsConnected.noTrivialComponent Y v hn
  use (asIso u).symm ≪≫ asIso v
  have hu : G.map u y = a := fiberPullbackEquiv_symm_fst_apply _ _ _ h
  have hv : G.map v y = b := fiberPullbackEquiv_symm_snd_apply _ _ _ h
  rw [← hu, ← hv]
  change (F.map u ≫ F.map _) y = F.map v y
  simp only [← F.map_comp, Iso.trans_hom, Iso.symm_hom, asIso_inv, asIso_hom,
    IsIso.hom_inv_id_assoc]

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
⊢ (functorToAction F).map g = v.inv ≫ i

Tactic:
simp [← hvgi]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
t : Aut F
⊢ (fun t ↦ asIso ((endMulEquivAutGalois F).symm t)) (((↑(endMulEquivAutGalois F)).comp (Aut.toEnd F)) t) = t

Tactic:
by
    simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
      MulEquiv.symm_apply_apply]
    exact Aut.ext rfl

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

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
x y : (F.obj X).obj
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨(φ : Aut X), h⟩ := MulAction.IsPretransitive.exists_smul_eq (M := Aut X) x y

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).obj
φ : Aut X
h : φ • x = y
⊢ ∃ g, g • x = y
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).obj
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
⊢ ContinuousAt (⇑(toAut F G)) 1

Tactic:
rw [continuousAt_def, map_one]

Goal state after:
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).obj
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
⊢ ∀ A ∈ nhds 1, ⇑(toAut F G) ⁻¹' A ∈ nhds 1
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
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
σ τ : Aut F
hst : σ ≈ τ
J' : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V) ⥤ Action FintypeCat (Aut F) := quotientDiag V h u ⋙ functorToAction F
m : End (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V)) := ⟦⟨σ⁻¹ * τ, ⋯⟩⟧
⊢ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧ =
    (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦τ⟧

Tactic:
have h1 : J'.map m ≫ s.ι.app (SingleObj.star _) = s.ι.app (SingleObj.star _) :=
        s.ι.naturality m

Goal state after:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
σ τ : Aut F
hst : σ ≈ τ
J' : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V) ⥤ Action FintypeCat (Aut F) := quotientDiag V h u ⋙ functorToAction F
m : End (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V)) := ⟦⟨σ⁻¹ * τ, ⋯⟩⟧
h1 :
  J'.map m ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V)) = s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))
⊢ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧ =
    (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦τ⟧
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 X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Y i₂)).hom (Z i₃) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.whiskerLeft (Y i₂) (β_ (X i₁) (Z i₃)).hom ≫
        MonoidalCategoryStruct.whiskerLeft (Y i₂) (ιTensorObj Z X i₃ i₁ (i₁ + i₃) ⋯) ≫
          ιTensorObj Y (tensorObj Z X) i₂ (i₁ + i₃) k ⋯

Tactic:
← ιTensorObj₃_eq Y Z X i₂ i₃ i₁ k (by rw [add_comm _ i₁, ← add_assoc, 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 X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Y i₂)).hom (Z i₃) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.whiskerLeft (Y i₂) (β_ (X i₁) (Z i₃)).hom ≫ ιTensorObj₃ Y Z X i₂ i₃ i₁ k ⋯
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ ⟨f, ⋯⟩ = ⟨g, ⋯⟩ → ⟨f, hf⟩ = ⟨g, hg⟩

Tactic:
rw [Subtype.mk_eq_mk, Subtype.mk_eq_mk]

Goal state after:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ f = g → f = g
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ 𝟙 c ∈ (comap φ S).arrows c c

Tactic:
rw [comap, mem_ofPred, Functor.map_id]

Goal state after:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ 𝟙 (φ.obj c) ∈ S.arrows (φ.obj c) (φ.obj c)
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    𝟙 (P ⊞ P.complement)

Tactic:
apply biprod.hom_ext'

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inl ≫ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    biprod.inl ≫ 𝟙 (P ⊞ P.complement)

case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inr ≫ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    biprod.inr ≫ 𝟙 (P ⊞ P.complement)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected → ∀ (c d : C), (S.arrows c d).Nonempty → c = d

Tactic:
rintro h c d ⟨f, fS⟩

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsTotallyDisconnected
c d : C
f : c ⟶ d
fS : f ∈ S.arrows c d
⊢ c = d
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
inst✝ : BraidedCategory C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
h : X ⟶ Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty f (Opposite.op (Arrow.mk g) ⋔ Arrow.mk h).hom

Tactic:
rw [← hasLiftingProperty_mk_iff]
  exact HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)

Tactic:
by
    have : Nonempty (CostructuredArrow (parallelPair f g) Z) :=
      ⟨mk (Y := zero) (h₁ Z).some⟩
    have : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x
      (mk (Y := zero) (h₁ Z).some) := by
        rintro ⟨(_ | _), ⟨⟩, φ⟩
        · apply h₂
        · refine Zigzag.trans ?_ (h₂ (f ≫ φ) _)
          exact Zigzag.of_inv (homMk left)
    exact zigzag_isConnected (fun x y => (this x).trans (this y).symm)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
hx : (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Tactic:
by
  rw [show 0 = colimit.ι F j 0 by simp, colimit_rep_eq_iff_exists] at hx
  obtain ⟨j', i, y, g⟩ := hx
  exact ⟨j', i, g ▸ by simp⟩

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

Goal state before:
pp: case inr
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
⊢ IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)

Tactic:
have hα (i j) (f : i ⟶ j) : α.app i ≫ c.map f = α.app j := by simp [← NatTrans.naturality]

Goal state after:
case inr
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
⊢ IsPullback (G.left.map f) (G.hom.app U) (G.hom.app V) (F.map f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ IsClosedUnderColimitsOfShape (fun f ↦ Coequifibered f.hom) J

Tactic:
isClosedUnderColimitsOfShape_iff_op,

Goal state after:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ (ObjectProperty.op fun f ↦ Coequifibered f.hom).IsClosedUnderLimitsOfShape Jᵒᵖ
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ ((ObjectProperty.op fun f ↦ Coequifibered f.hom).inverseImage e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
convert!
    (inferInstance : IsClosedUnderLimitsOfShape (fun f : Over F.op ↦ f.hom.Equifibered) Jᵒᵖ) with f

Goal state after:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := ⋯
f : Over F.op
⊢ (ObjectProperty.op fun f ↦ Coequifibered f.hom).inverseImage e.functor f ↔ Equifibered f.hom
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁵ : Category.{v_1, u_5} K
inst✝⁴ : Category.{v_2, u_6} K'
inst✝³ : Category.{v_3, u_1} J
inst✝² : Category.{v_4, u_2} J'
inst✝¹ : Category.{v_5, u_3} C
inst✝ : Category.{v_6, u_4} D
⊢ (preservesColimitsOfShape K).IsClosedUnderIsomorphisms

Tactic:
preservesColimitsOfShape_eq_iSup

Goal state after:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁵ : Category.{v_1, u_5} K
inst✝⁴ : Category.{v_2, u_6} K'
inst✝³ : Category.{v_3, u_1} J
inst✝² : Category.{v_4, u_2} J'
inst✝¹ : Category.{v_5, u_3} C
inst✝ : Category.{v_6, u_4} D
⊢ (⨅ F, preservesColimit F).IsClosedUnderIsomorphisms
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_empty
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst✝³ : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst✝² : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝¹ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst✝ : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
x✝³ x✝² : (i : PEmpty.{w + 1}) → C i
x✝¹ : x✝³ ⟶ x✝²
x✝ : MorphismProperty.pi W x✝¹
⊢ MorphismProperty.isomorphisms ((i : PEmpty.{w + 1}) → C i) x✝¹

Tactic:
rw [MorphismProperty.isomorphisms.iff, isIso_pi_iff]

Goal state after:
case h_empty
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst✝³ : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst✝² : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝¹ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst✝ : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
x✝³ x✝² : (i : PEmpty.{w + 1}) → C i
x✝¹ : x✝³ ⟶ x✝²
x✝ : MorphismProperty.pi W x✝¹
⊢ ∀ (i : PEmpty.{w + 1}), IsIso (x✝¹ i)
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
x x' : C
f : x ⟶ x'
y : C
z : D
⊢ f ⊵ₗ (y ⊙ₗ z) = (αₗ x y z).inv ≫ (f ▷ y) ⊵ₗ z ≫ (αₗ x' y z).hom

Tactic:
simp [whiskerRight_actionHomLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
y : D
z x x' : C
f : x ⟶ x'
⊢ (y ⊙ᵣ z) ⊴ᵣ f = (αᵣ y z x).inv ≫ y ⊴ᵣ z ◁ f ≫ (αᵣ y z x').hom

Tactic:
simp [whiskerRight_actionHomLeft]

Goal state after: