mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
⊢ ∃! τ, f ≫ τ.hom = σ.hom ≫ f

Tactic:
by
  let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  refine ⟨?_, ?_, ?_⟩
  · exact (evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)
  · apply evaluation_injective_of_isConnected F A B a
    simp
  · intro τ hτ
    apply evaluation_aut_injective_of_isConnected F B (F.map f a)
    simpa using ConcreteCategory.congr_hom (F.congr_map hτ) a

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
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
⊢ Nat.card (F.obj Z).obj < n

Tactic:
rw [hn, hnn, lt_add_iff_pos_left]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
⊢ 0 < Nat.card (F.obj Y).obj
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 ((F ⋙ FintypeCat.uSwitch).map f))
        ((FintypeCat.equivEquivIso.symm (Iso.app g' X)) ((F.obj X).uSwitchEquiv.symm x)))

Tactic:
← NatTrans.naturality_apply,

Goal state after:
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)) ((ConcreteCategory.hom (F'.map f)) ((F.obj X).uSwitchEquiv.symm x)))
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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
g : G
hg : g ∈ c
X : C
x✝ : IsGalois X
x : (F.obj X).obj
this : g ∈ gi { obj := X, pt := x, isGalois := ⋯ } • ↑(MulAction.stabilizer G x)
⊢ g • x = (ConcreteCategory.hom (t.hom.app X)) x

Tactic:
obtain ⟨s, (hsmem : s • x = x), (rfl : gi ⟨X, x, inferInstance⟩ • s = _)⟩ := this

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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
X : C
x✝ : IsGalois X
x : (F.obj X).obj
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ } • s ∈ c
⊢ (gi { obj := X, pt := x, isGalois := ⋯ } • s) • x = (ConcreteCategory.hom (t.hom.app X)) x
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
hp : ∀ i ∈ s, p✝ ∈ i.arrows c✝ d✝
x✝ : d✝ ⟶ e✝
hq : ∀ i ∈ s, x✝ ∈ i.arrows d✝ e✝
⊢ ∀ i ∈ s, p✝ ≫ x✝ ∈ i.arrows c✝ e✝

Tactic:
exact fun S hS => S.mul (hp S hS) (hq S hS)

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
hφ : Function.Injective φ.obj
S : Subgroupoid C
⊢ ∀ {c d e : D} {p : c ⟶ d},
    p ∈ {x | Map.Arrows φ hφ S c d x} →
      ∀ {q : d ⟶ e}, q ∈ {x | Map.Arrows φ hφ S d e x} → p ≫ q ∈ {x | Map.Arrows φ hφ S c e x}

Tactic:
rintro _ _ _ _ ⟨f, hf⟩ q hq
    obtain ⟨c₃, c₄, g, he, rfl, hg, gq⟩ := (Map.arrows_iff φ hφ S q).mp hq
    cases hφ he; rw [gq, ← eq_conj_eqToHom, ← φ.map_comp]
    constructor; exact S.mul hf hg

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

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    NatTrans.toCatHom₂ (mapWhiskerRight (α_ f g h).hom.toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D (f ≫ g).toFunctor h.toFunctor)).hom ≫
        (Cat.Hom.isoMk (mapCompLeft D f.toFunctor g.toFunctor)).hom ▷ (mapPair h.toFunctor (𝟭 D)).toCatHom ≫
          (α_ (mapPair f.toFunctor (𝟭 D)).toCatHom (mapPair g.toFunctor (𝟭 D)).toCatHom
                (mapPair h.toFunctor (𝟭 D)).toCatHom).hom ≫
            (mapPair f.toFunctor (𝟭 D)).toCatHom ◁ (Cat.Hom.isoMk (mapCompLeft D g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapCompLeft D f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
intros; exact congr($(mapWhiskerRight_associator_hom D _ _ _).toCatHom₂)

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
x✝ : (U.power α).I
⊢ (powerMap (f ≫ g) α).f x✝ = (powerMap f α ≫ powerMap g α).f x✝

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
⊢ (powerMap (f ≫ g) α).φ i✝ ≫ eqToHom ⋯ = (powerMap f α ≫ powerMap g α).φ i✝

Tactic:
· cat_disch

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
⊢ (powerMap (f ≫ g) α).φ i✝ ≫ eqToHom ⋯ = (powerMap f α ≫ powerMap g α).φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
x✝ : (U.power γ).I
⊢ (U.mapPower (g ∘ f)).f x✝ = (U.mapPower g ≫ U.mapPower f).f x✝

pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
i✝ : (U.power γ).I
⊢ (U.mapPower (g ∘ f)).φ i✝ ≫ eqToHom ⋯ = (U.mapPower g ≫ U.mapPower f).φ i✝

Tactic:
· cat_disch

Goal state after:
case h₂
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
i✝ : (U.power γ).I
⊢ (U.mapPower (g ∘ f)).φ i✝ ≫ eqToHom ⋯ = (U.mapPower g ≫ U.mapPower f).φ i✝
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
x✝ : (U.power β).I
⊢ (U.mapPower g ≫ powerMap f α).f x✝ = (powerMap f β ≫ V.mapPower g).f x✝

pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
i✝ : (U.power β).I
⊢ (U.mapPower g ≫ powerMap f α).φ i✝ ≫ eqToHom ⋯ = (powerMap f β ≫ V.mapPower g).φ i✝

Tactic:
· cat_disch

Goal state after:
case h₂
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
i✝ : (U.power β).I
⊢ (U.mapPower g ≫ powerMap f α).φ i✝ ≫ eqToHom ⋯ = (powerMap f β ≫ V.mapPower g).φ i✝
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 G : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F }.φ i ≫ eqToHom ⋯ = { f := f, φ := G }.φ i
i : X.I
⊢ F i = G i

Tactic:
simpa using h₂ i

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

Goal state before:
pp: 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
⊢ False

Tactic:
apply not_le_of_gt (Cardinal.cantor α)

Goal state after:
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 := ⋯
α : Cardinal.{u} := ⋯
⊢ 2 ^ α ≤ α
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

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
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
eₗ : x.fst ≅ y.fst
eᵣ : x.snd ≅ y.snd
w : F.map eₗ.hom ≫ y.iso.hom = x.iso.hom ≫ G.map eᵣ.hom
⊢ F.map eₗ.inv ≫ x.iso.hom = y.iso.hom ≫ G.map eᵣ.inv

Tactic:
simpa using F.map eₗ.inv ≫= w.symm =≫ G.map eᵣ.inv

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X P.X Q.X).inv

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| P.actLeft ▷ Q.X

Tactic:
whiskerLeft_comp

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ P.X S.X Q.X).hom ≫ R.X ◁ P.X ◁ Q.actLeft

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X P.X Q.X).inv

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| P.actLeft ▷ Q.X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ P.X ◁ Q.actLeft ≫ (α_ R.X P.X Q.X).inv

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| P.actLeft ▷ Q.X

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ P.X S.X Q.X).hom

Tactic:
associator_inv_naturality_right

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X P.X (S.X ⊗ Q.X)).inv ≫ (R.X ⊗ P.X) ◁ Q.actLeft

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| P.actLeft ▷ Q.X

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ P.X S.X Q.X).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ R.X P.X Q.X).inv ≫
    R.X ◁ (P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| actLeft P Q

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X R.X (P.X ⊗ Q.X)).hom

Tactic:
whiskerLeft_comp

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ (α_ R.X P.X Q.X).inv ≫
    R.X ◁ P.actLeft ▷ Q.X ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| actLeft P Q

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (α_ R.X R.X (P.X ⊗ Q.X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ ((α_ S.X Q.X T.X).hom ≫ S.X ◁ Q.actRight ≫ Q.actLeft)

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X S.X Q.X).hom ▷ T.X

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X (S.X ⊗ Q.X) T.X).hom

Tactic:
whiskerLeft_comp

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ (α_ S.X Q.X T.X).hom ≫ P.X ◁ (S.X ◁ Q.actRight ≫ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X S.X Q.X).hom ▷ T.X

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X (S.X ⊗ Q.X) T.X).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ (Q.actRight ▷ T.X ≫ Q.actRight)

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X Q.X (T.X ⊗ T.X)).hom

Tactic:
whiskerLeft_comp

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ Q.actRight ▷ T.X ≫ P.X ◁ Q.actRight

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ P.X Q.X (T.X ⊗ T.X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: case e'_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h :
  lift (fst R (R ⊗ R)) (lift (snd R (R ⊗ R) ≫ fst R R) (snd R (R ⊗ R) ≫ snd R R) ≫ σ) ≫ μ =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ) ≫ σ
⊢ R ◁ σ = lift (fst R (R ⊗ R)) (lift (snd R (R ⊗ R) ≫ fst R R) (snd R (R ⊗ R) ≫ snd R R) ≫ σ)

pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h :
  lift (fst R (R ⊗ R)) (lift (snd R (R ⊗ R) ≫ fst R R) (snd R (R ⊗ R) ≫ snd R R) ≫ σ) ≫ μ =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ) ≫ σ
⊢ lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ)

Tactic:
· cat_disch

Goal state after:
case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h :
  lift (fst R (R ⊗ R)) (lift (snd R (R ⊗ R) ≫ fst R R) (snd R (R ⊗ R) ≫ snd R R) ≫ σ) ≫ μ =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ) ≫ σ
⊢ lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ)