mathlib-initiative/mathlib-tactics huggingface dataset:
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 (↾_root_.Prod.fst)) (x, y) = x

Tactic:
rfl

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 (↾_root_.Prod.snd)) (x, y) = y

Tactic:
rfl

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 : C
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
j : ι
z : ToType ((Discrete.functor f ⋙ F).obj { as := j })
⊢ (ConcreteCategory.hom (F.map (g j))) z = (ConcreteCategory.hom (s.ι.app { as := j })) z

Tactic:
rfl

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

Goal state before:
pp: case e'_2
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
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) ((ConcreteCategory.hom (F.map u)) b) =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) ((ConcreteCategory.hom (F.map u)) b)

Tactic:
rfl

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

Goal state before:
pp: case convert_2
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
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b = (fiberPerm h b) t

Tactic:
rfl

Goal state after:
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
⊢ (ConcreteCategory.hom ((((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f).app A.obj))
      A.pt =
    (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
rfl

Goal state after:
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 : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom ((↑((Aut.unitsEndEquivAut F).symm f)).app { obj := A, pt := a, isGalois := ⋯ }.obj))
      { obj := A, pt := a, isGalois := ⋯ }.pt =
    (ConcreteCategory.hom (f.hom.app A)) a

Tactic:
rfl

Goal state after:
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
        (F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop { unop' := x })).hom))
      a =
    (ConcreteCategory.hom (F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom)) a

Tactic:
rfl

Goal state after:
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✝ : C
inst✝ : IsConnected X✝
x✝ y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x✝
hx' : x' = (e X✝).symm x✝
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ (ConcreteCategory.hom
        (FintypeCat.equivEquivIso
            ((F.obj Y).uSwitchEquiv.symm.trans
              ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (F.obj Y).uSwitchEquiv))).hom)
      ((ConcreteCategory.hom (F.map f)) x) =
    (F.obj Y).uSwitchEquiv
      ((ConcreteCategory.hom (g'.hom.app Y)) ((F.obj Y).uSwitchEquiv.symm ((ConcreteCategory.hom (F.map f)) x)))

Tactic:
rfl

Goal state after:
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
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).obj
⊢ (Iso.hom 1).app X = 𝟙 (F.obj X)

Tactic:
rfl

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
        ((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) ⟦σ⟧)

Tactic:
rfl

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

Goal state before:
pp: case refl
C : Type u
inst✝ : Category.{v, u} C
x✝ : C
⊢ x✝ = x✝

Tactic:
rfl

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

Goal state before:
pp: G : Type u₁
inst✝ : Groupoid G
⊢ of G ⋙ 𝟭 (FreeGroupoid G) = of G

Tactic:
Functor.comp_id

Goal state after:
G : Type u₁
inst✝ : Groupoid G
⊢ of G = of G
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (HomRel.CompClosure redStep) (Path.reverse p ≫ p) = Quot.mk (HomRel.CompClosure redStep) (𝟙 Y)

Tactic:
by
  nth_rw 2 [← Quiver.Path.reverse_reverse p]
  apply congr_comp_reverse

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)
j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)
a✝ : Aut F
⊢ (ConcreteCategory.hom (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom)
      ((ConcreteCategory.hom u.inv.hom) ⟦a✝⟧) =
    (ConcreteCategory.hom (s.ι.app j).hom) ((ConcreteCategory.hom u.inv.hom) ⟦a✝⟧)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ of C ⋙ 𝟭 (FreeGroupoid C) = 𝟭 C ⋙ of C

Tactic:
rfl

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

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
φ : C ⥤ D
φ' : D ⥤ E
⊢ of C ⋙ map φ ⋙ map φ' = (φ ⋙ φ') ⋙ of E

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Groupoid E
F : C ⥤ D
G : D ⥤ E
⊢ (of C ⋙ map F) ⋙ lift G = F ⋙ G

Tactic:
of_comp_map,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Groupoid E
F : C ⥤ D
G : D ⥤ E
⊢ (F ⋙ of D) ⋙ lift G = F ⋙ G
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
⊢ of V ⋙q (𝟭 (Quiver.FreeGroupoid V)).toPrefunctor = 𝟭q V ⋙q of V

Tactic:
rfl

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

Goal state before:
pp: V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''

Tactic:
rfl

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

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

Tactic:
sInf,

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

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

Tactic:
sInf,

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
⊢ y * (x * y⁻¹) ∈ S.vertexSubgroup cS

Tactic:
exact Sn.conj' y hx

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

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
⊢ Groupoid.inv p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj c✝)}

Tactic:
mem_ofPred,

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
⊢ φ.map (Groupoid.inv p✝) ∈ S.arrows (φ.obj d✝) (φ.obj c✝)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ 𝟙 c ∈ { arrows := fun c d ↦ {f | φ.map f ∈ S.arrows (φ.obj c) (φ.obj d)}, inv := ⋯, mul := ⋯ }.arrows c c

Tactic:
mem_ofPred,

Goal state after:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ φ.map (𝟙 c) ∈ S.arrows (φ.obj c) (φ.obj c)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ (comap φ S).arrows c✝ c✝
⊢ inv f ≫ γ ≫ f ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj d✝)}

Tactic:
mem_ofPred,

Goal state after:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ (comap φ S).arrows c✝ c✝
⊢ φ.map (inv f ≫ γ ≫ f) ∈ S.arrows (φ.obj d✝) (φ.obj d✝)
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inr ≫ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    biprod.inr ≫ 𝟙 (P ⊞ P.complement)

Tactic:
biprod.inr_desc_assoc,

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p = biprod.inr ≫ 𝟙 (P ⊞ P.complement)
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
f : A ⟶ B
i : IsInitial K
t : IsTerminal Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom (t.from X) ↔ HasLiftingProperty f (t.from (L ⟹ X))

Tactic:
hasLiftingProperty_mk_isInitial_iff'

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
f : A ⟶ B
i : IsInitial K
t : IsTerminal Y
⊢ HasLiftingProperty f ((ihom L).map (t.from X)) ↔ HasLiftingProperty f (t.from (L ⟹ X))
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
hm : ∀ (j : α), { f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
⊢ { f := fun i a ↦ (s.proj a).f i, φ := φ }.f i =
    { f := fun i a ↦ (s.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (s.proj a).φ i }.f i

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
x✝ : (monoFactorisation f).I.obj X
⊢ (ConcreteCategory.hom (f.app Y)) (Exists.choose ⋯) =
    (ConcreteCategory.hom (G.map g)) ((ConcreteCategory.hom (f.app X)) (Exists.choose ⋯))

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
x✝¹ : C
x✝ : (monoFactorisation f).I.obj x✝¹
⊢ (ConcreteCategory.hom (f.app x✝¹)) (Exists.choose ⋯) = ↑x✝

Tactic:
grind

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

Goal state before:
pp: case 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 F' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
x y : D
f : x ⟶ y
⊢ (F.map ((inclRight C D).map f) ≫
      match (inclRight C D).obj y with
      | left x => αₗ.app x
      | right x => αᵣ.app x) =
    (match (inclRight C D).obj x with
      | left x => αₗ.app x
      | right x => αᵣ.app x) ≫
      F'.map ((inclRight C D).map f)

Tactic:
| @right x y f =>

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

Goal state before:
pp: case left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α β : F ⟶ F'
h₁ : (inclLeft C D).whiskerLeft α = (inclLeft C D).whiskerLeft β
h₂ : (inclRight C D).whiskerLeft α = (inclRight C D).whiskerLeft β
t : C
⊢ α.app (left t) = β.app (left t)

Tactic:
exact congrArg (fun x ↦ x.app t) h₁

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f : X.I → Y.I
F : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F }.φ i ≫ eqToHom ⋯ = { f := f, φ := F }.φ i
⊢ { f := f, φ := F } = { f := f, φ := F }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: case e'_3
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ (m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd) = ↑((homPullbackEquiv f g pb hpb s.pt).1 m)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
f : Y ⟶ h.pullback
f_p₁ : f ≫ h.p₁ = g₁
f_p₂ : f ≫ h.p₂ = g₂
f_p✝¹ : f ≫ h.p = b
f'_p₁ : f ≫ h.p₁ = g₁
f'_p₂ : f ≫ h.p₂ = g₂
f_p✝ : f ≫ h.p = b
⊢ { f := f, f_p₁ := f_p₁, f_p₂ := f_p₂, f_p := f_p✝¹ } = { f := f, f_p₁ := f'_p₁, f_p₂ := f'_p₂, f_p := f_p✝ }

Tactic:
rfl

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

Goal state before:
pp: case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : m < n + 1
⊢ M m = M m

pp: case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m

Tactic:
rfl

Goal state after:
case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case refine_2
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ M m = M m

Tactic:
rfl

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

Goal state before:
pp: case refine_3
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = N m

Tactic:
rfl

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

Goal state before:
pp: case refine_4
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ N m = N m

Tactic:
rfl

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

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
f : Over F.op
⊢ { app := fun X ↦ (f.hom.app (Opposite.op X)).unop, naturality := ⋯ }.Coequifibered ↔
    Coequifibered (NatTrans.unop f.hom)

Tactic:
rfl

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

Goal state before:
pp: case refl
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
f : X ⟶ yp
⊢ f = f

Tactic:
rfl

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

Goal state before:
pp: 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))
m : s.pt ⟶ (cone f).pt
h : ∀ (j : ℕᵒᵖ), m ≫ (cone f).π.app j = s.π.app j
n : ℕ
⊢ m ≫ Pi.π M n =
    (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      Pi.π M n

Tactic:
simp only [dite_eq_ite, limit.lift_π,
      Fan.mk_π_app, ← h ⟨n + 1⟩, Category.assoc]

Goal state after:
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))
m : s.pt ⟶ (cone f).pt
h : ∀ (j : ℕᵒᵖ), m ≫ (cone f).π.app j = s.π.app j
n : ℕ
⊢ m ≫ Pi.π M n = m ≫ (cone f).π.app (Opposite.op (n + 1)) ≫ Pi.π (fun i ↦ if i < n + 1 then M i else N i) n ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝² : Category.{v₄, u₄} A'
inst✝¹ : Category.{v₅, u₅} B'
inst✝ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ = θ'

Tactic:
by
  apply CatCospanTransformMorphism.ext <;> assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
K : Type u_2
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F✝ : J ⥤ C
D : Type u_4
inst✝¹ : Category.{v_4, u_4} D
G : K ⥤ D
F : J ⥤ C
inst✝ : HasWeakLimit F
j : J
⊢ F.obj j = F.obj j

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (bifunctorComp₁₂ (curriedTensor C) (curriedTensor C)).flip = bifunctorComp₁₂ (curriedTensor C).flip (curriedTensor C)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)).flip =
    (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C).flip).flip.flip₁₃

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ bifunctorComp₁₂ (curriedTensor C) (curriedTensor C) =
    (bifunctorComp₂₃ (curriedTensor C).flip (curriedTensor C)).flip.flip₂₃

Tactic:
rfl

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

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
inst✝ : BraidedCategory C
X Y : C
⊢ ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                  (tensorBifunctor L W ε)).hom.app
            X).app
        Y ≫
      L'.map (β_ X Y).hom ≫
        ((Lifting₂.iso L' L' W W ((curriedTensor C).flip ⋙ (whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                    (tensorBifunctor L W ε).flip).inv.app
              X).app
          Y =
    LaxMonoidal.μ L' X Y ≫ L'.map (β_ X Y).hom ≫ OplaxMonoidal.δ L' Y X

Tactic:
rfl

Goal state after: