mathlib-initiative/mathlib-tactics huggingface dataset:
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.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
⊢ z ≫ (L.objObjPreimageIso W).inv = 0

Tactic:
hφ,

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
⊢ φ.map L ⋯ = 0
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
⊢ ∀ (X Y Z : C ⥤ D) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g

Tactic:
intros
    ext
    apply comp_smul

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V

Tactic:
← comp_hom,

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ (f.hom ≫ f.inv).hom = 𝟙 M.V
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V

Tactic:
← comp_hom,

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ (f.inv ≫ f.hom).hom = 𝟙 N.V
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
x✝ : CV X✝.V
⊢ (⇑(ConcreteCategory.hom f.hom) ∘ ⇑(ConcreteCategory.hom (X✝.ρ g))) x✝ =
    (⇑(ConcreteCategory.hom (Y✝.ρ g)) ∘ ⇑(ConcreteCategory.hom f.hom)) x✝

Tactic:
simpa using CategoryTheory.congr_fun (f.2 g) _

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

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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X)))) ≫
        (R ⋙ U).map f ≫ adj₂.unit.app ((R ⋙ U).obj Y) ≫ (R ⋙ U).map (adj₂.counit.app Y) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj ((𝟭 B).obj X)) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f

Tactic:
adj₂.right_triangle_components,

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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X)))) ≫ (R ⋙ U).map f ≫ 𝟙 ((R ⋙ U).obj Y) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj ((𝟭 B).obj X)) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.id
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.id f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| id =>

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case id
B : Type u
inst✝ : Quiver B
b c a✝ a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (Hom.id a✝)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.id a✝))

Tactic:
| id =>

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso } =
    { iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso } ≫ { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso }

Tactic:
by
    ext
    simp [Equiv.toIso, EquivFunctor.map_trans']

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X : Dial C
⊢ (tensorUnitImpl.tensorObjImpl X).rel =
    (Subobject.pullback (prod.map (Limits.prod.leftUnitor X.src).hom (Limits.prod.leftUnitor X.tgt).hom)).obj X.rel

Tactic:
simp [Subobject.pullback_top]

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X : Dial C
⊢ (X.tensorObjImpl tensorUnitImpl).rel =
    (Subobject.pullback (prod.map (Limits.prod.rightUnitor X.src).hom (Limits.prod.rightUnitor X.tgt).hom)).obj X.rel

Tactic:
simp [Subobject.pullback_top]

Goal state after:
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 ▷ X ≫ (∂R X Y Z).inv = coprod.inl

Tactic:
apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp

Goal state after:
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 ▷ X ≫ (∂R X Y Z).inv) ≫ (∂R X Y Z).hom = coprod.inl ≫ (∂R X Y Z).hom
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.inr ▷ X ≫ (∂R X Y Z).inv = coprod.inr

Tactic:
apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ (coprod.inr ▷ X ≫ (∂R X Y Z).inv) ≫ (∂R X Y Z).hom = coprod.inr ≫ (∂R X Y Z).hom
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✝ : MonoidalClosed C
X Y Z : C
⊢ (∂L X Y Z).inv = uncurry (coprod.desc (curry coprod.inl) (curry coprod.inr))

Tactic:
rw [← curry_eq_iff]

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ curry (∂L X Y Z).inv = coprod.desc (curry coprod.inl) (curry coprod.inr)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_1
𝒮 : 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 g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ) ≫ φ = τ

Tactic:
apply IsStronglyCartesian.ext p g ψ (h ≫ f) (by simp)

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst✝ : p.IsHomLift f' φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
by
  subst_hom_lift p f' φ'; clear a b R S
  have : p.IsHomLift (f ≫ g) φ' := (hf' ▸ inferInstance)
  apply IsStronglyCocartesian.universal_property' f

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

Goal state before:
pp: case mpr
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
⊢ LF.IsRightKanExtension α → LF.IsLeftDerivedFunctor α W

Tactic:
exact fun h => ⟨h⟩

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : (F' ⋙ G').map (α.app X₁) ≫ ε.app ((G ⋙ L₂).obj X₁) = ε.app ((L₁ ⋙ G').obj X₁) ≫ (𝟭 D₂).map (α.app X₁)
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁

Tactic:
have eq₂ := G'.congr_map (hη X₁)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₁ : C₁
eq₁ : (F' ⋙ G').map (α.app X₁) ≫ ε.app ((G ⋙ L₂).obj X₁) = ε.app ((L₁ ⋙ G').obj X₁) ≫ (𝟭 D₂).map (α.app X₁)
eq₂ : G'.map (η.app (L₁.obj X₁) ≫ F'.map (α.app X₁)) = G'.map (L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁))
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯) ≫
      bc.fst ≫ c₁.proj val✝ =
    s.proj (Sum.inl val✝)

Tactic:
erw [← Category.assoc, h.fac]

Goal state after:
case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯).π.app
        { as := WalkingPair.left } ≫
      c₁.proj val✝ =
    s.proj (Sum.inl val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯) ≫
      bc.snd ≫ c₂.proj val✝ =
    s.proj (Sum.inr val✝)

Tactic:
erw [← Category.assoc, h.fac]

Goal state after:
case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯).π.app
        { as := WalkingPair.right } ≫
      c₂.proj val✝ =
    s.proj (Sum.inr val✝)
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 : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝¹ : IsConnected A
inst✝ : Mono u
b : (F.obj A).obj
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) b = a

Tactic:
apply connected_component_unique F b a u (selfProdPermIncl h b)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
inst✝³ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝² : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝¹ : IsConnected A
inst✝ : Mono u
b : (F.obj A).obj
⊢ (ConcreteCategory.hom (F.map u)) b = (ConcreteCategory.hom (F.map (selfProdPermIncl h b))) a
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ X ∈ ⋃ X, Set.range (ff X), IsConnected X

pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ (σ : Aut F), (∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U

Tactic:
· rintro X ⟨A, ⟨Y, rfl⟩, hA2⟩
    obtain ⟨i, rfl⟩ := hA2
    exact h5 Y i

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ (σ : Aut F), (∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
⊢ Function.Injective ⇑(toAut F G)

Tactic:
by
  rw [← MonoidHom.ker_eq_bot_iff, eq_bot_iff]
  intro g (hg : toAut F G g = 1)
  refine h g (fun X x ↦ ?_)
  have : (toAut F G g).hom.app X = 𝟙 (F.obj X) := by
    rw [hg]
    rfl
  rw [← toAut_hom_app_apply, this, FintypeCat.id_apply]

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

Goal state before:
pp: case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
g σ : Aut F
this :
  ((functorToAction F).obj A).ρ g ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom =
    (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom ≫ s.pt.ρ g
⊢ (ConcreteCategory.hom
        (((ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))).ρ g ≫ u.inv.hom) ≫
          (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom))
      ⟦σ⟧ =
    (ConcreteCategory.hom (((functorToAction F).obj A).ρ g ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom))
      ((ConcreteCategory.hom u.inv.hom) ⟦σ⟧)

Tactic:
u.inv.comm g

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
g σ : Aut F
this :
  ((functorToAction F).obj A).ρ g ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom =
    (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom ≫ s.pt.ρ g
⊢ (ConcreteCategory.hom
        ((u.inv.hom ≫ ((functorToAction F).obj A).ρ g) ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom))
      ⟦σ⟧ =
    (ConcreteCategory.hom (((functorToAction F).obj A).ρ g ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom))
      ((ConcreteCategory.hom u.inv.hom) ⟦σ⟧)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)

Tactic:
· exact ih

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ (c d : ↑S.objs), Function.Injective fun f ↦ S.hom.map f

Tactic:
by
  rintro ⟨c, hc⟩ ⟨d, hd⟩ ⟨f, hf⟩ ⟨g, hg⟩ hfg; exact Subtype.ext hfg

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
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
⊢ f = g

Tactic:
apply (ChosenCoendsOfShape.isCoend F).hom_ext

Goal state after:
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
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
⊢ ∀ (j : WalkingMultispan (multispanShapeCoend J)),
    (ChosenCoendsOfShape.cowedge F).ι.app j ≫ f = (ChosenCoendsOfShape.cowedge F).ι.app j ≫ g
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case edge.right
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 : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c✝ : C
d✝ y✝ : D
f✝ : d✝ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      (edge c✝ d✝ ≫ (inclRight C D).map f✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (edge c✝ d✝) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝)

Tactic:
· case edge.right c _ _ f => simpa using! α.naturality <| (Prod.sectR c _).map f

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Deterministic (f ≫ inv f)

Tactic:
rw [IsIso.hom_inv_id]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Deterministic (𝟙 X)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ sectionsUncurry (sectionsCurry u) = u

Tactic:
by
  dsimp [sectionsCurry, sectionsUncurry]
  ext
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Transported e
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp +instances [Transported.instBraidedCategory, BraidedCategory.ofFaithful,
      fromInducedCoreMonoidal, Functor.CoreMonoidal.toLaxMonoidal]

Goal state after: