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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ X ∈ ⋃ X, Set.range (ff X), IsConnected X

Tactic:
rintro X ⟨A, ⟨Y, rfl⟩, hA2⟩
    obtain ⟨i, rfl⟩ := hA2
    exact h5 Y i

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

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ ∀ i ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, X c d ⊆ i.arrows c d

Tactic:
exact fun S hS f fS => hS _ _ fS

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
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ p✝ ≫ q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj e✝)}

Tactic:
simp only [mem_ofPred, Functor.map_comp]

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map p✝ ≫ φ.map q✝ ∈ S.arrows (φ.obj c✝) (φ.obj e✝)
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
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
this : Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
exact this

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✝¹ : (j : J✝) → (F✝.obj (op j)).obj j ⟶ X✝
hf✝ : ∀ ⦃i j : J✝⦄ (g : i ⟶ j), (F✝.map g.op).app i ≫ f✝¹ i = (F✝.obj (op j)).map g ≫ f✝¹ j
J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
⊢ (π F j ≫ (f.app (op j)).app j) ≫ (G.obj (op j)).map φ = (π F j' ≫ (f.app (op j')).app j') ≫ (G.map φ.op).app j'

Tactic:
have e := (f.app (op j)).naturality φ

Goal state after:
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✝¹ : (j : J✝) → (F✝.obj (op j)).obj j ⟶ X✝
hf✝ : ∀ ⦃i j : J✝⦄ (g : i ⟶ j), (F✝.map g.op).app i ≫ f✝¹ i = (F✝.obj (op j)).map g ≫ f✝¹ j
J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ (f.app (op j)).app j' = (f.app (op j)).app j ≫ (G.obj (op j)).map φ
⊢ (π F j ≫ (f.app (op j)).app j) ≫ (G.obj (op j)).map φ = (π F j' ≫ (f.app (op j')).app j') ≫ (G.map φ.op).app j'
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq biprod.fst biprod.snd 0 0

Tactic:
convert! of_is_biproduct₁ (BinaryBiproduct.isBilimit X Y)

Goal state after:
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:
rw [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.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ (F.leftOp ⋙ shrinkYoneda.{w, v, u}).map f ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm (↑s (unop j₁)) ≫ ((Functor.const Jᵒᵖ).obj P).map f

Tactic:
by
        rw [← s.property f.unop]
        dsimp
        rw [shrinkYonedaEquiv_symm_map, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: J : Type w
inst✝⁴ : Finite J
C : J → Type u₁
D : J → Type u₂
inst✝³ : (j : J) → Category.{v₁, u₁} (C j)
inst✝² : (j : J) → Category.{v₂, u₂} (D j)
L : (j : J) → C j ⥤ D j
W : (j : J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : J), (W j).ContainsIdentities
inst✝ : ∀ (j : J), (L j).IsLocalization (W j)
⊢ (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
revert J

Goal state after:
⊢ ∀ {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
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✝ : SymmetricCategory C
⊢ SymmetricCategory (LocalizedMonoidal L W ε)

Tactic:
refine .ofCurried (natTrans₂_ext (L') (L') W W fun X Y ↦ ?_)

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : SymmetricCategory C
X Y : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: 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
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (e₁.inv ≫ e₁.hom ⊗ₘ e₂.inv ≫ e₂.hom))

Tactic:
Iso.inv_hom_id,

Goal state after:
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
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (𝟙 (L.obj X₁) ⊗ₘ e₂.inv ≫ e₂.hom))
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: 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
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (𝟙 (L.obj X₁) ⊗ₘ e₂.inv ≫ e₂.hom))

Tactic:
Iso.inv_hom_id,

Goal state after:
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
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂ ≫ (𝟙 (L.obj X₁) ⊗ₘ 𝟙 (L.obj X₂)))
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 : C
y z : D
f : y ≅ z
⊢ x ⊴ₗ (f.inv ≫ f.hom) = 𝟙 (x ⊙ₗ z)

Tactic:
Iso.inv_hom_id,

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 : C
y z : D
f : y ≅ z
⊢ x ⊴ₗ 𝟙 z = 𝟙 (x ⊙ₗ z)
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
f : x ≅ y
z : D
⊢ (f.inv ≫ f.hom) ⊵ₗ z = 𝟙 (y ⊙ₗ z)

Tactic:
Iso.inv_hom_id,

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
f : x ≅ y
z : D
⊢ 𝟙 y ⊵ₗ z = 𝟙 (y ⊙ₗ z)
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
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₂ c₃ : C
d : D
e :
  (Functor.OplaxMonoidal.δ F (c₁ ⊗ c₂) c₃).unmop.app d ≫
      (Functor.OplaxMonoidal.δ F c₁ c₂).unmop.app ((F.obj c₃).unmop.obj d) ≫
        𝟙 ((F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d))) =
    (F.map (α_ c₁ c₂ c₃).hom).unmop.app d ≫
      (Functor.OplaxMonoidal.δ F c₁ (c₂ ⊗ c₃)).unmop.app d ≫
        (F.obj c₁).unmop.map ((Functor.OplaxMonoidal.δ F c₂ c₃).unmop.app d)
⊢ (F.map (α_ c₁ c₂ c₃).hom).unmop.app d ≫
      ((Functor.Monoidal.μIso F c₁ (c₂ ⊗ c₃)).unmop.app d).symm.hom ≫
        (F.obj c₁).unmop.map ((Functor.Monoidal.μIso F c₂ c₃).unmop.app d).symm.hom =
    ((Functor.Monoidal.μIso F (c₁ ⊗ c₂) c₃).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.μIso F c₁ c₂).unmop.app ((F.obj c₃).unmop.obj d)).symm.hom

Tactic:
simp only [Category.comp_id] at e

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
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₂ c₃ : C
d : D
e :
  (Functor.OplaxMonoidal.δ F (c₁ ⊗ c₂) c₃).unmop.app d ≫
      (Functor.OplaxMonoidal.δ F c₁ c₂).unmop.app ((F.obj c₃).unmop.obj d) =
    (F.map (α_ c₁ c₂ c₃).hom).unmop.app d ≫
      (Functor.OplaxMonoidal.δ F c₁ (c₂ ⊗ c₃)).unmop.app d ≫
        (F.obj c₁).unmop.map ((Functor.OplaxMonoidal.δ F c₂ c₃).unmop.app d)
⊢ (F.map (α_ c₁ c₂ c₃).hom).unmop.app d ≫
      ((Functor.Monoidal.μIso F c₁ (c₂ ⊗ c₃)).unmop.app d).symm.hom ≫
        (F.obj c₁).unmop.map ((Functor.Monoidal.μIso F c₂ c₃).unmop.app d).symm.hom =
    ((Functor.Monoidal.μIso F (c₁ ⊗ c₂) c₃).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.μIso F c₁ c₂).unmop.app ((F.obj c₃).unmop.obj d)).symm.hom
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
x : D
y z : C
f : y ≅ z
⊢ x ⊴ᵣ (f.inv ≫ f.hom) = 𝟙 (x ⊙ᵣ z)

Tactic:
Iso.inv_hom_id,

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
x : D
y z : C
f : y ≅ z
⊢ x ⊴ᵣ 𝟙 z = 𝟙 (x ⊙ᵣ z)
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
x y : D
f : x ≅ y
z : C
⊢ (f.inv ≫ f.hom) ⊵ᵣ z = 𝟙 (y ⊙ᵣ z)

Tactic:
Iso.inv_hom_id,

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
x y : D
f : x ≅ y
z : C
⊢ 𝟙 y ⊵ᵣ z = 𝟙 (y ⊙ᵣ z)
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
⊢ Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom

Tactic:
Iso.inv_hom_id,

Goal state after:
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
⊢ Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
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
⊢ Q.actLeft = X.X ◁ (f.inv ≫ f.hom) ≫ Q.actLeft

Tactic:
Iso.inv_hom_id,

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

Tactic:
Iso.inv_hom_id,

Goal state after:
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
⊢ Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
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
⊢ Q.actRight = (f.inv ≫ f.hom) ▷ Y.X ≫ Q.actRight

Tactic:
Iso.inv_hom_id,

Goal state after:
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
⊢ Q.actRight = 𝟙 Q.X ▷ Y.X ≫ Q.actRight
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: case e'_3
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) ≫ μ) ≫ σ
⊢ lift (R ◁ fst 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) ≫ μ)

Tactic:
ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

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

Goal state before:
pp: case e'_3
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) ≫ μ) ≫ σ
⊢ lift (fst R 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) ≫ μ)

Tactic:
ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ uncurry
      (g.app j ≫
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
            (pre (𝟙 (F₁.obj j'))).app (F₃.obj j') ≫ eHomWhiskerLeft C (F₁.obj j') (𝟙 (F₃.obj j'))) ≫
          (pre (F₁.map φ)).app (F₃.obj j')) =
    uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ))

Tactic:
rw [pre_id, NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerLeft,
          Functor.map_id, Category.comp_id, Category.comp_id]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
          (pre (F₁.map φ)).app (F₃.obj j')) =
    uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ))
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✝² : MonoidalClosed C
A : C
inst✝¹ : Reflective i
inst✝ : ExponentialIdeal i
X : D
this : IsIso ((reflectorAdjunction i).unit.app (A ⟹ i.obj X))
⊢ (i ⋙ ihom A).obj X ≅ (i ⋙ ihom A ⋙ reflector i ⋙ i).obj X

Tactic:
apply asIso ((reflectorAdjunction i).unit.app (A ⟹ i.obj X))

Goal state after: