mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Function.Surjective ⇑(toAut F G)

Tactic:
by
  intro t
  choose gi hgi using (fun X : PointedGaloisObject F ↦ toAut_surjective_isGalois F G t X)
  let cl (X : PointedGaloisObject F) : Set G := gi X • MulAction.stabilizer G X.pt
  let c : Set G := ⋂ i, cl i
  have hne : c.Nonempty := by
    rw [← Set.univ_inter c]
    apply CompactSpace.isCompact_univ.inter_iInter_nonempty
    · intro X
      apply IsClosed.leftCoset
      exact Subgroup.isClosed_of_isOpen _ (stabilizer_isOpen G X.pt)
    · intro s
      rw [Set.univ_inter]
      obtain ⟨gs, hgs⟩ :=
        toAut_surjective_isGalois_finite_family F G t (fun X : s ↦ X.val.obj) h
      use gs
      simp only [Set.mem_iInter]
      intro X hXmem
      rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul,
        hgs ⟨X, hXmem⟩, ← hgi X, inv_smul_smul]
  obtain ⟨g, hg⟩ := hne
  refine ⟨g, Iso.ext <| natTrans_ext_of_isGalois _ <| fun X _ ↦ ?_⟩
  ext x
  simp only [toAut_hom_app_apply]
  have : g ∈ (gi ⟨X, x, inferInstance⟩ • MulAction.stabilizer G x : Set G) := by
    simp only [Set.mem_iInter, c] at hg
    exact hg _
  obtain ⟨s, (hsmem : s • x = x), (rfl : gi ⟨X, x, inferInstance⟩ • s = _)⟩ := this
  rw [smul_eq_mul, mul_smul, hsmem]
  exact hgi ⟨X, x, inferInstance⟩ x

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
⊢ Quiver.FreeGroupoid.of C ⋙q (Quotient.functor (homRel C)).toPrefunctor ⋙q (lift φ).toPrefunctor = φ.toPrefunctor

Tactic:
simp [lift, Quotient.lift_spec, Quiver.FreeGroupoid.lift_spec]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ i₂ + i₁ + i₃ = k

Tactic:
rw [add_comm i₂ i₁, h]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : Type u₁
inst✝¹ : Groupoid G
H : Type u₂
inst✝ : Groupoid H
φ : C ⥤ G
ψ : G ⥤ H
⊢ lift (φ ⋙ ψ) = lift φ ⋙ ψ

Tactic:
by
  symm
  apply lift_unique
  rw [← Functor.assoc, lift_spec]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
⊢ (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d

Tactic:
apply S.mul h (S.inv hg)

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
d : D
⊢ d ∈ (map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d

Tactic:
dsimp [objs, map]

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty ↔ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d
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
l : h.LiftStruct g₁ g₂ b
⊢ g₁ ≫ f₁ = g₂ ≫ f₂

Tactic:
simp only [← l.f_p₁, ← l.f_p₂, Category.assoc, h.condition]

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

Goal state before:
pp: case inst
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun i ↦
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
apply +allowSynthFailures Pi.map_epi

Goal state after:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ ∀ (j : { x // x < n + 1 }),
    Epi (if h : ↑j < n then eqToHom ⋯ else if h' : ↑j < n + 1 then eqToHom ⋯ ≫ f ↑j ≫ eqToHom ⋯ else eqToHom ⋯)
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j✝ j'✝ : J
g : j✝ ⟶ j'✝
y : (F.obj (op j'✝)).obj j✝
⊢ Types.coendRel G ⟨j✝, (hom ((f.app (op j✝)).app j✝)) ((Hom.hom ((F.map g.op).app j✝)) y)⟩
    ⟨j'✝, (hom ((f.app (op j'✝)).app j'✝)) ((Hom.hom ((F.obj (op j'✝)).map g)) y)⟩

Tactic:
Types.coendRel_iff

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j✝ j'✝ : J
g : j✝ ⟶ j'✝
y : (F.obj (op j'✝)).obj j✝
⊢ ∃ f_1 y_1,
    (hom ((G.map f_1.op).app j✝)) y_1 = (hom ((f.app (op j✝)).app j✝)) ((Hom.hom ((F.map g.op).app j✝)) y) ∧
      (hom ((G.obj (op j'✝)).map f_1)) y_1 = (hom ((f.app (op j'✝)).app j'✝)) ((Hom.hom ((F.obj (op j'✝)).map g)) y)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝³ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝² : C
x✝¹ : D
x✝ : Reflective R := { toFull := inst✝, toFaithful := inst✝¹, L := L, adj := adj }
this : IsIso adj.toMonad.μ
⊢ IsIso (adj.unit.app ((ihom x✝¹).obj (R.obj x✝²)))

Tactic:
← dsimp% [Adjunction.toMonad] adj.toMonad.isSplitMono_iff_isIso_unit

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝³ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝² : C
x✝¹ : D
x✝ : Reflective R := { toFull := inst✝, toFaithful := inst✝¹, L := L, adj := adj }
this : IsIso adj.toMonad.μ
⊢ IsSplitMono (adj.unit.app ((ihom x✝¹).obj (R.obj x✝²)))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: 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) ≫ (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X =
    ((α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (α_ R.X P.X S.X).inv ▷ Q.X ≫ P.actLeft ▷ S.X ▷ Q.X) ≫
      (α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft

Tactic:
slice_lhs 1 1 => rw [whiskerLeft_comp]

Goal state after:
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) ≫ (α_ R.X P.X Q.X).inv) ≫ P.actLeft ▷ Q.X =
    ((α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (α_ R.X P.X S.X).inv ▷ Q.X ≫ P.actLeft ▷ S.X ▷ Q.X) ≫
      (α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
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 ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ 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)
| η ▷ (P.X ⊗ Q.X)

Tactic:
whiskerLeft_π_actLeft

Goal state after:
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 P.X Q.X).inv ≫ P.actLeft ▷ Q.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₁} (tensorLeft X)
| η ▷ (P.X ⊗ Q.X)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
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 ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ 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)
| μ ▷ (P.X ⊗ Q.X)

Tactic:
whiskerLeft_π_actLeft

Goal state after:
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 P.X Q.X).inv ≫ P.actLeft ▷ Q.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₁} (tensorLeft X)
| μ ▷ (P.X ⊗ Q.X)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.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 ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ 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

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

pp: case a.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 ◁ P.actLeft ▷ Q.X

Tactic:
whiskerLeft_π_actLeft

Goal state after:
case a.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 P.X Q.X).inv ≫ P.actLeft ▷ Q.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₁} (tensorLeft X)
| (α_ R.X R.X (P.X ⊗ Q.X)).hom

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

case a.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 ◁ P.actLeft ▷ Q.X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ 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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X (P.X ⊗ Q.X) T.X).hom

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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ (α_ P.X Q.X T.X).hom

pp: case a.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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ P.X ◁ Q.actRight

Tactic:
whiskerLeft_π_actLeft

Goal state after:
case a.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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X (P.X ⊗ Q.X) T.X).hom

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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ (α_ P.X Q.X T.X).hom

case a.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)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ P.X ◁ Q.actRight
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete

Goal state before:
pp: I : Type u₂
inst✝⁴ : Category.{v₂, u₂} I
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : ∀ (F : Discrete I ⥤ C), (Discrete.functor _root_.id).HasRightKanExtension F
A✝ B✝ : I ⥤ C
f : A✝ ⟶ B✝
h : IsIso (((whiskeringLeft (Discrete I) I C).obj (incl I)).map f)
⊢ IsIso f

Tactic:
simp only [NatTrans.isIso_iff_isIso_app] at *
    intro X
    exact h ⟨X⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
this : HasFiniteProducts D
⊢ IsIso ((reflectorAdjunction i).unit.app (𝟙_ C))

Tactic:
refine Functor.essImage.unit_isIso ⟨terminal D, ⟨PreservesTerminal.iso i |>.trans ?_⟩⟩

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
this : HasFiniteProducts D
⊢ ⊤_ C ≅ 𝟙_ C
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j : C
⊢ (ℌ.map f ℌ').app c ≫ ℌ'.π c j = ℌ.π c j ≫ (ihom (F.obj j)).map (f.app (j ⊗ c))

Tactic:
by
  dsimp [map]
  rw [← Wedge.mk_ι
      (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
      (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
    Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c)]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive 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₂
inst✝ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
⊢ coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂) = 0

Tactic:
by
    ext
    · simp [tensorHom_def, ← comp_whiskerRight_assoc, coprod.inl_desc]
    · simp [tensorHom_def', ← whiskerLeft_comp_assoc, coprod.inr_desc]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁
          (N.X ◁ f.hom ≫
            colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))
              WalkingParallelPair.one) ≫
        (PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)).inv ≫
          coequalizer.desc
            ((α_ M.X N.X P'.X).inv ≫
              coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X ≫
                coequalizer.π (TensorBimod.actRight M N ▷ P'.X)
                  ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft))
            ⋯

Tactic:
slice_rhs 2 2 => rw [whiskerLeft_comp]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      ((M.X ◁ N.X ◁ f.hom ≫
            M.X ◁
              colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))
                WalkingParallelPair.one) ≫
          (PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P'.X)
              ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)).inv) ≫
        coequalizer.desc
          ((α_ M.X N.X P'.X).inv ≫
            coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X ≫
              coequalizer.π (TensorBimod.actRight M N ▷ P'.X)
                ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft))
          ⋯
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
n : ℕ
α : F ⟶ G
⊢ F.a ≫ (n • U.map α.f) = (n • α.f) ≫ G.a

Tactic:
comp_nsmul,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
n : ℕ
α : F ⟶ G
⊢ n • F.a ≫ U.map α.f = (n • α.f) ≫ G.a
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
α : F ⟶ G
⊢ F.a ≫ U.map (-α.f) = (-α.f) ≫ G.a

Tactic:
by simp only [Functor.map_neg, comp_neg, Comonad.Coalgebra.Hom.h, neg_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)

Tactic:
comp_nsmul,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ F.map (n • α.f) ≫ A₂.str = n • A₁.str ≫ α.f
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ A₁.str ≫ (n • F.map α.f) = (n • α.f) ≫ A₂.str

Tactic:
comp_nsmul,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ n • A₁.str ≫ F.map α.f = (n • α.f) ≫ A₂.str