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

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
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ F.map ((𝟭 C).map x✝) = F.map (eqToHom ⋯ ≫ (F ⋙ F.strictInv).map x✝ ≫ eqToHom ⋯)

Tactic:
by

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
hφ : Function.Injective φ.obj
S : Subgroupoid C
⊢ ∀ {c d : D} {p : c ⟶ d}, p ∈ {x | Map.Arrows φ hφ S c d x} → Groupoid.inv p ∈ {x | Map.Arrows φ hφ S d c x}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

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
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
x : D
⊢ (F.strictInv ⋙ F).obj x = (𝟭 D).obj x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

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
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsIso
inst✝ : G.IsIso
x✝² x✝¹ : D
x✝ : x✝² ⟶ x✝¹
⊢ (F.strictInv ⋙ F).map x✝ = eqToHom ⋯ ≫ (𝟭 D).map x✝ ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

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
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
X : C
⊢ e.functor.map ((eqToIso ⋯).hom.app X) ≫ (eqToIso ⋯).hom.app (e.functor.obj X) = 𝟙 (e.functor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

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
F : C ⥤ D
G : D ⥤ E
e : C ≌ D
h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X
h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y
k : ∀ (X : C), e.unitIso.hom.app X = eqToHom ⋯
k' : ∀ (Y : D), e.counitIso.hom.app Y = eqToHom ⋯
⊢ ∀ (X : C), (𝟭 C).obj X = (e.functor ⋙ e.inverse).obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

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
F : C ⥤ D
G : D ⥤ E
e : C ≌ D
h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X
h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y
k : ∀ (X : C), e.unitIso.hom.app X = eqToHom ⋯
k' : ∀ (Y : D), e.counitIso.hom.app Y = eqToHom ⋯
⊢ ∀ (X : D), (e.inverse ⋙ e.functor).obj X = (𝟭 D).obj X

Tactic:
by

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
hφ : Function.Injective φ.obj
S : Subgroupoid C
⊢ ∀ {c d e : D} {p : c ⟶ d},
    p ∈ {x | Map.Arrows φ hφ S c d x} →
      ∀ {q : d ⟶ e}, q ∈ {x | Map.Arrows φ hφ S d e x} → p ≫ q ∈ {x | Map.Arrows φ hφ S c e x}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    𝟙 (P ⊞ P.complement)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.lift P.decompId_p P.complement.decompId_p ≫ biprod.desc P.decompId_i P.complement.decompId_i =
    𝟙 ((toKaroubi C).obj P.X)

Tactic:
by

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
⊢ GaloisConnection (map φ hφ) (comap φ)

Tactic:
by

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
hφ : Function.Injective φ.obj
d : D
⊢ d ∈ (map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d

Tactic:
by

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
hφ : Function.Injective φ.obj
⊢ (map φ hφ S).objs = φ.obj '' S.objs

Tactic:
by

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
c d : D
f : c ⟶ d
⊢ f ∈ (im φ hφ).arrows c d ↔ ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
by

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
d : D
⊢ d ∈ (im φ hφ).objs ↔ ∃ c, φ.obj c = d

Tactic:
by

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
hφ' : im φ hφ = ⊤
d : D
⊢ d ∈ ⊤.objs

Tactic:
apply mem_top_objs

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
hφ' : im φ hφ = ⊤
⊢ Function.Surjective φ.obj

Tactic:
by

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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d : D
⊢ 𝟙 d ∈ (map φ hφ S).arrows d d

Tactic:
by

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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
⊢ d' ∈ ⊤.objs

Tactic:
apply mem_top_objs

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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
⊢ d' ∈ (im φ hφ).objs

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ i₁ + i₃ + i₂ = k

Tactic:
by

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
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
g : φ.obj c ⟶ φ.obj c'
⊢ g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c')

Tactic:
by

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
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') (φ.map (Groupoid.inv f ≫ γ ≫ f))
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
by

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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d d' : D
g : d ⟶ d'
δ : d ⟶ d
hδ : δ ∈ (map φ hφ S).arrows d d
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
x✝ : op (left a✝¹) ⟶ op (left a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (left a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (left a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
x✝ : op (right a✝¹) ⟶ op (left a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (left a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (right a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ {f | c = d ∧ f ∈ S.arrows c d} → Groupoid.inv p ∈ {f | d = c ∧ f ∈ S.arrows d c}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d e : C} {p : c ⟶ d},
    p ∈ {f | c = d ∧ f ∈ S.arrows c d} →
      ∀ {q : d ⟶ e}, q ∈ {f | d = e ∧ f ∈ S.arrows d e} → p ≫ q ∈ {f | c = e ∧ f ∈ S.arrows c e}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.disconnect ≤ S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.disconnect.IsTotallyDisconnected

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
x✝ : op (right a✝¹) ⟶ op (right a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (right a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (right a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ {_f | c ∈ D ∧ d ∈ D} → Groupoid.inv p ∈ {_f | d ∈ D ∧ c ∈ D}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
D : Set C
⊢ ∀ {c d e : C} {p : c ⟶ d},
    p ∈ {_f | c ∈ D ∧ d ∈ D} → ∀ {q : d ⟶ e}, q ∈ {_f | d ∈ D ∧ e ∈ D} → p ≫ q ∈ {_f | c ∈ D ∧ e ∈ D}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
D : Set C
c : C
⊢ c ∈ (full D).objs ↔ c ∈ D

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
⊢ full ∅ = ⊥

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
⊢ full univ = ⊤

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ⊆ E
⊢ full D ≤ full E

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝ : C
⊢ (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.map
        ((NatIso.ofComponents
                (fun x ↦
                  match x with
                  | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
                  | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a))))
                ⋯).hom.app
          (op (left a✝))) ≫
      (NatIso.ofComponents
              (fun x ↦
                match x with
                | left a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (left a))
                | right a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (right a)))
              ⋯).hom.app
        ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp.obj
          (op (left a✝))) =
    𝟙
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.obj
        (op (left a✝)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
⊢ (associator X Y Z).inv ≫ (braiding (tensorObj X Y) Z).hom ≫ (associator Z X Y).inv =
    whiskerLeft X (braiding Y Z).hom ≫ (associator X Z Y).inv ≫ whiskerRight (braiding X Z).hom Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝⁵ : AddCommMonoid I
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : MonoidalCategory C
X Y : GradedObject I C
inst✝² : SymmetricCategory C
inst✝¹ : X.HasTensor Y
inst✝ : Y.HasTensor X
⊢ (braiding X Y).hom ≫ (braiding Y X).hom = 𝟙 (tensorObj X Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Opposites

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝ : D
⊢ (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.map
        ((NatIso.ofComponents
                (fun x ↦
                  match x with
                  | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
                  | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a))))
                ⋯).hom.app
          (op (right a✝))) ≫
      (NatIso.ofComponents
              (fun x ↦
                match x with
                | left a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (left a))
                | right a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (right a)))
              ⋯).hom.app
        ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp.obj
          (op (right a✝))) =
    𝟙
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.obj
        (op (right a✝)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Join.Sum

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
x y : C ⊕ D
h h' : x ⟶ y
heq : (fromSum C D).map h = (fromSum C D).map h'
⊢ h = h'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasPullbacks C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty X.hom (Opposite.op Y ⋔ Z).hom

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial A
⊢ HasLiftingProperty (Arrow.mk (i.to B) □ Arrow.mk g).hom h ↔ HasLiftingProperty g ((ihom B).map h)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
f : A ⟶ B
h : X ⟶ Y
i : IsInitial K
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk (i.to L)).hom h ↔ HasLiftingProperty f ((ihom L).map h)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : HasPullbacks C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom (t.from X) ↔ HasLiftingProperty g ((MonoidalClosed.pre f).app X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
g : K ⟶ L
i : IsInitial A
t : IsTerminal Y
⊢ HasLiftingProperty (Arrow.mk (i.to B) □ Arrow.mk g).hom (t.from X) ↔ HasLiftingProperty g (t.from (B ⟹ X))

Tactic:
by

Goal state after: