mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ Y' s, ∃ (_ : P.isoModSerre s), f ≫ s = 0) → P (Abelian.image f)

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ Y' s, ∃ (_ : P.isoModSerre s), f ≫ s = 0

Tactic:
· rintro ⟨Y', s, hs, eq⟩
    rw [← exists_comp_monoModSerre_eq_zero_iff P]
    exact ⟨Y', s, hs.1, eq⟩

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ Y' s, ∃ (_ : P.isoModSerre s), f ≫ s = 0
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ ∀ (x y : G), ⟨1, x * y⟩ = ⟨1, x⟩ * ⟨1, y⟩

Tactic:
intros; ext <;> simp

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 : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.f
⊢ L.map φ.f ≫ L.map f = 0

Tactic:
rw [← hφ, Category.assoc, Category.assoc, hw, comp_zero, comp_zero]

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
C : Type u_3
inst✝ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
⊢ PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F

Tactic:
constructor
  intro J _
  apply Action.preservesColimitsOfShape_of_preserves
  exact PreservesColimitsOfSize.preservesColimitsOfShape

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

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

Tactic:
exact (inferInstance : Epi (((evaluation _ _).obj c).map η))

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ (t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X))
      ((t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X)).symm (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)) =
    t.leftToRight.app (G.obj X)

Tactic:
homEquiv_symm_apply,

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ (t.adj₂.homEquiv (F.obj (G.obj X)) (G.obj X))
      (G.map (t.adj₁.counit.app X ≫ t.adj₂.unit.app X) ≫ t.adj₂.counit.app (G.obj X)) =
    t.leftToRight.app (G.obj X)
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
⊢ ∀ ⦃X Y : (i : I) × C i⦄ (f : X ⟶ Y),
    (Functor.sigma F).map f ≫ SigmaHom.mk ((α Y.fst).app Y.snd) =
      SigmaHom.mk ((α X.fst).app X.snd) ≫ (Functor.sigma G).map f

Tactic:
by
    rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
    change SigmaHom.mk _ = SigmaHom.mk _
    rw [(α i).naturality]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : (f a).get h₂ = Sum.inl b✝
h₃ : b ∈ Part.some b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
simp only [Part.mem_some_iff] at h₃

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : (f a).get h₂ = Sum.inl b✝
h₃ : b = b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
a'✝ : α
e : (f a).get h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p ↦
        WellFounded.fixF
          (fun a IH ↦
            Part.assert (f a).Dom fun hf ↦
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          y ⋯)
      a'✝ ⋯

Tactic:
injection h₂.symm.trans e

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: 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
hif : IsIso (↾f)
⊢ ∃ f, graphFunctor.map f.hom = r

Tactic:
use asIso (↾f)
      ext ⟨x, y⟩
      exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X : ↑s.pt), (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X

pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
· intro X
      apply Types.limit_ext.{v, v}
      intro j
      simp [← comp_apply, ← w j]

Goal state after:
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ ∀ (X Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y₁ Y₂ : LocalizedMonoidal L W ε
f : Y₁ ⟶ Y₂
⊢ 𝟙 X ⊗ₘ f = X ◁ f

Tactic:
by
  simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ : LocalizedMonoidal L W ε
f : X₁ ⟶ X₂
Y : LocalizedMonoidal L W ε
⊢ f ⊗ₘ 𝟙 Y = f ▷ Y

Tactic:
by
  simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂ = (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)

Tactic:
by
  simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ : LocalizedMonoidal L W ε
⊢ 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)

Tactic:
by
  simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
⊢ X ◁ 𝟙 Y = 𝟙 (X ⊗ Y)

Tactic:
by
  simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
⊢ 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)

Tactic:
by
  simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.EnrichedCat

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u₁
inst✝¹ : EnrichedCategory V D
E : Type u₂
inst✝ : EnrichedCategory V E
F G H : EnrichedFunctor V C D
α : F ⟶ G
β : G ⟶ H
I : EnrichedFunctor V D E
⊢ whiskerRight { out := α.out ≫ β.out } I = whiskerRight α I ≫ whiskerRight β I

Tactic:
by
  ext X
  simp only [whiskerRight_out_app, NatTrans.comp_app, EnrichedFunctor.category_comp_out,
    EnrichedFunctor.forget, EnrichedFunctor.comp_obj, EnrichedFunctor.comp_map]
  simp [← ForgetEnrichment.homOf_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) g) ≫ eComp V X Y Z ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom

Tactic:
← eHomEquiv_comp_assoc

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ (eHomCongr V α γ).hom =
    (λ_ (𝟙_ V)).inv ≫
      ((eHomEquiv V) f ≫ (eHomCongr V α β).hom) ▷ 𝟙_ V ≫
        (X₁ ⟶[V] Y₁) ◁ ((eHomEquiv V) g ≫ (eHomCongr V β γ).hom) ≫ eComp V X₁ Y₁ Z₁

Tactic:
simp only [eHomCongr, MonoidalCategory.whiskerRight_id, assoc,
    MonoidalCategory.whiskerLeft_comp]
  rw [rightUnitor_inv_naturality_assoc, rightUnitor_inv_naturality_assoc,
    rightUnitor_inv_naturality_assoc, hom_inv_id_assoc, ← whisker_exchange_assoc,
    ← whisker_exchange_assoc, ← eComp_eHomWhiskerLeft, eHom_whisker_cancel_assoc,
    ← eComp_eHomWhiskerRight_assoc, ← tensorHom_def_assoc,
    ← eHomEquiv_comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
f : X ⟶ Y
⊢ 𝟙_ (LocalizedMonoidal L W ε) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
by
  simp +instances [monoidalCategoryStruct]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
j : J
⊢ enrichedComp V F₁ F₂ F₃ ≫ end_.π (diagram V F₁ F₃) j =
    (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)

Tactic:
by
  simp [enrichedComp]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F.toFunctor ≅ G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.hom.app a)
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.inv.app a)

Tactic:
by
      have : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom := (Iso.app_hom α a) ▸ isHomLift' a
      rw [← Iso.app_inv]
      apply IsHomLift.lift_id_inv

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R R' S : 𝒮
a a' b : 𝒳
f : R ⟶ S
f' : R' ⟶ S
g : R' ≅ R
h : f' = g.hom ≫ f
φ : a ⟶ b
φ' : a' ⟶ b
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian f' φ'
this : p.IsHomLift ((fun x ↦ g.inv ≫ x) (g.hom ≫ f)) φ
⊢ p.IsHomLift g.inv (domainIsoOfBaseIso p h φ φ').inv

Tactic:
simpa using IsStronglyCartesian.map_isHomLift p f' φ' (congrArg (g.inv ≫ ·) h.symm) φ

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

Goal state before:
pp: A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
⊢ IsFiltered A

Tactic:
refine isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨?_⟩

Goal state after:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
⊢ limit (colimit F.flip) ⟶ colimit (limit F)
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := ⋯
this✝² : Fintype ↑T
this✝¹ : MulAction G (FintypeCat.of ↑T).obj := ⋯
T' : Action FintypeCat G := ⋯
i : T' ⟶ X := ⋯
this✝ : Mono i
this : IsIso i
⊢ IsIso i.hom

Tactic:
exact map_isIso (forget₂ _ FintypeCat) i

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

Goal state before:
pp: case pos
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
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
have hn2 : Nat.card (F.obj Z) < n := by
      rw [hn, hnn, lt_add_iff_pos_left]
      exact Nat.pos_of_ne_zero (non_zero_card_fiber_of_not_initial F Y hni)

Goal state after:
case pos
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
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
hn2 : Nat.card (F.obj Z).obj < n
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Groupoid.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f = f ≫ inv g ≫ g

Tactic:
simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), 𝟙 c ∈ (sInf s).arrows c c

Tactic:
simp_rw [sInf, mem_iInter₂]

Goal state after:
C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), ∀ i ∈ s, 𝟙 c ∈ i.arrows c c
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, γ ∈ (sInf s).arrows c c → Groupoid.inv p ≫ γ ≫ p ∈ (sInf s).arrows d d

Tactic:
simp_rw [sInf, mem_iInter₂]

Goal state after:
C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, (∀ i ∈ s, γ ∈ i.arrows c c) → ∀ i ∈ s, Groupoid.inv p ≫ γ ≫ p ∈ i.arrows d d
Module: Mathlib.CategoryTheory.Join.Sum

Goal state before:
pp: case inl.inl
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : C
f✝¹ f✝ : x✝ ⟶ y✝
heq : (inclLeft C D).map f✝¹ = (inclLeft C D).map f✝
⊢ (Sum.inl_ C D).map f✝¹ = (Sum.inl_ C D).map f✝

Tactic:
simp [Functor.map_injective _ heq]

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

Goal state before:
pp: case inr.inr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
x✝ y✝ : D
f✝¹ f✝ : x✝ ⟶ y✝
heq : (inclRight C D).map f✝¹ = (inclRight C D).map f✝
⊢ (Sum.inr_ C D).map f✝¹ = (Sum.inr_ C D).map f✝

Tactic:
simp [Functor.map_injective _ heq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ (X_1 : X ⥤ F ⊡ G),
    { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ } =
      𝟙
        { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
          iso :=
            X_1.associator (π₁ F G) F ≪≫
              X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm }

Tactic:
intros; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ {X_1 Y Z : X ⥤ F ⊡ G} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    { fst := whiskerRight (f ≫ g) (π₁ F G), snd := whiskerRight (f ≫ g) (π₂ F G), w := ⋯ } =
      { fst := whiskerRight f (π₁ F G), snd := whiskerRight f (π₂ F G), w := ⋯ } ≫
        { fst := whiskerRight g (π₁ F G), snd := whiskerRight g (π₂ F G), w := ⋯ }

Tactic:
intros; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ (X_1 : CatCommSqOver F G X),
    { app := fun x ↦ { fst := (𝟙 X_1).fst.app x, snd := (𝟙 X_1).snd.app x, w := ⋯ }, naturality := ⋯ } =
      𝟙
        { obj := fun x ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x },
          map := fun {x y} f ↦ { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }

Tactic:
intros; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ {X_1 Y Z : CatCommSqOver F G X} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    { app := fun x ↦ { fst := (f ≫ g).fst.app x, snd := (f ≫ g).snd.app x, w := ⋯ }, naturality := ⋯ } =
      { app := fun x ↦ { fst := f.fst.app x, snd := f.snd.app x, w := ⋯ }, naturality := ⋯ } ≫
        { app := fun x ↦ { fst := g.fst.app x, snd := g.snd.app x, w := ⋯ }, naturality := ⋯ }

Tactic:
intros; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ {X_1 Y : X ⥤ F ⊡ G} (f : X_1 ⟶ Y),
    (𝟭 (X ⥤ F ⊡ G)).map f ≫
        (NatIso.ofComponents
            (fun x ↦
              mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y).obj x).snd) ⋯)
            ⋯).hom =
      (NatIso.ofComponents
            (fun x ↦
              mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X_1).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X_1).obj x).snd) ⋯)
            ⋯).hom ≫
        (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).map f

Tactic:
intros; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ (X_1 : X ⥤ F ⊡ G),
    (toCatCommSqOver F G X).map
          ((NatIso.ofComponents
                  (fun x ↦
                    NatIso.ofComponents
                      (fun x_1 ↦
                        mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                          (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                      ⋯)
                  ⋯).hom.app
            X_1) ≫
        (NatIso.ofComponents
                (fun x ↦
                  CatCommSqOver.mkIso
                    (NatIso.ofComponents
                      (fun x_1 ↦
                        Iso.refl
                          (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).fst.obj
                            x_1))
                      ⋯)
                    (NatIso.ofComponents
                      (fun x_1 ↦
                        Iso.refl
                          (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).snd.obj
                            x_1))
                      ⋯)
                    ⋯)
                ⋯).hom.app
          ((toCatCommSqOver F G X).obj X_1) =
      𝟙 ((toCatCommSqOver F G X).obj X_1)

Tactic:
intros; ext <;> simp

Goal state after: