mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
this : F.HasLeftDerivedFunctor W ↔ W.Q.HasRightKanExtension F
⊢ F.HasLeftDerivedFunctor W ↔ L.HasRightKanExtension F

Tactic:
this,

Goal state after:
C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
this : F.HasLeftDerivedFunctor W ↔ W.Q.HasRightKanExtension F
⊢ W.Q.HasRightKanExtension F ↔ L.HasRightKanExtension F
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case pos
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)
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
let t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }

Goal state after:
case pos
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 }
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom
X Y : C
f : X ⟶ Y
x✝ : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map f ≫ (a Y).hom)) x✝ = (ConcreteCategory.hom ((a X).hom ≫ F.map f)) x✝

Tactic:
simpa using ConcreteCategory.congr_hom (h ⟨X, Y, f⟩) _

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
⊢ (functorToContAction F).EssSurj

Tactic:
let : FiberFunctor F' := FiberFunctor.comp_right _

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
⊢ (functorToContAction F).EssSurj
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
⊢ {
        down :=
          (ConcreteCategory.hom
              ((((yoneda.obj (F ⋙ FintypeCat.incl)).mapIso
                        (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).op).toEquiv
                    (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f)).app
                ((incl F).obj A)))
            ((ConcreteCategory.hom ((colimit.ι ((incl F).op ⋙ coyoneda) (Opposite.op A)).app ((incl F).obj A)))
              (𝟙 ((incl F).obj A))) }.down =
    (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
change (((FullyFaithful.whiskeringRight (FullyFaithful.ofFullyFaithful
      FintypeCat.incl) C).homEquiv) f).app A
    (((colimit.ι _ _) ≫ (colimit.isoColimitCocone ⟨cocone F, isColimit F⟩).hom).app
      A _) = f.app A A.pt

Goal state after:
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))
      ((ConcreteCategory.hom
          ((colimit.ι ((incl F).op ⋙ coyoneda) (Opposite.op A) ≫
                (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom).app
            A.obj))
        (𝟙 ((incl F).obj A))) =
    (ConcreteCategory.hom (f.app A.obj)) A.pt
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
⊢ ∃ g, g • x = y

Tactic:
let : FiberFunctor F' := FiberFunctor.comp_right _

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
⊢ ∃ g, g • x = y
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
this : ((toAut F G) g).hom.app X = 𝟙 (F.obj X)
⊢ (ConcreteCategory.hom (((toAut F G) g).hom.app X)) x = x

Tactic:
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
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
this : ((toAut F G) g).hom.app X = 𝟙 (F.obj X)
⊢ (ConcreteCategory.hom (𝟙 (F.obj X))) x = x
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z✝ : Cat
F : X✝ ⟶ Y✝
G : Y✝ ⟶ Z✝
⊢ map (F ≫ G).toFunctor = map F.toFunctor ≫ map G.toFunctor

Tactic:
by simp [Grpd.comp_eq_comp, map_comp]

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
hf : f ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
g : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
hg : g ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
hfg : (fun f ↦ S.hom.map f) ⟨f, hf⟩ = (fun f ↦ S.hom.map f) ⟨g, hg⟩
⊢ ⟨f, hf⟩ = ⟨g, hg⟩

Tactic:
exact Subtype.ext hfg

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasPullbacks C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
h : X ⟶ Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom h ↔ HasLiftingProperty f (Opposite.op (Arrow.mk g) ⋔ Arrow.mk h).hom

Tactic:
by
  rw [← hasLiftingProperty_mk_iff]
  exact HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
⊢ ∀ (j : WalkingMultispan (multispanShapeCoend J)),
    (ChosenCoendsOfShape.cowedge F).ι.app j ≫ f = (ChosenCoendsOfShape.cowedge F).ι.app j ≫ g

Tactic:
rintro (a | a)

Goal state after:
case left
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).L
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ g

case right
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).R
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ g
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
hh : ¬k < m + 1
ih :
  (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 ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (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:
this,

Goal state after:
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
hh : ¬k < m + 1
ih :
  (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 ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯ ≫ 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 ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case succ
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 + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    functorMap f (m + 1) ≫ Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯

Tactic:
this,

Goal state after:
case succ
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 + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯ ≫ homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    functorMap f (m + 1) ≫ Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

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

Tactic:
this,

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend J)), (cowedge F).ι.app j ≫ m = s.ι.app j
⊢ m = ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯

Tactic:
ext ⟨j⟩; exact ConcreteCategory.congr_hom (h (.right j.fst)) j.snd

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app none = s.π.app none

Tactic:
by
        rw [← s.w WalkingCospan.Hom.inl, ← t.w WalkingCospan.Hom.inl, ← Category.assoc]
        congr
        exact fac_left s

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

Goal state before:
pp: case refine_2
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
⊢ (curriedAssociatorNatIso (LocalizedMonoidal L W ε)).inv ≫
      ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε) =
    ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε)

Tactic:
apply natTrans₃_ext (L') (L') (L') W W W
    simpa using! map_hexagon_reverse _ _ _

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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
⊢ ε (L ⋙ F) ≫ (Lifting.iso L W G F).hom.app (𝟙_ C) = ε G

pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
x✝¹ x✝ : C
⊢ μ (L ⋙ F) x✝¹ x✝ ≫ (Lifting.iso L W G F).hom.app (x✝¹ ⊗ x✝) =
    ((Lifting.iso L W G F).hom.app x✝¹ ⊗ₘ (Lifting.iso L W G F).hom.app x✝) ≫ μ G x✝¹ x✝

Tactic:
· simp [functorMonoidalOfComp_ε]

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
this : F.Monoidal := functorMonoidalOfComp L W F G
x✝¹ x✝ : C
⊢ μ (L ⋙ F) x✝¹ x✝ ≫ (Lifting.iso L W G F).hom.app (x✝¹ ⊗ x✝) =
    ((Lifting.iso L W G F).hom.app x✝¹ ⊗ₘ (Lifting.iso L W G F).hom.app x✝) ≫ μ G x✝¹ x✝
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ curry ((β_ I A).hom ≫ Hom.left u) ≫ (ihom I).map X.hom = toUnit A ≫ curryRightUnitorHom I

Tactic:
rw [curry_natural_right, Category.assoc, ← Functor.map_comp, w,
      ← curry_natural_right, toUnit_comp_curryRightUnitorHom]
    congr
    simp [braiding_hom_snd]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
c : C
d d' : D
f : d ⟶ d'
⊢ 𝟙 c ⊙ₗₘ f = c ⊴ₗ f

Tactic:
by
  simp [actionHom_def]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
c c' : C
f : c ⟶ c'
d : D
⊢ f ⊙ₗₘ 𝟙 d = f ⊵ₗ d

Tactic:
by
  simp [actionHom_def]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
d d' : D
f : d ⟶ d'
c : C
⊢ f ⊙ᵣₘ 𝟙 c = f ⊵ᵣ c

Tactic:
by
  simp [actionHom_def]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
d : D
c c' : C
f : c ⟶ c'
⊢ 𝟙 d ⊙ᵣₘ f = d ⊴ᵣ f

Tactic:
by
  simp [actionHom_def]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [((e' e).functor ⋙ (e' e).inverse).map_braiding X Y,
        assoc, Functor.Monoidal.μ_δ, comp_id, Functor.Monoidal.μ_δ_assoc]

Goal state after:
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
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
h' : ∀ (d d' : D), IsIso (L.map (d ◁ adj.unit.app d'))
d d' : D
this : adj.unit.app d ⊗ₘ adj.unit.app d' = adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'
⊢ IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
this,

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
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
h' : ∀ (d d' : D), IsIso (L.map (d ◁ adj.unit.app d'))
d d' : D
this : adj.unit.app d ⊗ₘ adj.unit.app d' = adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'
⊢ IsIso (L.map (adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'))
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ

Tactic:
· replace h := h (fst (R ⊗ R) R ≫ fst _ _) (fst _ _ ≫ snd _ _) (snd _ _)
    simp only [Hom.mul_def, Hom.add_def] at h
    convert! h using 2
    · cat_disch
    · ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
this : prod.fst = prod.snd
⊢ prod.lift f g ≫ prod.fst = g

Tactic:
this,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
this : prod.fst = prod.snd
⊢ prod.lift f g ≫ prod.snd = g
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
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
⊢ ExponentialIdeal i

Tactic:
let L : C ⥤ D := reflector i

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
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
⊢ ExponentialIdeal i