mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this : HomRel.CompClosure redStep (q ≫ q.reverse) (q ≫ f.toPath ≫ (reverse f).toPath ≫ q.reverse)
⊢ HomRel.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath ≫ q.reverse)

Tactic:
simp only [← Category.assoc] at this ⊢

Goal state after:
case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this : HomRel.CompClosure redStep (q ≫ q.reverse) (((q ≫ f.toPath) ≫ (reverse f).toPath) ≫ q.reverse)
⊢ HomRel.CompClosure redStep (q ≫ q.reverse) ((q.cons f ≫ (reverse f).toPath) ≫ q.reverse)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

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

Tactic:
apply congr_comp_reverse

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g :=
  TwoSquare.StructuredArrowRightwards.mk (TwoSquare.overPost F X) g (Over.mk prod.fst)
    (Over.homMk
      (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z))
      ⋯)
    prod.snd ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ Over.Hom.left (StructuredArrow.hom Q).left ≫
      F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom) =
    Over.Hom.left (StructuredArrow.hom P).left

Tactic:
rw [← cancel_mono (prodComparison F X _)]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g :=
  TwoSquare.StructuredArrowRightwards.mk (TwoSquare.overPost F X) g (Over.mk prod.fst)
    (Over.homMk
      (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z))
      ⋯)
    prod.snd ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ (Over.Hom.left (StructuredArrow.hom Q).left ≫
        F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
      prodComparison F X Z =
    Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ discrete.arrows c✝ c✝
⊢ Groupoid.inv f ≫ γ ≫ f ∈ discrete.arrows d✝ d✝

Tactic:
cases hγ

Goal state after:
case id
C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
⊢ Groupoid.inv f ≫ 𝟙 c✝ ≫ f ∈ discrete.arrows d✝ d✝
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 := ⋯
α : Cardinal.{u} := ⋯
⊢ 2 ^ α ≤ α

Tactic:
let yp : C := ∏ᶜ fun _ : md => Y

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 := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
⊢ 2 ^ α ≤ α
Module: Mathlib.CategoryTheory.Localization.FiniteProducts

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
J : Type
inst✝³ : HasProductsOfShape J C
inst✝² : W.IsStableUnderProductsOfShape J
inst✝¹ : W.ContainsIdentities
inst✝ : Finite J
F : Discrete J ⥤ C
⊢ ∀ (j : Discrete J),
    (coneOfAdj (adj L W J) (F ⋙ L)).π.app j =
      ((compLimitFunctorIso L W J).app F).hom ≫ (L.mapCone (limit.cone F)).π.app j

Tactic:
by simp [adj_counit_app, constLimAdj]

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

Goal state before:
pp: case α_inv_hom
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)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).inv ≫
      (α_ (projectObj f✝ X✝) (projectObj f✝ Y✝) (projectObj f✝ Z✝)).hom =
    𝟙 (projectObj f✝ (X✝.tensor (Y✝.tensor Z✝)))

Tactic:
rw [Iso.inv_hom_id]

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

Goal state before:
pp: case ρ_inv_hom
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)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (ρ_ (projectObj f✝ X✝)).inv ≫ (ρ_ (projectObj f✝ X✝)).hom = 𝟙 (projectObj f✝ X✝)

Tactic:
rw [Iso.inv_hom_id]

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

Goal state before:
pp: case l_inv_hom
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)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (λ_ (projectObj f✝ X✝)).inv ≫ (λ_ (projectObj f✝ X✝)).hom = 𝟙 (projectObj f✝ X✝)

Tactic:
rw [Iso.inv_hom_id]

Goal state after:
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 ≫ ((toOver I).obj A).hom) = toUnit A ≫ curryRightUnitorHom I

Tactic:
toUnit_comp_curryRightUnitorHom

Goal state after:
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 ≫ ((toOver I).obj A).hom) = curry (SemiCartesianMonoidalCategory.fst I A)
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝² x✝¹ : Type u
x✝ : x✝² ⟶ x✝¹
⊢ (__Functor✝ ⋙ __Functor✝).map x✝ ≫ ↾joinM = ↾joinM ≫ __Functor✝.map x✝

Tactic:
ext _

Goal state after:
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝³ x✝² : Type u
x✝¹ : x✝³ ⟶ x✝²
x✝ : (__Functor✝ ⋙ __Functor✝).obj x✝³
⊢ (ConcreteCategory.hom ((__Functor✝ ⋙ __Functor✝).map x✝¹ ≫ ↾joinM)).toFun x✝ =
    (ConcreteCategory.hom (↾joinM ≫ __Functor✝.map x✝¹)).toFun x✝
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
c₁✝ c₂✝ c₃✝ c₄✝ : Cᵒᵖ
d₁✝ d₂✝ : Dᵒᵖ
f : unop c₂✝ ⟶ unop c₁✝
g : unop c₄✝ ⟶ unop c₃✝
h : unop d₂✝ ⟶ unop d₁✝
this :
  (αₗ (unop c₂✝) (unop c₄✝) (unop d₂✝)).inv ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ (αₗ (unop c₁✝) (unop c₃✝) (unop d₁✝)).hom =
    f ⊙ₗₘ g ⊙ₗₘ h
⊢ (((op f ⊗ₘ op g).unop ⊙ₗₘ Quiver.Hom.unop (op h)).op ≫ (αₗ (unop c₂✝) (unop c₄✝) (unop d₂✝)).symm.op.hom).unop =
    ((αₗ (unop c₁✝) (unop c₃✝) (unop d₁✝)).symm.op.hom ≫
        (Quiver.Hom.unop (op f) ⊙ₗₘ (Quiver.Hom.unop (op g) ⊙ₗₘ Quiver.Hom.unop (op h)).op.unop).op).unop

Tactic:
simp [← this]

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ᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : C
d₁✝ d₂✝ : D
f : c₁✝ ⟶ c₂✝
g : c₃✝ ⟶ c₄✝
h : d₁✝ ⟶ d₂✝
this :
  (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).inv ≫ ((f.op ⊗ₘ g.op) ⊙ₗₘ h.op) ≫ (αₗ (op c₁✝) (op c₃✝) (op d₁✝)).hom =
    f.op ⊙ₗₘ g.op ⊙ₗₘ h.op
⊢ (((f ⊗ₘ g).op ⊙ₗₘ h.op).unop ≫ (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).symm.unop.hom).op =
    ((αₗ (op c₁✝) (op c₃✝) (op d₁✝)).symm.unop.hom ≫ (f.op ⊙ₗₘ (g.op ⊙ₗₘ h.op).unop.op).unop).op

Tactic:
simp [← this]

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ᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : C
d₁✝ d₂✝ : D
f : c₁✝ ⟶ c₂✝
g : c₃✝ ⟶ c₄✝
h : d₁✝ ⟶ d₂✝
⊢ ((f ⊗ₘ g).op ⊙ₗₘ h.op).unop ≫ (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).symm.unop.hom =
    (αₗ (op c₁✝) (op c₃✝) (op d₁✝)).symm.unop.hom ≫ (f.op ⊙ₗₘ (g.op ⊙ₗₘ h.op).unop.op).unop

Tactic:
apply Quiver.Hom.op_inj
    have := (αₗ (op _) (op _) (op _)).inv ≫=
      MonoidalLeftAction.actionAssocIso_hom_naturality f.op g.op h.op
    simp only [Iso.inv_hom_id_assoc] at this
    simp [← this]

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
d₁✝ d₂✝ : Dᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : Cᵒᵖ
f : unop d₂✝ ⟶ unop d₁✝
g : unop c₂✝ ⟶ unop c₁✝
h : unop c₄✝ ⟶ unop c₃✝
this :
  (αᵣ (unop d₂✝) (unop c₂✝) (unop c₄✝)).inv ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ (αᵣ (unop d₁✝) (unop c₁✝) (unop c₃✝)).hom =
    (f ⊙ᵣₘ g) ⊙ᵣₘ h
⊢ ((Quiver.Hom.unop (op f) ⊙ᵣₘ (op g ⊗ₘ op h).unop).op ≫ (αᵣ (unop d₂✝) (unop c₂✝) (unop c₄✝)).symm.op.hom).unop =
    ((αᵣ (unop d₁✝) (unop c₁✝) (unop c₃✝)).symm.op.hom ≫
        ((Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op.unop ⊙ᵣₘ Quiver.Hom.unop (op h)).op).unop

Tactic:
simp [← this]

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ᵒᵖ
d₁✝ d₂✝ : D
c₁✝ c₂✝ c₃✝ c₄✝ : C
f : d₁✝ ⟶ d₂✝
g : c₁✝ ⟶ c₂✝
h : c₃✝ ⟶ c₄✝
this :
  (αᵣ (op d₂✝) (op c₂✝) (op c₄✝)).inv ≫ (f.op ⊙ᵣₘ g.op ⊗ₘ h.op) ≫ (αᵣ (op d₁✝) (op c₁✝) (op c₃✝)).hom =
    (f.op ⊙ᵣₘ g.op) ⊙ᵣₘ h.op
⊢ ((f.op ⊙ᵣₘ (g ⊗ₘ h).op).unop ≫ (αᵣ (op d₂✝) (op c₂✝) (op c₄✝)).symm.unop.hom).op =
    ((αᵣ (op d₁✝) (op c₁✝) (op c₃✝)).symm.unop.hom ≫ ((f.op ⊙ᵣₘ g.op).unop.op ⊙ᵣₘ h.op).unop).op

Tactic:
simp [← this]

Goal state after:
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
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ f.inv ≫ f.hom = 𝟙 Q.X

Tactic:
rw [Iso.inv_hom_id]

Goal state after:
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 ≫ 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

Tactic:
slice_lhs 2 3 => rw [associator_inv_naturality_right]

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 (S.X ⊗ Q.X)).inv ≫ (R.X ⊗ P.X) ◁ Q.actLeft) ≫ 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.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'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
x✝ : (tensorLeft ((L ⋙ R).obj d)).obj (Opposite.unop (Opposite.op d')) ⟶ R.obj c
⊢ (ConcreteCategory.hom (↾fun g ↦ g ≫ (pre (adj.unit.app d)).app (R.obj c)))
      ((ihom.adjunction (R.obj (L.obj d))).unit.app d' ≫ (ihom (R.obj (L.obj d))).map x✝) =
    ((ihom.adjunction d).homEquiv d' (R.obj c))
      ((ConcreteCategory.hom ((yoneda.obj (R.obj c)).map ((adj.unit.app d).op ▷ Opposite.op d'))) x✝)

Tactic:
Adjunction.homEquiv_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'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
x✝ : (tensorLeft ((L ⋙ R).obj d)).obj (Opposite.unop (Opposite.op d')) ⟶ R.obj c
⊢ (ConcreteCategory.hom (↾fun g ↦ g ≫ (pre (adj.unit.app d)).app (R.obj c)))
      ((ihom.adjunction (R.obj (L.obj d))).unit.app d' ≫ (ihom (R.obj (L.obj d))).map x✝) =
    (ihom.adjunction d).unit.app d' ≫
      (ihom d).map ((ConcreteCategory.hom ((yoneda.obj (R.obj c)).map ((adj.unit.app d).op ▷ Opposite.op d'))) x✝)
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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
d : D
⊢ IsIso (adj.unit.app ((ihom d).obj (R.obj c)))

Tactic:
revert c d

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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
⊢ ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((curriedTensor C).map f))
⊢ (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((tensoringLeft C).map f))

Tactic:
← vcomp2

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((curriedTensor C).map f))
⊢ (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f))
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✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                    ((unitCompPartialBijective A ⋯)
                      (curry
                        ((β_ A B).inv ≫ ((reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map (f ≫ g)) ≫ 𝟙 (i.obj X')))) ≫
                  𝟙 (i.obj X')))) ≫
        𝟙 (i.obj X') =
    i.map
        (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X))) ≫
      i.map g

Tactic:
Adjunction.homEquiv_unit

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✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                    ((unitCompPartialBijective A ⋯)
                      (curry
                        ((β_ A B).inv ≫ ((reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map (f ≫ g)) ≫ 𝟙 (i.obj X')))) ≫
                  𝟙 (i.obj X')))) ≫
        𝟙 (i.obj X') =
    i.map
        (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry
                              ((β_ A B).inv ≫ ((reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f) ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X))) ≫
      i.map g
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 H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c j : C
⊢ Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      ℌ.π c j =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c))

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

Goal state after: