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

Goal state before:
pp: G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ (ConcreteCategory.hom (X.ρ g⁻¹ ≫ f.hom)) x = (ConcreteCategory.hom (Y.ρ g⁻¹ * Y.ρ g).hom) ↑y

Tactic:
rw [f.comm, FintypeCat.comp_apply, h]

Goal state after:
G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ (ConcreteCategory.hom (Y.ρ g⁻¹)) ((ConcreteCategory.hom (Y.ρ g).hom) ↑y) =
    (ConcreteCategory.hom (Y.ρ g⁻¹ * Y.ρ g).hom) ↑y
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
σ τ : Aut F
hst : σ ≈ τ
⊢ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧ =
    (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦τ⟧

Tactic:
by
      let J' := quotientDiag V h u ⋙ functorToAction F
      let m : End (SingleObj.star (V.toSubgroup ⧸ Subgroup.subgroupOf U V)) :=
        ⟦⟨σ⁻¹ * τ, (QuotientGroup.leftRel_apply).mp hst⟩⟧
      have h1 : J'.map m ≫ s.ι.app (SingleObj.star _) = s.ι.app (SingleObj.star _) :=
        s.ι.naturality m
      conv_rhs => rw [← h1]
      have h2 : (J'.map m).hom (u.inv.hom ⟦τ⟧) = u.inv.hom ⟦σ⟧ := by
        simp [J', functorToAction_map_quotientToEndObjectHom V h u m, ← comp_apply, m]
      simp [← h2, J']

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
x✝¹ x✝ : Quiver.FreeGroupoid C
f g : x✝¹ ⟶ x✝
r : homRel C f g
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map f = (Quiver.FreeGroupoid.lift φ.toPrefunctor).map g

Tactic:
by
      have {X Y : C} (f : X ⟶ Y) :=
        Prefunctor.congr_hom (Quiver.FreeGroupoid.lift_spec φ.toPrefunctor) f
      induction r <;> cat_disch

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

Goal state before:
pp: G : Type u₁
inst✝ : Groupoid G
⊢ 𝟭 (FreeGroupoid G) = lift (of G)

Tactic:
apply lift_unique

Goal state after:
G : Type u₁
inst✝ : Groupoid G
⊢ of G ⋙ 𝟭 (FreeGroupoid G) = of G
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:
apply lift_unique

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : Type u₁
inst✝¹ : Groupoid G
H : Type u₂
inst✝ : Groupoid H
φ : C ⥤ G
ψ : G ⥤ H
⊢ of C ⋙ lift φ ⋙ ψ = φ ⋙ ψ
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ 𝟭 (FreeGroupoid C) = map (𝟭 C)

Tactic:
apply lift_unique

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ of C ⋙ 𝟭 (FreeGroupoid C) = 𝟭 C ⋙ of C
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Category.{v₂, u₂} E
φ : C ⥤ D
φ' : D ⥤ E
⊢ map φ ⋙ map φ' = map (φ ⋙ φ')

Tactic:
apply lift_unique

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Category.{v₂, u₂} E
φ : C ⥤ D
φ' : D ⥤ E
⊢ of C ⋙ map φ ⋙ map φ' = (φ ⋙ φ') ⋙ of E
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

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

Tactic:
apply lift_unique

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Groupoid E
F : C ⥤ D
G : D ⥤ E
⊢ of C ⋙ map F ⋙ lift G = F ⋙ G
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
⊢ 𝟭 (Quiver.FreeGroupoid V) = lift (𝟭q V ⋙q of V)

Tactic:
apply lift_unique

Goal state after:
V : Type u
inst✝ : Quiver V
⊢ of V ⋙q (𝟭 (Quiver.FreeGroupoid V)).toPrefunctor = 𝟭q V ⋙q of V
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')

Tactic:
apply lift_unique

Goal state after:
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
⊢ (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).ρ σ =
    𝟙 (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V

Tactic:
refine FintypeCat.hom_ext _ _ (fun x ↦ ?_)

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
x : (fun X ↦ X.obj) (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V
⊢ (ConcreteCategory.hom
        ((Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).ρ σ))
      x =
    (ConcreteCategory.hom
        (𝟙 (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V))
      x
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
⊢ ↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))) = 𝟙 (F.obj x✝ ⊕ G.obj x✝)

Tactic:
ext ⟨⟩

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
val✝ : F.obj x✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))))).toFun (Sum.inl val✝) =
    (hom (𝟙 (F.obj x✝ ⊕ G.obj x✝))).toFun (Sum.inl val✝)

case inr
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
val✝ : G.obj x✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))))).toFun (Sum.inr val✝) =
    (hom (𝟙 (F.obj x✝ ⊕ G.obj x✝))).toFun (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))) =
    ↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝))

Tactic:
ext ⟨⟩

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
val✝ : F.obj X✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))))).toFun (Sum.inl val✝) =
    (hom (↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝)))).toFun
      (Sum.inl val✝)

case inr
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
val✝ : G.obj X✝
⊢ (hom (↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))))).toFun (Sum.inr val✝) =
    (hom (↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝)))).toFun
      (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ (coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)) =
    ↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝

Tactic:
ext ⟨⟩

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
val✝ : F₁.obj x✝²
⊢ (hom ((coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)))).toFun (Sum.inl val✝) =
    (hom (↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝)).toFun (Sum.inl val✝)

case inr
C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
val✝ : F₂.obj x✝²
⊢ (hom ((coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)))).toFun (Sum.inr val✝) =
    (hom (↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝)).toFun (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: 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))
⊢ ∀ (j : ℕᵒᵖ),
    (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
        (cone f).π.app j =
      s.π.app j

Tactic:
intro ⟨n⟩
    apply Pi.hom_ext
    intro m
    by_cases h : m < n
    · simp only [Category.assoc, cone_π_app_comp_Pi_π_pos f _ _ h]
      simp only [dite_eq_ite, limit.lift_π_assoc,
        Discrete.functor_obj_eq_as, Fan.mk_π_app, Category.assoc, eqToHom_trans]
      have hh : m + 1 ≤ n := by lia
      rw [← s.w (homOfLE hh).op]
      simp only [homOfLE_leOfHom, Category.assoc]
      congr
      induction hh using Nat.leRec with
      | refl => simp
      | @le_succ_of_le n hh ih =>
        have : homOfLE (Nat.le_succ_of_le hh) = homOfLE hh ≫ homOfLE (Nat.le_succ n) := by simp
        rw [this, op_comp, Functor.map_comp]
        simp only [Nat.succ_eq_add_one, homOfLE_leOfHom,
          Functor.ofOpSequence_map_homOfLE_succ, Category.assoc]
        have h₁ : (if _ : m < m + 1 then M m else N m) = if _ : m < n then M m else N m := by
          rw [dif_pos (by lia), dif_pos (by lia)]
        have h₂ : (if _ : m < n then M m else N m) = if _ : m < n + 1 then M m else N m := by
          rw [dif_pos h, dif_pos (by lia)]
        rw [← eqToHom_trans h₁ h₂]
        slice_lhs 2 4 => rw [ih (by lia)]
        simp only [functorMap, dite_eq_ite, Pi.π, Pi.map_π_assoc]
        split_ifs
        rw [dif_pos (by lia)]
        simp
    · simp only [Category.assoc]
      rw [cone_π_app_comp_Pi_π_neg f _ _ h]
      simp only [dite_eq_ite, limit.lift_π_assoc,
        Discrete.functor_obj_eq_as, Fan.mk_π_app, Category.assoc]
      slice_lhs 2 4 => simp only [← dite_eq_ite, ← functorMap_commSq f h]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hₗ
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 : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).fst = (β.app x).fst

pp: case hᵣ
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 : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).snd = (β.app x).snd

Tactic:
· exact congrArg (fun t ↦ t.app x) e₁

Goal state after:
case hᵣ
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 : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
x : X
⊢ (α.app x).snd = (β.app x).snd
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)
X✝ Y✝ : Over I
u : X✝ ⟶ Y✝
⊢ (ihom I).map X✝.hom ≫ 𝟙 ((ihom I).obj I) = (ihom I).map (Hom.left u) ≫ (ihom I).map Y✝.hom

Tactic:
by simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (Δ ≫ (f ≫ inv f ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)
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
x y : C
z z' : D
f : z ⟶ z'
⊢ 𝟙 (x ⊗ y) ⊙ₗₘ f = ((αₗ x y z).hom ≫ (𝟙 x ⊙ₗₘ 𝟙 y ⊙ₗₘ f)) ≫ (αₗ x y z').inv

Tactic:
← actionAssocIso_hom_naturality

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 C
inst✝ : MonoidalLeftAction C D
x y : C
z z' : D
f : z ⟶ z'
⊢ 𝟙 (x ⊗ y) ⊙ₗₘ f = (((𝟙 x ⊗ₘ 𝟙 y) ⊙ₗₘ f) ≫ (αₗ x y z').hom) ≫ (αₗ x y z').inv
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
z z' : D
f : z ⟶ z'
x y : C
⊢ f ⊙ᵣₘ 𝟙 (x ⊗ y) = ((αᵣ z x y).hom ≫ ((f ⊙ᵣₘ 𝟙 x) ⊙ᵣₘ 𝟙 y)) ≫ (αᵣ z' x y).inv

Tactic:
← actionAssocIso_hom_naturality

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 C
inst✝ : MonoidalRightAction C D
z z' : D
f : z ⟶ z'
x y : C
⊢ f ⊙ᵣₘ 𝟙 (x ⊗ y) = ((f ⊙ᵣₘ 𝟙 x ⊗ₘ 𝟙 y) ≫ (αᵣ z' x y).hom) ≫ (αᵣ z' x y).inv
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✝ : MonoidalRightAction C D
x : C
t : D
⊢ (λ_ ((curriedAction C D).obj x)).inv.app t =
    ((curriedAction C D).map (λ_ x).inv ≫
          { app := fun x_1 ↦ (αᵣ x_1 (𝟙_ C) x).hom, naturality := ⋯ } ≫
            (actionUnitNatIso C D).hom ▷ (curriedAction C D).obj x).app
      t

Tactic:
simpa [-actionHom_leftUnitor] using
      t ⊴ᵣ (λ_ x).inv ≫= actionHom_leftUnitor x t

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ᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop c'✝ ⟶ unop c✝
g : unop d'✝ ⟶ unop d✝
⊢ (Quiver.Hom.unop (op f) ⊙ₗₘ Quiver.Hom.unop (op g)).op =
    (Quiver.Hom.unop (op f) ⊵ₗ unop d✝).op ≫ (unop c'✝ ⊴ₗ Quiver.Hom.unop (op g)).op

Tactic:
apply Quiver.Hom.unop_inj

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

Tactic:
apply Quiver.Hom.unop_inj

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
c₁✝ c₂✝ c₃✝ c₄✝ : Cᵒᵖ
d₁✝ d₂✝ : Dᵒᵖ
f : unop c₂✝ ⟶ unop c₁✝
g : unop c₄✝ ⟶ unop c₃✝
h : unop d₂✝ ⟶ unop d₁✝
⊢ (((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
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
d✝ d'✝ : Dᵒᵖ
x✝ : d✝ ⟶ d'✝
⊢ (λₗ (unop d✝)).symm.op.hom ≫ x✝ = (unop (𝟙_ Cᵒᵖ) ⊴ₗ x✝.unop).op ≫ (λₗ (unop d'✝)).symm.op.hom

Tactic:
apply Quiver.Hom.unop_inj

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
d✝ d'✝ : Dᵒᵖ
x✝ : d✝ ⟶ d'✝
⊢ ((λₗ (unop d✝)).symm.op.hom ≫ x✝).unop = ((unop (𝟙_ Cᵒᵖ) ⊴ₗ x✝.unop).op ≫ (λₗ (unop d'✝)).symm.op.hom).unop
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'✝ x✝² : Cᵒᵖ
x✝¹ : c✝ ⟶ c'✝
x✝ : Dᵒᵖ
⊢ ((x✝¹ ▷ x✝²).unop ⊵ₗ unop x✝).op =
    (αₗ (unop c✝) (unop x✝²) (unop x✝)).symm.op.hom ≫
      (x✝¹.unop ⊵ₗ unop (op (unop x✝² ⊙ₗ unop x✝))).op ≫ (αₗ (unop c'✝) (unop x✝²) (unop x✝)).symm.op.inv

Tactic:
apply Quiver.Hom.unop_inj

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
c✝ c'✝ x✝² : Cᵒᵖ
x✝¹ : c✝ ⟶ c'✝
x✝ : Dᵒᵖ
⊢ ((x✝¹ ▷ x✝²).unop ⊵ₗ unop x✝).op.unop =
    ((αₗ (unop c✝) (unop x✝²) (unop x✝)).symm.op.hom ≫
        (x✝¹.unop ⊵ₗ unop (op (unop x✝² ⊙ₗ unop x✝))).op ≫ (αₗ (unop c'✝) (unop x✝²) (unop x✝)).symm.op.inv).unop
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
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((α_ x✝³ x✝² x✝¹).hom.unop ⊵ₗ unop x✝).op ≫
      (αₗ (unop x✝³) (unop (x✝² ⊗ x✝¹)) (unop x✝)).symm.op.hom ≫
        (unop x✝³ ⊴ₗ (αₗ (unop x✝²) (unop x✝¹) (unop x✝)).symm.op.hom.unop).op =
    (αₗ (unop (x✝³ ⊗ x✝²)) (unop x✝¹) (unop x✝)).symm.op.hom ≫
      (αₗ (unop x✝³) (unop x✝²) (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom

Tactic:
apply Quiver.Hom.unop_inj

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✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (((α_ x✝³ x✝² x✝¹).hom.unop ⊵ₗ unop x✝).op ≫
        (αₗ (unop x✝³) (unop (x✝² ⊗ x✝¹)) (unop x✝)).symm.op.hom ≫
          (unop x✝³ ⊴ₗ (αₗ (unop x✝²) (unop x✝¹) (unop x✝)).symm.op.hom.unop).op).unop =
    ((αₗ (unop (x✝³ ⊗ x✝²)) (unop x✝¹) (unop x✝)).symm.op.hom ≫
        (αₗ (unop x✝³) (unop x✝²) (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom).unop
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
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((λ_ x✝¹).hom.unop ⊵ₗ unop x✝).op =
    (αₗ (unop (𝟙_ Cᵒᵖ)) (unop x✝¹) (unop x✝)).symm.op.hom ≫ (λₗ (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom

Tactic:
apply Quiver.Hom.unop_inj

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ᵒᵖ
x✝ : Dᵒᵖ
⊢ ((λ_ x✝¹).hom.unop ⊵ₗ unop x✝).op.unop =
    ((αₗ (unop (𝟙_ Cᵒᵖ)) (unop x✝¹) (unop x✝)).symm.op.hom ≫ (λₗ (unop (op (unop x✝¹ ⊙ₗ unop x✝)))).symm.op.hom).unop
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
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((ρ_ x✝¹).hom.unop ⊵ₗ unop x✝).op =
    (αₗ (unop x✝¹) (unop (𝟙_ Cᵒᵖ)) (unop x✝)).symm.op.hom ≫ (unop x✝¹ ⊴ₗ (λₗ (unop x✝)).symm.op.hom.unop).op

Tactic:
apply Quiver.Hom.unop_inj

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ᵒᵖ
x✝ : Dᵒᵖ
⊢ ((ρ_ x✝¹).hom.unop ⊵ₗ unop x✝).op.unop =
    ((αₗ (unop x✝¹) (unop (𝟙_ Cᵒᵖ)) (unop x✝)).symm.op.hom ≫ (unop x✝¹ ⊴ₗ (λₗ (unop x✝)).symm.op.hom.unop).op).unop
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
c✝ c'✝ : Cᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop d'✝ ⟶ unop d✝
g : unop c'✝ ⟶ unop c✝
⊢ (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op =
    (Quiver.Hom.unop (op f) ⊵ᵣ unop c✝).op ≫ (unop d'✝ ⊴ᵣ Quiver.Hom.unop (op g)).op

Tactic:
apply Quiver.Hom.unop_inj

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✝ : MonoidalRightAction C D
c✝ c'✝ : Cᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop d'✝ ⟶ unop d✝
g : unop c'✝ ⟶ unop c✝
⊢ (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op.unop =
    ((Quiver.Hom.unop (op f) ⊵ᵣ unop c✝).op ≫ (unop d'✝ ⊴ᵣ Quiver.Hom.unop (op g)).op).unop