mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasFunctorEnrichedHom V F₁ F₂
X✝ Y✝ Z✝ : J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : Under Z✝
⊢ enrichedHomπ V (Under.forget X✝ ⋙ F₁) (Under.forget X✝ ⋙ F₂) ((Under.map (f ≫ g)).obj j) =
    enrichedHomπ V (Under.forget X✝ ⋙ F₁) (Under.forget X✝ ⋙ F₂) ((Under.map f).obj ((Under.map g).obj j))

Tactic:
congr 1

Goal state after:
case e_12
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasFunctorEnrichedHom V F₁ F₂
X✝ Y✝ Z✝ : J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : Under Z✝
⊢ (Under.map (f ≫ g)).obj j = (Under.map f).obj ((Under.map g).obj j)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasFunctorEnrichedHom V F₁ F₂
X✝ Y✝ Z✝ : J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X✝ ⋙ F₁))
      (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X✝ ⋙ F₂)) =
    precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X✝ ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget X✝ ⋙ F₂)) ≫
      precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y✝ ⋙ F₁))
        (Iso.refl (Under.map g ⋙ Under.forget Y✝ ⋙ F₂))

Tactic:
ext j
    -- this was produced by `simp?`
    simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π,
      Under.map_obj_right, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
      eHomWhiskerLeft_id, comp_id, assoc]
    congr 1
    simp [Under.map, Comma.mapLeft]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case h
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf : (fiberInclusion.map f).base = 𝟙 S
⊢ (Fiber.inducedFunctor ⋯).map
      ((fiberInclusion.map f).fiber ≫ eqToHom ⋯ ≫ (F.mapId { as := op S }).hom.toNatTrans.app Y) =
    f

Tactic:
ext <;> simp [hf, ← Cat.Hom₂.comp_app]

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

Goal state before:
pp: case refine_2
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.FintypeCat.ofMulAction G X).V.obj
⊢ ∃ a, (ConcreteCategory.hom i.hom) a = x'

Tactic:
· let x : X := i.hom y
        obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq G x x'
        use σ • y
        change (Y.ρ σ ≫ i.hom) y = x'
        rw [i.comm, FintypeCat.comp_apply]
        exact hσ

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a ↦ F.map f.hom ≫ (a f.right).hom

Tactic:
by fun_prop

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
f : Arrow C
⊢ Continuous fun a ↦ (a f.left).hom ≫ F.map f.hom

Tactic:
by fun_prop

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
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous fun p ↦ X.obj.V.uSwitchEquiv.symm p

Tactic:
by fun_prop

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
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X : ContAction FintypeCat (Aut F')
⊢ Continuous fun p ↦ (p.1, X.obj.V.uSwitchEquiv p.2)

Tactic:
by fun_prop

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

Goal state before:
pp: C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f ≫ inv g ≫ g = f ≫ inv f ≫ g

Tactic:
congr 1

Goal state after:
case e_a
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ inv g ≫ g = inv f ≫ g
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝¹ : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this✝ : ∀ (i : ι), DiscreteTopology (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : G × (f i).V.obj → G × X.V.obj := fun p ↦ (p.1, (ConcreteCategory.hom r.hom) p.2)
q : G × X.V.obj → X.V.obj := fun p ↦ (ConcreteCategory.hom (X.ρ p.1).hom) p.2
q' : G × (f i).V.obj → (f i).V.obj := fun p ↦ (ConcreteCategory.hom ((f i).ρ p.1).hom) p.2
heq : q ∘ r'' = ⇑(ConcreteCategory.hom r.hom) ∘ q'
hrinj : Function.Injective ⇑(ConcreteCategory.hom r.hom)
t₁ : TopologicalSpace (G × (f i).V.obj) := inferInstance
this : TopologicalSpace.induced (⇑(ConcreteCategory.hom r.hom)) inferInstance = ⊥
⊢ Continuous r''

Tactic:
by fun_prop

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

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f ↔
    ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
by
  constructor
  · rintro ⟨g, hg⟩; exact ⟨_, _, g, rfl, rfl, hg, eq_conj_eqToHom _⟩
  · rintro ⟨a, b, g, rfl, rfl, hg, rfl⟩; rw [← eq_conj_eqToHom]; constructor; exact hg

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

Goal state before:
pp: case pos
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 < n
h✝ : m < n + 1
⊢ M m = M m

pp: case neg
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 < n
h✝ : ¬m < n + 1
⊢ N m = M m

Tactic:
rfl; try lia

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

Goal state before:
pp: case refine_2
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 < n
h' : m < n + 1
⊢ M m = M m

Tactic:
rfl; try lia

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

Goal state before:
pp: case refine_3
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 < n
h' : m < n + 1
⊢ N m = N m

Tactic:
rfl; try lia

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

Goal state before:
pp: case refine_4
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 < n
h' : ¬m < n + 1
⊢ N m = N m

Tactic:
rfl; try lia

Goal state after:
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 ⋯
⊢ functorMap f (m + 1) ≫
      (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:
congr 1

Goal state after:
case e_a
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 ⋯ =
    Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯
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)
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
m : s.pt ⟶ (wedge F).pt
h : ∀ (j : WalkingMulticospan (multicospanShapeEnd J)), m ≫ (wedge F).π.app j = s.π.app j
x : s.pt
j : J
⊢ ↑((hom m).toFun x) j = ↑((hom (↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩)).toFun x) j

Tactic:
exact ConcreteCategory.congr_hom (h (.left j)) x

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

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
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
⊢ BraidedCategory (LocalizedMonoidal L W ε)

Tactic:
by
  refine .ofBifunctor (braidingNatIso L W ε) ?_ ?_
  · apply natTrans₃_ext (L') (L') (L') W W W
    simpa using! map_hexagon_forward _ _ _
  · apply natTrans₃_ext (L') (L') (L') W W W
    simpa using! map_hexagon_reverse _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ Functor.whiskerRight (pushforwardId I).hom (pullback (𝟙 I)) ≫ (pullbackPushforwardAdj (𝟙 I)).counit =
    (pullbackPushforwardAdj (𝟙 I)).counit

Tactic:
rw [pushforwardId, Adjunction.rightAdjointUniq_hom_counit]

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
A' A : C
X : Over I
g : A' ⟶ A
v : A ⟶ (sections I).obj X
⊢ homMk ((β_ A' I).hom ≫ uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯ =
    homMk (g ▷ I ≫ (β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯

Tactic:
congr 1

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
A' A : C
X : Over I
g : A' ⟶ A
v : A ⟶ (sections I).obj X
⊢ (β_ A' I).hom ≫ uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom)) =
    g ▷ I ≫ (β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x : C
⊢ (λ_ ((curriedActionMop C D).obj x)).inv =
    (curriedActionMop C D).map (λ_ x).inv ≫
      Quiver.Hom.mop { app := fun x_1 ↦ (αₗ (𝟙_ C) x x_1).hom, naturality := ⋯ } ≫
        (actionUnitNatIso C D).hom.mop ▷ (curriedActionMop C D).obj x

Tactic:
apply MonoidalOpposite.hom_ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x : C
⊢ (λ_ ((curriedActionMop C D).obj x)).inv.unmop =
    ((curriedActionMop C D).map (λ_ x).inv ≫
        Quiver.Hom.mop { app := fun x_1 ↦ (αₗ (𝟙_ C) x x_1).hom, naturality := ⋯ } ≫
          (actionUnitNatIso C D).hom.mop ▷ (curriedActionMop C D).obj x).unmop
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x : C
⊢ (ρ_ ((curriedActionMop C D).obj x)).inv =
    (curriedActionMop C D).map (ρ_ x).inv ≫
      Quiver.Hom.mop { app := fun x_1 ↦ (αₗ x (𝟙_ C) x_1).hom, naturality := ⋯ } ≫
        (curriedActionMop C D).obj x ◁ (actionUnitNatIso C D).hom.mop

Tactic:
apply MonoidalOpposite.hom_ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
x : C
⊢ (ρ_ ((curriedActionMop C D).obj x)).inv.unmop =
    ((curriedActionMop C D).map (ρ_ x).inv ≫
        Quiver.Hom.mop { app := fun x_1 ↦ (αₗ x (𝟙_ C) x_1).hom, naturality := ⋯ } ≫
          (curriedActionMop C D).obj x ◁ (actionUnitNatIso C D).hom.mop).unmop
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
W X Y Z : Arrow C
⊢ (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom = (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
  apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext (by simp)
  apply ((tensorRight _ ⋙ tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;>
  simp [associator_naturality_left_assoc]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
      Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
      Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

Tactic:
apply ((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

Goal state after:
case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ (tensorLeft X.right).map
        (pushout.inl (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    (tensorLeft X.right).map
        (pushout.inl (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ (tensorLeft X.right).map
        (pushout.inr (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    (tensorLeft X.right).map
        (pushout.inr (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ yoneda.obj (G ⊗ H) ⟶ yoneda.obj H

Tactic:
refine ⟨fun X ↦ ↾fun x ↦ h' _ (x ≫ fst _ _) (x ≫ snd _ _), fun X Y f ↦ ?_⟩
      ext
      simp [← cancel_mono φ, hh', comp_mul, comp_inv]

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
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:
by
  revert c d
  rw [((isIso_tfae adj).out 0 3 :)]
  intro d d'
  infer_instance

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

Goal state before:
pp: case e'_3.h_fst
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 ◁ fst R R ≫ μ = lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ

Tactic:
congr 1

Goal state after:
case e'_3.h_fst.e_a
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 ◁ fst R R = lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R)
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: case h_snd
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 ◁ snd R R ≫ μ = lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ

Tactic:
congr 1

Goal state after:
case h_snd.e_a
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 ◁ snd R R = lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R)
Module: Mathlib.CategoryTheory.Monoidal.Ring

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

Tactic:
congr 1

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

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

Tactic:
congr 1

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