mathlib-initiative/mathlib-tactics huggingface dataset:
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.V ≅ N.V
comm : ∀ (g : G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g
g : G
w : M.ρ g = f.hom ≫ N.ρ g ≫ f.inv
⊢ N.ρ g ≫ f.inv = f.inv ≫ M.ρ g

Tactic:
simp [w]

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
inst✝ : HasFiniteLimits V
⊢ autoParam
    (∀ (J : Type) [inst : SmallCategory J] [FinCategory J],
      PreservesLimitsOfShape J ((evaluation (SingleObj G) V).obj (SingleObj.star G)))
    PreservesFiniteLimits.preservesFiniteLimits._autoParam

Tactic:
intro _

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteLimits V
J✝ : Type
⊢ ∀ [inst : SmallCategory J✝] [FinCategory J✝],
    PreservesLimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))
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
inst✝ : HasFiniteColimits V
⊢ autoParam
    (∀ (J : Type) [inst : SmallCategory J] [FinCategory J],
      PreservesColimitsOfShape J ((evaluation (SingleObj G) V).obj (SingleObj.star G)))
    PreservesFiniteColimits.preservesFiniteColimits._autoParam

Tactic:
intro _

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteColimits V
J✝ : Type
⊢ ∀ [inst : SmallCategory J✝] [FinCategory J✝],
    PreservesColimitsOfShape J✝ ((evaluation (SingleObj G) V).obj (SingleObj.star G))
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
this : Abelian D := abelian L P
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L

Tactic:
intro _

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
this : Abelian D := abelian L P
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), PreservesLimit (parallelPair f 0) L
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
this : Abelian D := abelian L P
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L

Tactic:
intro _

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
this : Abelian D := abelian L P
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), PreservesColimit (parallelPair f 0) L
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

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

Tactic:
intro _

Goal state after:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Mono (η.app c)
⊢ Mono η
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)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ F.map (adj₁.unit.app (L.obj Y) ≫ U.map g) = g ≫ F.map (adj₁.unit.app X) ↔
    (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.homEquiv (L.obj Y) (F.obj X)) g ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
rw [← (adj₁.homEquiv _ _).injective.eq_iff, adj₁.homEquiv_unit,
        adj₁.homEquiv_unit, adj₁.homEquiv_unit, eq_comm]

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)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) =
      adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) ↔
    (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ adj₁.unit.app (U.obj (F.obj X))
Module: Mathlib.CategoryTheory.Bicategory.Coherence

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

Tactic:
dsimp
    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
    simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
x : B
h : x ⟶ c
X✝ Y✝ : RightLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ η.left) ▷ f ≫ (Y✝.whisker h).counit = (X✝.whisker h).counit

Tactic:
by
    dsimp only [whisker_lift, whisker_counit]
    rw [← RightLift.w η]
    simp [-RightLift.w]

Goal state after:
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 g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv

Tactic:
intro _

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a : B
⊢ (α.naturality (𝟙 a)).inv =
    α.app a ◁ (G.mapId a).hom ≫ (ρ_ (α.app a)).hom ≫ (λ_ (α.app a)).inv ≫ (F.mapId a).inv ▷ α.app a

Tactic:
by
  simp [naturality_id_iso]

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
⊢ ∀ {a b : B} (f : a ⟶ b),
    (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom

Tactic:
intro a b f

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
    ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
⊢ ∀ {a b : B} (f : a ⟶ b),
    (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom

Tactic:
intro a b f

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
    ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
⊢ ∀ {a b : B} (f : a ⟶ b),
    F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom ≫ (η ≫ θ ≫ ι).naturality f =
      ((η ≫ θ) ≫ ι).naturality f ≫ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f

Tactic:
intro a b f

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom ≫ (η ≫ θ ≫ ι).naturality f =
    ((η ≫ θ) ≫ ι).naturality f ≫ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
⊢ (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)).Final

Tactic:
let x := (sB.inverse ⋙ R ⋙ sT.functor).obj b

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
⊢ (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)).Final
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₂.IsInvertedBy (prodLift₁ F hF).flip

Tactic:
intro _

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
X✝ : C₂
⊢ ∀ ⦃Y : C₂⦄ (f : X✝ ⟶ Y), W₂ f → IsIso ((prodLift₁ F hF).flip.map f)
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 : C
⊢ (ρ_ (L'.obj X)).hom = L'.obj X ◁ (ε' L W ε).inv ≫ (μ L W ε X (𝟙_ C)).hom ≫ L'.map (ρ_ X).hom

Tactic:
dsimp +instances [monoidalCategoryStruct, rightUnitor]
  rw [liftNatTrans_app]
  dsimp
  rw [assoc]
  change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _
  simp only [comp_id]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒴.p.IsHomLift f (F.map φ)
⊢ 𝒳.p.IsHomLift f φ

Tactic:
by
  apply of_fac 𝒳.p f φ (F.w_obj a ▸ domain_eq 𝒴.p f (F.map φ))
    (F.w_obj b ▸ codomain_eq 𝒴.p f (F.map φ))
  simp [congr_hom F.w.symm, fac 𝒴.p f (F.map φ)]

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

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ (homCartesianLift f g φ' ≫ cartesianLift a f).fiber = φ'.fiber ≫ eqToHom ⋯

Tactic:
by simp [← Cat.Hom₂.comp_app]

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun b ↦
    (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
            ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b })).asEquivalence.trans
      (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b }))).asEquivalence.symm
⊢ IsFiltered A

Tactic:
have : ∀ b, IsFiltered (CostructuredArrow _ ((sB.inverse ⋙ R ⋙ sT.functor).obj b)) :=
    fun b => IsFiltered.of_equivalence (sC b.1).symm

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun b ↦
    (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
            ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b })).asEquivalence.trans
      (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b }))).asEquivalence.symm
this :
  ∀ (b : AsSmall B), IsFiltered (CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
⊢ IsFiltered A
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: X Y : FintypeCat
f : X ⟶ Y
⊢ FintypeCat

Tactic:
by
  haveI : Fintype (↑(Set.range f)ᶜ) := Fintype.ofFinite _
  exact FintypeCat.of (↑(Set.range 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
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : ¬Nat.card (F.obj X).obj < Nat.card (F.obj Y).obj
⊢ Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj

Tactic:
simp only [not_lt] at hlt

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : Nat.card (F.obj Y).obj ≤ Nat.card (F.obj X).obj
⊢ Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
X : C
inst✝ : IsConnected X
⊢ (∀ (i : Unit), IsConnected ((fun x ↦ X) i)) ∧ Finite Unit

Tactic:
exact ⟨fun _ ↦ inferInstance, inferInstance⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsGalois A
a b : (F.obj A).obj
⊢ (ConcreteCategory.hom (F.map ((evaluationEquivOfIsGalois F A a).symm b).hom)) a = b

Tactic:
change (evaluationEquivOfIsGalois F A a) _ = _

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsGalois A
a b : (F.obj A).obj
⊢ (evaluationEquivOfIsGalois F A a) ((evaluationEquivOfIsGalois F A a).symm b) = b
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h.right
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
refine ⟨evaluation_injective_of_isConnected F A X a, ?_⟩
    intro x
    use u ≫ Pi.π _ x
    exact (selfProdProj_fiber h1) x

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
H : Set (Aut F)
h1 : 1 ∈ H
h : IsOpen H
⊢ ∃ I x, (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ H

Tactic:
obtain ⟨U, hUopen, rfl⟩ := isOpen_induced_iff.mp h

Goal state after:
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 x,
    (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U
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
f : End F
A : PointedGaloisObject F
⊢ ↑((endEquivSectionsFibers F) f) A = (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
dsimp [endEquivSectionsFibers, Types.sectionsEquiv]
  erw [Types.limitEquivSections_apply, colimitCoyonedaHomIsoLimit'_π_apply]
  change (((FullyFaithful.whiskeringRight (FullyFaithful.ofFullyFaithful
      FintypeCat.incl) C).homEquiv) f).app A
    (((colimit.ι _ _) ≫ (colimit.isoColimitCocone ⟨cocone F, isColimit F⟩).hom).app
      A _) = f.app A A.pt
  simp
  rfl

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

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

Tactic:
· rintro ⟨c, ⟨γ, γS⟩, rfl⟩
    exact ⟨φ.map γ, ⟨γ, γS⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
h₂ : x✝¹ ≫ h.p₂₃ = x✝ ≫ h.p₂₃
⊢ x✝¹ ≫ h.p₂ = x✝ ≫ h.p₂

Tactic:
by simpa using h₂ =≫ h₂₃.p₁

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
⊢ functorMap f n ≫
      (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m

Tactic:
have h₁ : (if _ : m < m + 1 then M m else N m) = if _ : m < n then M m else N m := by
          rw [dif_pos (by lia), dif_pos (by lia)]

Goal state after:
case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
⊢ functorMap f n ≫
      (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
x : P.obj c.pt
x✝ : Jᵒᵖ
⊢ (shrinkYoneda.{w, v, u}.mapCocone (coconeLeftOpOfCone c)).ι.app x✝ ≫ shrinkYonedaEquiv.symm x =
    c'.ι.app x✝ ≫
      hc'.desc
        { pt := P,
          ι :=
            { app := fun j ↦ shrinkYonedaEquiv.symm (↑(Types.sectionOfCone (P.mapCone c) x) (unop j)),
              naturality := ⋯ } }

Tactic:
hc'.fac

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
x : P.obj c.pt
x✝ : Jᵒᵖ
⊢ (shrinkYoneda.{w, v, u}.mapCocone (coconeLeftOpOfCone c)).ι.app x✝ ≫ shrinkYonedaEquiv.symm x =
    { pt := P,
            ι :=
              { app := fun j ↦ shrinkYonedaEquiv.symm (↑(Types.sectionOfCone (P.mapCone c) x) (unop j)),
                naturality := ⋯ } }.ι.app
      x✝