mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case c
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ Cone (parallelPair f 0 ⋙ P.ι)

pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ IsLimit ?c

pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P (Cone.pt ?c)

Tactic:
· exact (Cone.postcompose (Iso.symm (diagramIsoParallelPair _)).hom).obj
      (Fork.ofι (kernel.ι f.hom) (by simp))

Goal state after:
case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ IsLimit
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯))

case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯)).pt
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.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
l : L.obj (cokernel f) ⟶ L.obj φ.Y'
hl : L.map (cokernel.π f) ≫ l = L.map φ.f
⊢ L.map (cokernel.π f) ≫ l ≫ inv (L.map φ.s) ≫ (L.objObjPreimageIso W).hom = w

Tactic:
simp [reassoc_of% hl, ← hφ]

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

Goal state before:
pp: case refine_1
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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ F.map (U.map (h X).right) ≫ adj₁.counit.app ((U ⋙ F).obj X) ≫ s.π = adj₁.counit.app (h X).W ≫ (h X).right ≫ s.π

Tactic:
← adj₁.counit_naturality_assoc (h X).right

Goal state after:
case refine_1
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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ F.map (U.map (h X).right) ≫ adj₁.counit.app ((U ⋙ F).obj X) ≫ s.π =
    F.map (U.map (h X).right) ≫ adj₁.counit.app ((U ⋙ F).obj X) ≫ s.π
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
g : G
⊢ (𝟙_ (Action W G)).ρ g ≫ ε F = ε F ≫ ((F.mapAction G).obj (𝟙_ (Action V G))).ρ g

Tactic:
dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
g : G
⊢ 𝟙 (𝟙_ W) ≫ ε F = ε F ≫ F.map (𝟙 (𝟙_ V))
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
g : G
⊢ ((F.mapAction G).obj (𝟙_ (Action V G))).ρ g ≫ η F = η F ≫ (𝟙_ (Action W G)).ρ g

Tactic:
dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
g : G
⊢ F.map (𝟙 (𝟙_ V)) ≫ η F = η F ≫ 𝟙 (𝟙_ W)
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: case mp
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
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
h : IsIso t.adj₁.unit
⊢ IsIso t.adj₂.counit

Tactic:
let idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm

Goal state after:
case mp
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
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
h : IsIso t.adj₁.unit
idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm
⊢ IsIso t.adj₂.counit
Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
x✝⁶ x✝⁵ x✝⁴ : InducedBicategory C F
x✝³ x✝² : x✝⁶ ⟶ x✝⁵
x✝¹ x✝ : x✝⁵ ⟶ x✝⁴
η : x✝³ ⟶ x✝²
θ : x✝¹ ⟶ x✝
⊢ mkHom₂ (x✝³.hom ◁ θ.hom) ≫ mkHom₂ (η.hom ▷ x✝.hom) = mkHom₂ (η.hom ▷ x✝¹.hom) ≫ mkHom₂ (x✝².hom ◁ θ.hom)

Tactic:
by ext; simpa using whisker_exchange _ _

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = σs'.unit

Tactic:
dsimp only [StructuredArrow.mk_hom_eq_self, σs']

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

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ Category.{?u.8, u + 1} (KleisliCat m)

Tactic:
refine { id_comp := ?_, comp_id := ?_, assoc := ?_ } <;> intros <;>
  ext

Goal state after:
case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (𝟙 X✝ ≫ f✝) x✝ = f✝ x✝

case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (f✝ ≫ 𝟙 Y✝) x✝ = f✝ x✝

case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
x✝ : W✝
⊢ ((f✝ ≫ g✝) ≫ h✝) x✝ = (f✝ ≫ g✝ ≫ h✝) x✝
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X Y : ↑s.pt
f : X ⟶ Y
⊢ (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.map f = eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯

Tactic:
dsimp [limitConeLift]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X Y : ↑s.pt
f : X ⟶ Y
⊢ (hom
        (limit.π
          (homDiagram
            ((hom
                (limit.lift (F ⋙ objects)
                  { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
              X)
            ((hom
                (limit.lift (F ⋙ objects)
                  { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
              Y))
          j))
      (Types.Limit.mk
        (homDiagram
          ((hom
              (limit.lift (F ⋙ objects)
                { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
            X)
          ((hom
              (limit.lift (F ⋙ objects)
                { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
            Y))
        (fun j ↦ eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) ⋯) =
    eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
Y : Over X
⊢ (mapPullbackAdj (𝟙 X)).unit.app Y ≫ (pullbackId X).hom.app ((map (𝟙 X)).obj Y) = (mapPullbackAdj (𝟙 X)).unit.app Y

Tactic:
pullbackId,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
Y : Over X
⊢ (mapPullbackAdj (𝟙 X)).unit.app Y ≫
      ((mapPullbackAdj (𝟙 X)).rightAdjointUniq (mapPullbackAdj (𝟙 X))).hom.app ((map (𝟙 X)).obj Y) =
    (mapPullbackAdj (𝟙 X)).unit.app Y
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

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

Tactic:
pullbackId,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
⊢ (mapPullbackAdj (𝟙 X)).unit ≫
      (map (𝟙 X)).whiskerLeft ((mapPullbackAdj (𝟙 X)).rightAdjointUniq (mapPullbackAdj (𝟙 X))).hom =
    (mapPullbackAdj (𝟙 X)).unit
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:
pullbackId,

Goal state after:
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 ((mapPullbackAdj (𝟙 X)).rightAdjointUniq (mapPullbackAdj (𝟙 X))).hom (map (𝟙 X)) ≫
      (mapPullbackAdj (𝟙 X)).counit =
    (mapPullbackAdj (𝟙 X)).counit
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
val✝ : A
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inl val✝)) =
    𝟙
      (match inl val✝ with
      | inl X => F.obj X
      | inr X => G.obj X)

Tactic:
simp only [← map_id]; rfl

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

Goal state before:
pp: case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
val✝ : B
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (𝟙 (inr val✝)) =
    𝟙
      (match inr val✝ with
      | inl X => F.obj X
      | inr X => G.obj X)

Tactic:
simp only [← map_id]; rfl

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

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ B
G : C ⥤ D
a a' : A
f : a ⟶ a'
⊢ (F.sum G).map ((Sum.inl_ A C).map f) = (Sum.inl_ B D).map (F.map f)

Tactic:
simp [sum]

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

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ B
G : C ⥤ D
c c' : C
f : c ⟶ c'
⊢ (F.sum G).map ((Sum.inr_ A C).map f) = (Sum.inr_ B D).map (G.map f)

Tactic:
simp [sum]

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
hab : a = b
S : 𝒮
hS : p.obj b = S
⊢ p.IsHomLift (𝟙 S) (eqToHom hab)

Tactic:
subst hS hab

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)
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₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j : J
⊢ lift s ≫ (coneFunctorEnrichedHom V F₁ F₂).π.app j = s.π.app j

Tactic:
dsimp [coneFunctorEnrichedHom]
  ext k
  have := s.w k.hom
  dsimp at this
  -- this was produced by `simp? [lift, ← this]`
  simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, lift, functorEnrichedHom_obj,
    assoc, end_.lift_π, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
    eHomWhiskerLeft_id, comp_id, ← this, Under.map_obj_right, Under.mk_right]
  congr
  simp [Under.map, Comma.mapLeft]
  rfl

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
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ (ConcreteCategory.hom (Y.ρ g⁻¹ * Y.ρ g).hom) ↑y = ↑y

Tactic:
by
          simp [← map_mul, inv_mul_cancel, Action.ρ_one, FintypeCat.id_hom]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A X : C
inst✝ : IsConnected A
F : C ⥤ FintypeCat := ⋯
a : (F.obj A).obj
⊢ Function.Injective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
exact evaluation_injective_of_isConnected F A X a

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
hn2 : Nat.card (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
⊢ ∃ x, (∀ (i : ι₁ ⊕ ι₂), IsConnected (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)

Tactic:
use Cofan.combPairIsColimit hc₁ hc₂ c

Goal state after:
case h
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) := ⋯
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
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
⊢ (∀ (i : ι₁ ⊕ ι₂), IsConnected (Sum.elim f₁ f₂ i)) ∧ Finite (ι₁ ⊕ ι₂)
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h.inl
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
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
val✝ : ι₁
⊢ IsConnected (Sum.elim f₁ f₂ (Sum.inl val✝))

pp: case h.inr
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
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
val✝ : ι₂
⊢ IsConnected (Sum.elim f₁ f₂ (Sum.inr val✝))

Tactic:
· exact hf₁ _

Goal state after:
case h.inr
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
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
val✝ : ι₂
⊢ IsConnected (Sum.elim f₁ f₂ (Sum.inr val✝))
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 : AutGalois F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom (((autMulEquivAutGalois F).symm { unop' := x }).hom.app A)) a =
    (ConcreteCategory.hom (F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom)) a

Tactic:
by
  rw [← autMulEquivAutGalois_π, MulEquiv.apply_symm_apply]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
⊢ (Over.forget (F.obj X)).map
        (Over.homMk
          (prod.lift
              (have this := W.hom;
              this)
              g ≫
            inv (prodComparison F X Z))
          ⋯) ≫
      (TwoSquare.overPost F X).app (Over.mk prod.fst) ≫ F.map prod.snd =
    g

Tactic:
simp [inv_prodComparison_map_snd]

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

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f →
    ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
rintro ⟨g, hg⟩

Goal state after:
case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
g : c✝ ⟶ d✝
hg : g ∈ S.arrows c✝ d✝
⊢ ∃ a b g_1,
    ∃ (ha : φ.obj a = φ.obj c✝) (hb : φ.obj b = φ.obj d✝) (_ : g_1 ∈ S.arrows a b),
      φ.map g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
X✝ Y✝ Z✝ : FormalCoproduct C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ powerMap (x✝¹ ≫ x✝) (ToType (Opposite.unop x)), naturality := ⋯ } =
    { app := fun x ↦ powerMap x✝¹ (ToType (Opposite.unop x)), naturality := ⋯ } ≫
      { app := fun x ↦ powerMap x✝ (ToType (Opposite.unop x)), naturality := ⋯ }

Tactic:
by ext : 1; simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ ((Prod.fst C D).isoWhiskerLeft eₗ).inv ≫ whiskerRight (edgeTransform C D) F =
    whiskerRight (edgeTransform C D) G ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).inv

Tactic:
Iso.inv_comp_eq,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ whiskerRight (edgeTransform C D) F =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).inv
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : FormalCoproduct C
i : X.I
⊢ Sigma.ι X.toFun i ≫ X.coproductIsoSelf.hom = Hom.fromIncl i (𝟙 (X.obj i))

Tactic:
by
  simp [coproductIsoSelf]

Goal state after: