mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: V : Type (u + 1)
inst✝³ : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst✝² : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝¹ : ConcreteCategory V FV
G : Type u_3
inst✝ : Monoid G
X : Action V G
g h : G
x : ToType X
⊢ (g * h) • x = g • h • x

Tactic:
by
    change ConcreteCategory.hom (X.ρ (g * h)) x =
      ConcreteCategory.hom (X.ρ g) ((ConcreteCategory.hom (X.ρ h)) x)
    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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this✝ : HasFiniteProducts D
this : HasKernels D
⊢ Abelian D

Tactic:
have := hasCokernels L P

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this✝¹ : HasFiniteProducts D
this✝ : HasKernels D
this : HasCokernels D
⊢ Abelian D
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁴ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝³ : ConcreteCategory V FV
inst✝² : HasForget₂ V TopCat
G : Type u_4
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
X : Action V G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ 1 • x = x

Tactic:
by
    change ((CategoryTheory.forget₂ _ TopCat).map (X.ρ 1)) x = x
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
⊢ { l //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }

Tactic:
have := fun Y ↦ h Y |>.mono

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ { l //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h✝ : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (adj₂.homEquiv X (F.obj Y'))
      ((adj₁.homEquiv (L.obj X) (F.obj Y')).symm
        ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj X)) (L.map g ≫ h))) =
    ↑((Fork.IsLimit.homIso
          (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) X)
        (g ≫
          (Fork.IsLimit.homIso
                (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y).symm
            ⟨(adj₂.homEquiv Y (F.obj Y'))
                ((adj₁.homEquiv (L.obj Y) (F.obj Y')).symm
                  ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h)),
              ⋯⟩))

Tactic:
simp only [Adjunction.homEquiv_counit]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h✝ : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (adj₂.homEquiv X (F.obj Y'))
      (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj X)) (L.map g ≫ h)) ≫ adj₁.counit.app (F.obj Y')) =
    ↑((Fork.IsLimit.homIso
          (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) X)
        (g ≫
          (Fork.IsLimit.homIso
                (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y).symm
            ⟨(adj₂.homEquiv Y (F.obj Y'))
                (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h) ≫ adj₁.counit.app (F.obj Y')),
              ⋯⟩))
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (f ◁ η) =
      (Iso.refl (liftHom F (f ≫ g))).hom ≫ liftHom F f ◁ Quot.lift (liftHom₂ F) ⋯ η ≫ (Iso.refl (liftHom F (f ≫ h))).inv

Tactic:
intro a b c f g h η
    induction η using Quot.rec
    · cat_disch
    · rfl

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

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
              θ.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ ι.app b ⊗≫ (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫
              θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [← whisker_exchange]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j : ConnectedComponents J
⊢ IsConnected j.Component

Tactic:
by
  -- Show it's connected by constructing a zigzag (in `j.Component`) between any two objects
  apply isConnected_of_zigzag
  rintro ⟨j₁, hj₁⟩ ⟨j₂, rfl⟩
  -- We know that the underlying objects j₁ j₂ have some zigzag between them in `J`
  have h₁₂ : Zigzag j₁ j₂ := Quotient.exact' hj₁
  -- Get an explicit zigzag as a list
  rcases List.exists_isChain_cons_of_relationReflTransGen h₁₂ with ⟨l, hl₁, hl₂⟩
  -- Everything which has a zigzag to j₂ can be lifted to the same component as `j₂`.
  let f : ∀ x, Zigzag x j₂ → (ConnectedComponents.mk j₂).Component :=
    fun x h => ⟨x, Quotient.sound' h⟩
  -- Everything in our chosen zigzag from `j₁` to `j₂` has a zigzag to `j₂`.
  have hf : ∀ a : J, a ∈ l → Zigzag a j₂ := by
    intro i hi
    apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)
    · intro j k
      apply Relation.ReflTransGen.head
    · apply Relation.ReflTransGen.refl
  -- Now lift the zigzag from `j₁` to `j₂` in `J` to the same thing in `j.Component`.
  refine ⟨l.pmap f hf, ?_, by grind⟩
  refine @List.isChain_cons_pmap_of_isChain_cons _ _ Zag _ _ f
    (fun x y _ _ h => ?_) _ _ h₁₂ hl₁ _
  exact zag_of_zag_obj (ConnectedComponents.ι _) h

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
b : β
⊢ b ∈ res f s a ↔ a ∈ s ∧ f a = b

Tactic:
by
  simp [res, @eq_comm _ b]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
this :
  Functor.whiskerRight ((mapPullbackAdj (𝟙 X)).rightAdjointUniq (mapPullbackAdj (𝟙 X))).hom (map (𝟙 X)) ≫
      (mapPullbackAdj (𝟙 X)).counit =
    (mapPullbackAdj (𝟙 X)).counit
⊢ Functor.whiskerRight (pullbackId X).hom (map (𝟙 X)) ≫ (mapPullbackAdj (𝟙 X)).counit = (mapPullbackAdj (𝟙 X)).counit

Tactic:
rw [pullbackId, Adjunction.rightAdjointUniq_hom_counit]

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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
⊢ Pentagon Y₁ Y₂ Y₃ Y₄

Tactic:
obtain ⟨X₃, ⟨e₃⟩⟩ : ∃ X₃, Nonempty ((L').obj X₃ ≅ Y₃) := ⟨_, ⟨(L').objObjPreimageIso Y₃⟩⟩

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
⊢ Pentagon Y₁ Y₂ Y₃ Y₄
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂R X Y Z).hom = coprod.inl ▷ X

Tactic:
rw [rightDistrib_hom, coprod.inl_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case refine_1
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ⊗ₘ 𝟙 (L'.obj X₄)) ≫
        (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
          (e₁.hom ⊗ₘ (e₂.hom ⊗ₘ e₃.hom) ⊗ₘ e₄.hom) ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom)

Tactic:
← associator_naturality_assoc,

Goal state after:
case refine_1
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ⊗ₘ 𝟙 (L'.obj X₄)) ≫
        ((e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom) ⊗ₘ e₄.hom) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom)
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ V₁.str ≫ F.map h.inv = h.inv ≫ V₀.str

Tactic:
rw [h.eq_inv_comp, ← Category.assoc, ← w, Category.assoc, ← F.map_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
⊢ ∀ {a' : 𝒳} (g_1 : p.obj a' ⟶ R) (φ' : a' ⟶ c) [p.IsHomLift (g_1 ≫ f ≫ g) φ'], ∃! χ, p.IsHomLift g_1 χ ∧ χ ≫ φ ≫ ψ = φ'

Tactic:
intro a' h τ hτ
    use map p f φ (f' := h ≫ f) rfl (map p g ψ (assoc h f g).symm τ)
    refine ⟨⟨inferInstance, ?_⟩, ?_⟩
    · rw [← assoc, fac, fac]
    · intro π' ⟨hπ'₁, hπ'₂⟩
      apply map_uniq
      apply map_uniq
      simp only [assoc, hπ'₂]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_2} D
inst✝² : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
⊢ F.HasLeftDerivedFunctor W

Tactic:
have := IsLeftDerivedFunctor.isRightKanExtension LF α W

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_2} D
inst✝² : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
this : LF.IsRightKanExtension α
⊢ F.HasLeftDerivedFunctor W
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: case refine_1
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
f : X₁ ⟶ X₂
φ : 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 φ)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (φ ≫ L.map f)) =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))

Tactic:
have eq := s.π.naturality
        (StructuredArrow.homMk f : StructuredArrow.mk φ ⟶ StructuredArrow.mk (φ ≫ L.map f))
      dsimp at eq hφ ⊢
      rw [id_comp] at eq
      rw [assoc] at hφ
      simp [eq, ← reassoc_of% hφ, ← e.inv.naturality f]

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
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom (F.map prod.snd))
      ((PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y ≪≫
              Types.binaryProductIso (F.obj X).obj (F.obj Y).obj).toEquiv.symm
        (x, y)) =
    y

Tactic:
change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.snd) _ = _

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom
        ((Types.binaryProductIso ((pair X Y ⋙ F ⋙ FintypeCat.incl).obj { as := WalkingPair.left })
              ((pair X Y ⋙ F ⋙ FintypeCat.incl).obj { as := WalkingPair.right })).inv ≫
          ((Cone.postcomposeEquivalence (diagramIsoPair (pair X Y ⋙ F ⋙ FintypeCat.incl))).symm.inverse.map
                ((isLimitOfPreserves (F ⋙ FintypeCat.incl) (prodIsProd X Y)).liftConeMorphism
                  ((Cone.postcomposeEquivalence (diagramIsoPair (pair X Y ⋙ F ⋙ FintypeCat.incl))).symm.functor.obj
                    (limit.cone (pair ((F ⋙ FintypeCat.incl).obj X) ((F ⋙ FintypeCat.incl).obj Y)))))).hom ≫
            (F ⋙ FintypeCat.incl).map prod.snd))
      (x, y) =
    y
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A : C
inst✝ : IsConnected A
⊢ Finite (Aut A)

Tactic:
by
  let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  apply Finite.of_injective (fun f ↦ F.map f.hom a)
  exact evaluation_aut_injective_of_isConnected F A a

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
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b

Tactic:
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

Goal state after:
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
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c✝ d✝ : C
p : d✝ ⟶ c✝
γ : c✝ ⟶ c✝
hs : γ ∈ S.arrows c✝ c✝
⊢ p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d✝ d✝

Tactic:
convert! Sn.conj (Groupoid.inv p) hs; simp

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ X c d ⊆ (generated X).arrows c d

Tactic:
by
  dsimp only [generated, sInf]
  simp only [subset_iInter₂_iff]
  exact fun S hS f fS => hS _ _ fS

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ 𝟭 C = (e.functor ⋙ f.functor) ⋙ f.inverse ⋙ e.inverse

Tactic:
by
    rw [Functor.assoc, ← Functor.assoc f.functor, ← f.unit_eq, Functor.id_comp]
    exact e.unit_eq

Goal state after:
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'
    · rw [biprod.inl_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_left, ← assoc]
      refine (?_ =≫ _).trans zero_comp
      ext
      simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f,
        complement_p, comp_sub, comp_id, idem, sub_self, zero_def]
    · rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_right, ← assoc]
      refine (?_ =≫ _).trans zero_comp
      ext
      simp only [complement_X, comp_f, decompId_i_f, complement_p,
        decompId_p_f, sub_comp, id_comp, idem, sub_self, zero_def]

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
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j : J
⊢ ι F j ≫ map f = (f.app (op j)).app j ≫ ι G j

Tactic:
simp [chosenCoend.map]

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

Goal state before:
pp: 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)

Tactic:
simp only [Hom, comp, Category.assoc]

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

Goal state before:
pp: 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)

Tactic:
simp only [Hom, comp, Category.assoc]

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

Goal state before:
pp: 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)

Tactic:
simp only [Hom, comp, Category.assoc]

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✝)
⊢ (match left a✝³, right a✝¹, left a✝, PUnit.unit, h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    {
      down :=
        f.down ≫
          (match left a✝², right a✝¹, left a✝, g, h with
            | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
            | left _x, left _y, right _z, x, x_1 => PUnit.unit
            | left _x, right _y, right _z, x, x_1 => PUnit.unit
            | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }).down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: 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)

Tactic:
simp only [Hom, comp, Category.assoc]

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

Goal state before:
pp: 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)

Tactic:
simp only [Hom, comp, Category.assoc]

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✝)
⊢ {
      down :=
        (match left a✝³, right a✝², left a✝¹, f, g with
            | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
            | left _x, left _y, right _z, x, x_1 => PUnit.unit
            | left _x, right _y, right _z, x, x_1 => PUnit.unit
            | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }).down ≫
          h.down } =
    match left a✝³, right a✝², left a✝, f,
      match right a✝², left a✝¹, left a✝, g, h with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down } with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }