mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ IsFilteredOrEmpty (Grothendieck F)

Tactic:
refine ⟨?_, ?_⟩
  · rintro ⟨c, f⟩ ⟨d, g⟩
    exact ⟨⟨max c d, max ((F.map (leftToMax c d)).toFunctor.obj f)
      ((F.map (rightToMax c d)).toFunctor.obj g)⟩,
      ⟨leftToMax c d, leftToMax _ _⟩, ⟨rightToMax c d, rightToMax _ _⟩, trivial⟩
  · rintro ⟨c, f⟩ ⟨d, g⟩ ⟨u, x⟩ ⟨v, y⟩
    refine ⟨⟨coeq u v, coeq (eqToHom ?_ ≫
        (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y)⟩,
          ⟨coeqHom u v, coeqHom _ _⟩, ?_⟩
    · conv_rhs => rw [← Cat.Hom.comp_obj, ← F.map_comp, coeq_condition, F.map_comp,
        Cat.Hom.comp_obj]
    · set_option backward.isDefEq.respectTransparency.types false in
      apply Grothendieck.ext _ _ (coeq_condition u v)
      refine Eq.trans ?_ (eqToHom _ ≫= coeq_condition _ _)
      simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : PreGaloisCategory C
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
G' : Type ?u.17
hg : Group G'
hf : Fintype G'
e : G ≃* G'
⊢ HasColimitsOfShape (SingleObj G) C

Tactic:
exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

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

Goal state before:
pp: G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
⊢ (ConcreteCategory.hom (Y.ρ g).hom) ↑y ∈ (Set.range ⇑(ConcreteCategory.hom f.hom))ᶜ

Tactic:
intro ⟨x, h⟩
      apply y.property
      use (X.ρ g⁻¹).hom x
      calc (X.ρ g⁻¹ ≫ f.hom) x
          = ((Y.ρ g⁻¹ * Y.ρ g)).hom y.val := by rw [f.comm, FintypeCat.comp_apply, h]; rfl
        _ = y.val := by
          simp [← map_mul, inv_mul_cancel, Action.ρ_one, FintypeCat.id_hom]

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

Goal state before:
pp: G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
⊢ (ConcreteCategory.hom (Y.ρ g).hom) ↑y ∈ (Set.range ⇑(ConcreteCategory.hom f.hom))ᶜ

Tactic:
by
      intro ⟨x, h⟩
      apply y.property
      use (X.ρ g⁻¹).hom x
      calc (X.ρ g⁻¹ ≫ f.hom) x
          = ((Y.ρ g⁻¹ * Y.ρ g)).hom y.val := by rw [f.comm, FintypeCat.comp_apply, h]; rfl
        _ = y.val := by
          simp [← map_mul, inv_mul_cancel, Action.ρ_one, FintypeCat.id_hom]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
G' : Type ?u.12
hg : Group G'
hf : Fintype G'
e : G ≃* G'
⊢ HasColimitsOfShape (SingleObj G) FintypeCat

Tactic:
exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

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✝ : IsConnected X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := (e X).symm x
hx' : x' = (e X).symm x
y' : (F'.obj X).obj := (e X).symm y
hy' : y' = (e X).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
g : F ≅ F := NatIso.ofComponents gapp ⋯
⊢ ∃ g, g • x = y

Tactic:
refine ⟨g, show (gapp X).hom x = y from ?_⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := (e X).symm x
hx' : x' = (e X).symm x
y' : (F'.obj X).obj := (e X).symm y
hy' : y' = (e X).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
g : F ≅ F := NatIso.ofComponents gapp ⋯
⊢ (ConcreteCategory.hom (gapp X).hom) x = y
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
⊢ c ∈ S.objs → 𝟙 c ∈ S.arrows c c

Tactic:
by
  rintro ⟨γ, hγ⟩
  convert! S.mul hγ (S.inv hγ)
  simp only [inv_eq_inv, IsIso.hom_inv_id]

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

Tactic:
rw [SetLike.le_def, Sigma.forall]

Goal state after:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ (∀ (a : C) (b : (d : C) × (a ⟶ d)), ⟨a, b⟩ ∈ S → ⟨a, b⟩ ∈ T) ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
x✝¹ x✝ : ↑S.objs
s : C
hs : s ∈ S.objs
t : C
ht : t ∈ S.objs
⊢ (inclusion h).obj ⟨s, hs⟩ = (inclusion h).obj ⟨t, ht⟩ → ⟨s, hs⟩ = ⟨t, ht⟩

Tactic:
simpa only [inclusion, Subtype.mk_eq_mk] using id

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

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty → ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Tactic:
rintro ⟨f, hf⟩
    change Map.Arrows φ hφ S d d f at hf; rw [Map.arrows_iff] at hf
    obtain ⟨c, d, g, ec, ed, eg, gS, eg⟩ := hf
    exact ⟨c, ⟨mem_objs_of_src S eg, ec⟩⟩

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

Goal state before:
pp: case left.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² a✝¹ : C
f : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝).Hom d
g : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d

Goal state after:
case left.left.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : C
f : (left a✝³).Hom (left a✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.left.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : C
f : (left a✝³).Hom (left a✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² a✝¹ : C
f : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (right a✝).Hom d
g : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d

Goal state after:
case left.left.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : C
f : (left a✝³).Hom (left a✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.left.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : C
f : (left a✝³).Hom (left a✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² : C
a✝¹ : D
f : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (left a✝).Hom d
g : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d

Goal state after:
case left.right.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : C
a✝² : D
f : (left a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.right.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : C
a✝² : D
f : (left a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² : C
a✝¹ : D
f : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝).Hom d
g : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d

Goal state after:
case left.right.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : C
a✝² : D
f : (left a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case left.right.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : C
a✝² : D
f : (left a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² : D
a✝¹ : C
f : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝).Hom d
g : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d

Goal state after:
case right.left.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.left.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² : D
a✝¹ : C
f : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (right a✝).Hom d
g : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d

Goal state after:
case right.left.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.left.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² a✝¹ : D
f : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (left a✝).Hom d
g : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d

Goal state after:
case right.right.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.right.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
d : C ⋆ D
a✝² a✝¹ : D
f : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝).Hom d
g : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases d

Goal state after:
case right.right.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

case right.right.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : FormalCoproduct C
i j k : X.I
hij : i = j
hjk : j = k
⊢ X.objIsoOfEq hij ≪≫ X.objIsoOfEq hjk = X.objIsoOfEq ⋯

Tactic:
by
  subst hij hjk
  simp

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₁₂ ≫ h₁₂.p = h.p

Tactic:
← h₁₂.hp₂,

Goal state after:
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₁₂ ≫ h₁₂.p₂ ≫ f₂ = h.p
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
f : md → (X ⟶ Y)
⊢ (fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) (Pi.lift f) = f

Tactic:
ext k

Goal state after:
case refine_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
f : md → (X ⟶ Y)
k : md
⊢ (fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) (Pi.lift f) k = f k
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
⊢ (preservesLimitsOfShape K).IsClosedUnderIsomorphisms

Tactic:
rw [preservesLimitsOfShape_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, preservesLimit F).IsClosedUnderIsomorphisms
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
C : Type u_3
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_5, u_3} C
e : K ≌ K'
G : J ⥤ C
⊢ preservesColimitsOfShape K G ↔ preservesColimitsOfShape K' G

Tactic:
simp only [preservesColimitsOfShape_iff]

Goal state after:
J : Type u_1
C : Type u_3
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_5, u_3} C
e : K ≌ K'
G : J ⥤ C
⊢ PreservesColimitsOfShape K G ↔ PreservesColimitsOfShape K' G
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
K : Type u_2
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F✝ : J ⥤ C
D : Type u_4
inst✝¹ : Category.{v_4, u_4} D
G : K ⥤ D
F : J ⥤ C
inst✝ : HasWeakLimit F
j j' : J
hj : j = j'
⊢ F.obj j = F.obj j'

Tactic:
subst hj

Goal state after:
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
K : Type u_2
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F✝ : J ⥤ C
D : Type u_4
inst✝¹ : Category.{v_4, u_4} D
G : K ⥤ D
F : J ⥤ C
inst✝ : HasWeakLimit F
j : J
⊢ F.obj j = F.obj j
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
inst✝ : HasWeakLimit F
j j' : J
hj : j = j'
⊢ π F j ≫ eqToHom ⋯ = π F j'

Tactic:
subst hj

Goal state after:
J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_3
inst✝¹ : Category.{v_3, u_3} C
F : J ⥤ C
inst✝ : HasWeakLimit F
j : J
⊢ π F j ≫ eqToHom ⋯ = π F j
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
⊢ ∃ a, (fun g ↦ f ≫ g) a = g

Tactic:
let d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData :=
        .ofExists (fun j hj ↦ (hf.map_mem j hj _ hZ).2) (fun j hj s ↦ by
          let c : Cocone ((Set.principalSegIio j).monotone.functor ⋙ hf.F) :=
            { pt := Z
              ι.app k := s.1 (op k)
              ι.naturality _ _ g := by
                dsimp
                simpa only [Category.comp_id] using! s.2 g.op }
          exact ⟨(hf.F.isColimitOfIsWellOrderContinuous j hj).desc c, fun k hk ↦
            by simpa using! (hf.F.isColimitOfIsWellOrderContinuous j hj).fac c ⟨k, hk⟩⟩)
      let σ := d.sectionsMk (hf.isoBot.hom ≫ g)
      let c : Cocone hf.F :=
        { pt := Z
          ι.app j := σ.1 (op j)
          ι.naturality _ _ f := by
            dsimp
            simpa only [Category.comp_id] using! σ.2 f.op }
      exact ⟨hf.isColimit.desc c, by
        simp only [← hf.fac, Category.assoc, hf.isColimit.fac c ⊥, c, σ,
          d.sectionsMk_val_op_bot, Iso.inv_hom_id_assoc]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option
J : Type w
inst✝ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
⊢ ∀ {C : Option J → Type u₁} {D : Option J → Type u₂} [inst : (j : Option J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → C j ⥤ D j)
    (W : (j : Option J) → MorphismProperty (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
    [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
C

Goal state after:
case h_option
J : Type w
inst✝ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
⊢ ∀ {D : Option J → Type u₂} [inst : (j : Option J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → C j ⥤ D j)
    (W : (j : Option J) → MorphismProperty (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
    [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
t : X ⟶ Y
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
⊢ motive t

Tactic:
induction t using Quotient.inductionOn with

Goal state after:
case h
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
f : X ⟶ᵐ Y
⊢ motive ⟦f⟧
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case id_whiskerRight
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 𝟙 (projectObj f✝ X✝) ▷ projectObj f✝ Y✝ = 𝟙 (projectObj f✝ X✝ ⊗ projectObj f✝ Y✝)

Tactic:
MonoidalCategory.id_whiskerRight

Goal state after:
case id_whiskerRight
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 𝟙 (projectObj f✝ X✝ ⊗ projectObj f✝ Y✝) = 𝟙 (projectObj f✝ X✝ ⊗ projectObj f✝ Y✝)
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalLeftAction C D
inst✝¹ : MonoidalLeftAction C D'
inst✝ : F.OplaxLeftLinear C
c c' : C
d : D
⊢ δₗ F c (c' ⊙ₗ d) ≫ c ⊴ₗ δₗ F c' d ≫ (αₗ c c' (F.obj d)).inv = F.map (αₗ c c' d).inv ≫ δₗ F (c ⊗ c') d

Tactic:
by
  simpa [-δₗ_associativity, -δₗ_associativity_assoc] using
    F.map (αₗ _ _ _).inv ≫=
      (δₗ_associativity F c c' d).symm =≫
      (αₗ _ _ _).inv

Goal state after: