mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
            (α.app { as := c.base }).toFunctor.map (f ≫ g).fiber }.base =
    ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫ (α.app { as := b.base }).toFunctor.map f.fiber } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              (α.app { as := c.base }).toFunctor.map g.fiber }).base

pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ eqToHom ⋯ ≫
      { base := (f ≫ g).base,
          fiber :=
            (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
              (α.app { as := c.base }).toFunctor.map (f ≫ g).fiber }.fiber =
    ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫ (α.app { as := b.base }).toFunctor.map f.fiber } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              (α.app { as := c.base }).toFunctor.map g.fiber }).fiber

Tactic:
· dsimp

Goal state after:
case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ eqToHom ⋯ ≫
      { base := (f ≫ g).base,
          fiber :=
            (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
              (α.app { as := c.base }).toFunctor.map (f ≫ g).fiber }.fiber =
    ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫ (α.app { as := b.base }).toFunctor.map f.fiber } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              (α.app { as := c.base }).toFunctor.map g.fiber }).fiber
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := (𝟙 a).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
            (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber }.base =
    (𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }).base

pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := (𝟙 a).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
            (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber }.fiber =
    (𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }).fiber ≫ eqToHom ⋯

Tactic:
· dsimp

Goal state after:
case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := (𝟙 a).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
            (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber }.fiber =
    (𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }).fiber ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.base =
    ({ base := f.base,
          fiber :=
            (α.app { as := op a.base }).toFunctor.map f.fiber ≫
              (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
        { base := g.base,
          fiber :=
            (α.app { as := op b.base }).toFunctor.map g.fiber ≫
              (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).base

pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.fiber =
    ({ base := f.base,
            fiber :=
              (α.app { as := op a.base }).toFunctor.map f.fiber ≫
                (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
          { base := g.base,
            fiber :=
              (α.app { as := op b.base }).toFunctor.map g.fiber ≫
                (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).fiber ≫
      eqToHom ⋯

Tactic:
· dsimp

Goal state after:
case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.fiber =
    ({ base := f.base,
            fiber :=
              (α.app { as := op a.base }).toFunctor.map f.fiber ≫
                (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
          { base := g.base,
            fiber :=
              (α.app { as := op b.base }).toFunctor.map g.fiber ≫
                (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).fiber ≫
      eqToHom ⋯
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Core C
f g : X ⟶ Y
h : f.iso.hom = g.iso.hom
⊢ f.iso = g.iso

Tactic:
exact Iso.ext h

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
⊢ f.preimage Set.univ = f.Dom

Tactic:
ext; simp [mem_preimage, mem_dom]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [Category.assoc, Hom.mk.injEq, true_and]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : FinitaryPreExtensive C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
inst✝² : FinitaryPreExtensive D
F : C ⥤ D
inst✝¹ : PreservesFiniteCoproducts F
inst✝ : F.ReflectsEffectiveEpis
α : Type
x✝ : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily (fun a ↦ F.obj (X a)) fun a ↦ F.map (π a)
⊢ EffectiveEpiFamily X π

Tactic:
simp only [← effectiveEpi_desc_iff_effectiveEpiFamily]
    apply F.effectiveEpi_of_map
    convert!
      (inferInstance :
        EffectiveEpi (inv (sigmaComparison F X) ≫ (Sigma.desc (fun a ↦ F.map (π a)))))
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
inst✝³ : BraidedCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u
inst✝¹ : Category.{v, u} D
inst✝ : EnrichedOrdinaryCategory V D
X✝ Y✝ Z✝ : Dᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Quiver.Hom.opEquiv.symm.trans homEquiv) (f ≫ g) =
    (λ_ (𝟙_ V)).inv ≫
      ((Quiver.Hom.opEquiv.symm.trans homEquiv) f ⊗ₘ (Quiver.Hom.opEquiv.symm.trans homEquiv) g) ≫ eComp V X✝ Y✝ Z✝

Tactic:
simp only [tensorHom_eComp_op_eq, leftUnitor_inv_braiding_assoc, ← unitors_inv_equal]

Goal state after:
V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
inst✝³ : BraidedCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u
inst✝¹ : Category.{v, u} D
inst✝ : EnrichedOrdinaryCategory V D
X✝ Y✝ Z✝ : Dᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Quiver.Hom.opEquiv.symm.trans homEquiv) (f ≫ g) =
    (λ_ (𝟙_ V)).inv ≫
      ((Quiver.Hom.opEquiv.symm.trans homEquiv) g ⊗ₘ (Quiver.Hom.opEquiv.symm.trans homEquiv) f) ≫
        eComp V (Opposite.unop Z✝) (Opposite.unop Y✝) (Opposite.unop X✝)
Module: Mathlib.CategoryTheory.Filtered.Flat

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsCofiltered D
inst✝ : RepresentablyFlat F
this : IsFiltered Cᵒᵖ
⊢ IsCofiltered C

Tactic:
exact isCofiltered_of_isFiltered_op C

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

Goal state before:
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
h✝ : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
h : σ.hom.app X = 𝟙 (F.obj X)
⊢ (autEmbedding F) σ X = 1

Tactic:
exact Iso.ext h

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
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).obj
a : (F.obj X).obj
⊢ ∃ g, ∀ (x : (F.obj X).obj), g • x = (ConcreteCategory.hom (t.hom.app X)) x

Tactic:
obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G a (t.hom.app X a)

Goal state after:
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
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).obj
a : (F.obj X).obj
g : G
hg : g • a = (ConcreteCategory.hom (t.hom.app X)) a
⊢ ∃ g, ∀ (x : (F.obj X).obj), g • x = (ConcreteCategory.hom (t.hom.app X)) x
Module: Mathlib.CategoryTheory.Groupoid.VertexGroup

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ inv f ≫ f ≫ δ ≫ inv f ≫ f = δ

Tactic:
inv_comp,

Goal state after:
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ inv f ≫ f ≫ δ ≫ 𝟙 d = δ
Module: Mathlib.CategoryTheory.Groupoid.VertexGroup

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ ((inv f ≫ f) ≫ δ) ≫ 𝟙 d = δ

Tactic:
inv_comp,

Goal state after:
C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ (𝟙 d ≫ δ) ≫ 𝟙 d = δ
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
⊢ ∃ X, Nonempty ((functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑V)))

Tactic:
obtain ⟨I, hf, hc, hi⟩ := exists_set_ker_evaluation_subset_of_isOpen F (one_mem V) V.isOpen'

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
⊢ ∃ X, Nonempty ((functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑V)))
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c : C
⊢ univ.Nonempty

Tactic:
simp only [univ_nonempty]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
n : ℕ
⊢ HasWidePullback (Arrow.mk ((isTerminalIncl T hT).from U)).right
    (fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).left) fun x ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom

Tactic:
by
  dsimp
  have : HasProduct fun (x : Fin (n + 1)) ↦ U := ⟨⟨_, U.isLimitPowerFan (Fin (n + 1))⟩⟩
  exact hasWidePullback_of_isTerminal _ (isTerminalIncl _ hT)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
this : coprod.inl ≫ coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫ Cofork.π s = coprod.inl ≫ 0
⊢ (F.flip.obj Y₂).map f₁ ≫ Cofork.π s = 0 ≫ Cofork.π s

Tactic:
coprod.inl_desc_assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
this : (F.map f₁).app Y₂ ≫ Cofork.π s = coprod.inl ≫ 0
⊢ (F.flip.obj Y₂).map f₁ ≫ Cofork.π s = 0 ≫ Cofork.π s
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case 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
n m✝ k m : ℕ
h : n ≤ m
ih :
  ∀ (hh : ¬k < m),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
        Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
      Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
hh : ¬k < m + 1
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Tactic:
specialize ih (by lia)
    have : homOfLE (by lia : n ≤ m + 1) =
        homOfLE (by lia : n ≤ m) ≫ homOfLE (by lia : m ≤ m + 1) := by simp
    rw [this, op_comp, Functor.map_comp]
    slice_lhs 2 4 => rw [ih]
    simp only [homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
      functorMap, dite_eq_ite]
    split_ifs
    · omega
    simp [dif_neg (by lia : ¬(k < m)), dif_neg hh]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F.map f = π ((ConcreteCategory.hom (W.map f)) x)
x₁ x₂ : W.Elements
f : x₁ ⟶ x₂
⊢ ((Functor.const W.Elements).obj pt).map f ≫ π x₂.snd = π x₁.snd ≫ (CategoryOfElements.π W ⋙ F).map f

Tactic:
simpa using (hπ x₁.snd f.val).symm

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

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    rintro W X Y Z ⟨f⟩ ⟨g⟩ ⟨h⟩
    exact Quotient.sound (assoc f g h)

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

Goal state before:
pp: case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
W✝ X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ⊗ₘ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g'✝

Tactic:
rw [hfg, hfg']

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalLeftAction C D
inst✝¹ : MonoidalLeftAction C D'
inst✝ : F.OplaxLeftLinear C
d : D
⊢ δₗ F (𝟙_ C) d ≫ (λₗ (F.obj d)).hom = F.map (λₗ d).hom

Tactic:
simpa [-δₗ_unitality_inv] using
    F.map (λₗ[C] d).hom ≫=
      (δₗ_unitality_inv F d).symm =≫
      (λₗ[C] (F.obj d)).hom

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((α_ x✝³ x✝² x✝¹).hom.unop ⊵ₗ unop x✝).op ≫
      (αₗ (unop x✝³) (unop (x✝² ⊗ x✝¹)) (unop x✝)).symm.op.hom ≫
        (unop x✝³ ⊴ₗ (αₗ (unop x✝²) (unop x✝¹) (unop x✝)).symm.op.hom.unop).op =
    (αₗ (unop (x✝³ ⊗ x✝²)) (unop x✝¹) (unop x✝)).symm.op.hom ≫
      (αₗ (unop x✝³) (unop x✝²) (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom

Tactic:
apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((α_ x✝³ x✝² x✝¹).hom.unop ⊵ₗ unop x✝).op ≫
      (αₗ (unop x✝³) (unop (x✝² ⊗ x✝¹)) (unop x✝)).symm.op.hom ≫
        (unop x✝³ ⊴ₗ (αₗ (unop x✝²) (unop x✝¹) (unop x✝)).symm.op.hom.unop).op =
    (αₗ (unop (x✝³ ⊗ x✝²)) (unop x✝¹) (unop x✝)).symm.op.hom ≫
      (αₗ (unop x✝³) (unop x✝²) (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom

Tactic:
by
    apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((λ_ x✝¹).hom.unop ⊵ₗ unop x✝).op =
    (αₗ (unop (𝟙_ Cᵒᵖ)) (unop x✝¹) (unop x✝)).symm.op.hom ≫ (λₗ (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom

Tactic:
apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((λ_ x✝¹).hom.unop ⊵ₗ unop x✝).op =
    (αₗ (unop (𝟙_ Cᵒᵖ)) (unop x✝¹) (unop x✝)).symm.op.hom ≫ (λₗ (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom

Tactic:
by
    apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((ρ_ x✝¹).hom.unop ⊵ₗ unop x✝).op =
    (αₗ (unop x✝¹) (unop (𝟙_ Cᵒᵖ)) (unop x✝)).symm.op.hom ≫ (unop x✝¹ ⊴ₗ (λₗ (unop x✝)).symm.op.hom.unop).op

Tactic:
apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((ρ_ x✝¹).hom.unop ⊵ₗ unop x✝).op =
    (αₗ (unop x✝¹) (unop (𝟙_ Cᵒᵖ)) (unop x✝)).symm.op.hom ≫ (unop x✝¹ ⊴ₗ (λₗ (unop x✝)).symm.op.hom.unop).op

Tactic:
by
    apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.unop).op ≫
      (αᵣ (unop x✝) (unop x✝³) (unop (x✝² ⊗ x✝¹))).symm.op.hom ≫
        (αᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝³))) (unop x✝²) (unop x✝¹)).symm.op.hom =
    (αᵣ (unop x✝) (unop (x✝³ ⊗ x✝²)) (unop x✝¹)).symm.op.hom ≫
      ((αᵣ (unop x✝) (unop x✝³) (unop x✝²)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op

Tactic:
apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.unop).op ≫
      (αᵣ (unop x✝) (unop x✝³) (unop (x✝² ⊗ x✝¹))).symm.op.hom ≫
        (αᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝³))) (unop x✝²) (unop x✝¹)).symm.op.hom =
    (αᵣ (unop x✝) (unop (x✝³ ⊗ x✝²)) (unop x✝¹)).symm.op.hom ≫
      ((αᵣ (unop x✝) (unop x✝³) (unop x✝²)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op

Tactic:
by
    apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (λ_ x✝¹).hom.unop).op =
    (αᵣ (unop x✝) (unop (𝟙_ Cᵒᵖ)) (unop x✝¹)).symm.op.hom ≫ ((ρᵣ (unop x✝)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op

Tactic:
apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (λ_ x✝¹).hom.unop).op =
    (αᵣ (unop x✝) (unop (𝟙_ Cᵒᵖ)) (unop x✝¹)).symm.op.hom ≫ ((ρᵣ (unop x✝)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op

Tactic:
by
    apply Quiver.Hom.unop_inj
    apply IsIso.inv_eq_inv.mp
    simp

Goal state after: