mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst✝¹ : HasLimit G
inst✝ : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
⊢ IsIso ((F i).map (limit.lift G c))

Tactic:
let e := IsLimit.conePointUniqueUpToIso (hc i) H

Goal state after:
C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst✝¹ : HasLimit G
inst✝ : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
e : ((F i).mapCone c).pt ≅ ((F i).mapCone (limit.cone G)).pt := (hc i).conePointUniqueUpToIso H
⊢ IsIso ((F i).map (limit.lift G c))
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
i : WalkingPair
⊢ s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt

Tactic:
cases i

Goal state after:
case left
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
⊢ s.pt ⟶ WalkingPair.casesOn WalkingPair.left c₁.pt c₂.pt

case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
⊢ s.pt ⟶ WalkingPair.casesOn WalkingPair.right c₁.pt c₂.pt
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
⊢ MonoCoprod C

Tactic:
let F := GaloisCategory.getFiberFunctor C
  exact MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono F

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
i : WalkingPair
⊢ WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt

Tactic:
cases i

Goal state after:
case left
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
⊢ WalkingPair.casesOn WalkingPair.left c₁.pt c₂.pt ⟶ s.pt

case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
⊢ WalkingPair.casesOn WalkingPair.right c₁.pt c₂.pt ⟶ s.pt
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i✝ : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
hn2 : Nat.card (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
i : ι₁ ⊕ ι₂
⊢ IsConnected (Sum.elim f₁ f₂ i)

Tactic:
cases i

Goal state after:
case h.inl
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
hn2 : Nat.card (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
val✝ : ι₁
⊢ IsConnected (Sum.elim f₁ f₂ (Sum.inl val✝))

case h.inr
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
hnn : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
hn2 : Nat.card (F.obj Z).obj < n
ι₁ : Type
f₁ : ι₁ → C
g₁ : (i : ι₁) → f₁ i ⟶ Y
hc₁ : IsColimit (Cofan.mk Y g₁)
hf₁ : ∀ (i : ι₁), IsConnected (f₁ i)
he₁ : Finite ι₁
ι₂ : Type
f₂ : ι₂ → C
g₂ : (i : ι₂) → f₂ i ⟶ Z
hc₂ : IsColimit (Cofan.mk Z g₂)
hf₂ : ∀ (i : ι₂), IsConnected (f₂ i)
he₂ : Finite ι₂
val✝ : ι₂
⊢ IsConnected (Sum.elim f₁ f₂ (Sum.inr val✝))
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
⊢ ∃ a, (functorToAction F).map a = f

Tactic:
let ψ : Z ⟶ X := g ≫ prod.fst

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
⊢ ∃ a, (functorToAction F).map a = f
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
⊢ (F.obj X).obj ≃ (F.obj X).obj

Tactic:
by
  let σ (t : F.obj X) : F.obj X := F.map (selfProdProj u t) b
  apply Equiv.ofBijective σ
  apply Finite.injective_iff_bijective.mp
  intro t s (hs : F.map (selfProdProj u t) b = F.map (selfProdProj u s) b)
  change id t = id s
  have h' : selfProdProj u t = selfProdProj u s := evaluation_injective_of_isConnected F A X b hs
  rw [← selfProdProj_fiber h s, ← selfProdProj_fiber h t, h']

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
⊢ ∀
    (xi :
      (fun X ↦ X)
        ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
          (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })))
    (xj :
      (fun X ↦ X)
        ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
          (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ }))),
    (ConcreteCategory.hom
            ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
              (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })))
          xi =
        (ConcreteCategory.hom
            ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
              (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })))
          xj →
      ∃ k f g,
        (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) xi =
          (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) xj

Tactic:
(u : (A : C) ⟶ X)

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
u : A ⟶ X
⊢ ∀
    (xj :
      (fun X ↦ X)
        ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
          (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ }))),
    (ConcreteCategory.hom
            ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
              (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })))
          u =
        (ConcreteCategory.hom
            ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
              (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })))
          xj →
      ∃ k f g,
        (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) u =
          (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) xj
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x : (F.obj X).obj
⊢ (fun f ↦ (ConcreteCategory.hom (F.map f)) a) (u ≫ Pi.π (fun x ↦ X) x) = x

Tactic:
exact (selfProdProj_fiber h1) x

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

Goal state before:
pp: 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)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
⊢ σ.hom.app X = 𝟙 (F.obj X)

Tactic:
have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _

Goal state after:
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)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
this : Fintype (fι ⟨X, XinI⟩)
⊢ σ.hom.app X = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
H : Set (Aut F)
h1 : 1 ∈ H
h : IsOpen H
⊢ ∃ I x, (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ H

Tactic:
obtain ⟨U, hUopen, rfl⟩ := isOpen_induced_iff.mp h
  obtain ⟨I, u, ho, ha⟩ := isOpen_pi_iff.mp hUopen 1 h1
  choose fι ff fc h4 h5 h6 using (fun X : I => has_decomp_connected_components X.val)
  refine ⟨⋃ X, Set.range (ff X), Fintype.ofFinite _, ?_, ?_⟩
  · rintro X ⟨A, ⟨Y, rfl⟩, hA2⟩
    obtain ⟨i, rfl⟩ := hA2
    exact h5 Y i
  · refine fun σ h ↦ ha (fun X XinI ↦ ?_)
    suffices h : autEmbedding F σ X = 1 by
      rw [h]
      exact (ho X XinI).right
    have h : σ.hom.app X = 𝟙 (F.obj X) := by
      have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _
      ext x
      obtain ⟨⟨j⟩, a, ha : F.map _ a = x⟩ := Limits.FintypeCat.jointly_surjective
        (Discrete.functor (ff ⟨X, XinI⟩) ⋙ F) _ (Limits.isColimitOfPreserves F (h4 ⟨X, XinI⟩)) x
      rw [FintypeCat.id_apply, ← ha, NatTrans.naturality_apply]
      simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]
    exact Iso.ext h

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 X
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : Y ⟶ Z
⊢ whiskerLeft X f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ whiskerRight f X

Tactic:
dsimp [braiding]

Goal state after:
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 X
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : Y ⟶ Z
⊢ (whiskerLeft X f ≫ fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) =
    (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) ≫ whiskerRight f X
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✝³ : Y.HasTensor Z
inst✝² : Z.HasTensor Y
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : X ⟶ Y
⊢ whiskerRight f Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ whiskerLeft Z f

Tactic:
dsimp [braiding]

Goal state after:
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✝³ : Y.HasTensor Z
inst✝² : Z.HasTensor Y
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : X ⟶ Y
⊢ (whiskerRight f Z ≫ fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i k ⋯) =
    (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) ≫ whiskerLeft Z f
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 X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      ((associator X Y Z).hom ≫ (braiding X (tensorObj Y Z)).hom ≫ (associator Y Z X).hom) k =
    ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      (whiskerRight (braiding X Y).hom Z ≫ (associator Y X Z).hom ≫ whiskerLeft Y (braiding X Z).hom) k

Tactic:
dsimp [braiding]

Goal state after:
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 X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      (associator X Y Z).hom k ≫
        (tensorObjDesc fun i j hij ↦ (β_ (X i) (tensorObj Y Z j)).hom ≫ ιTensorObj (tensorObj Y Z) X j i k ⋯) ≫
          (associator Y Z X).hom k =
    ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) Z k ≫
        (associator Y X Z).hom k ≫
          whiskerLeft Y (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
V : Type u_1
inst✝¹ : Quiver V
inst✝ : Nonempty V
⊢ Nonempty (Quiver.FreeGroupoid V)

Tactic:
inhabit V

Goal state after:
V✝ : Type u
inst✝² : Quiver V✝
V : Type u_1
inst✝¹ : Quiver V
inst✝ : Nonempty V
inhabited_h : Inhabited V
⊢ Nonempty (Quiver.FreeGroupoid V)
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
⊢ ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      ((associator X Y Z).inv ≫ (braiding (tensorObj X Y) Z).hom ≫ (associator Z X Y).inv) k =
    ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      (whiskerLeft X (braiding Y Z).hom ≫ (associator X Z Y).inv ≫ whiskerRight (braiding X Z).hom Y) k

Tactic:
dsimp [braiding]

Goal state after:
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
⊢ ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      (associator X Y Z).inv k ≫
        (tensorObjDesc fun i j hij ↦ (β_ (tensorObj X Y i) (Z j)).hom ≫ ιTensorObj Z (tensorObj X Y) j i k ⋯) ≫
          (associator Z X Y).inv k =
    ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      whiskerLeft X (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i k ⋯) k ≫
        (associator X Z Y).inv k ≫
          whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) Y k
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ (comap φ S).arrows c✝ c✝
⊢ Groupoid.inv f ≫ γ ≫ f ∈ (comap φ S).arrows d✝ d✝

Tactic:
simp_rw [inv_eq_inv f, comap, mem_ofPred, Functor.map_comp, Functor.map_inv, ← inv_eq_inv]
    exact Sn.conj _ hγ

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:
rw [mem_map_iff] at hδ

Goal state after:
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δ : ∃ a b g, ∃ (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), δ = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
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:
dsimp [braiding]

Goal state after:
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
⊢ ((fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) ≫ fun k ↦
      tensorObjDesc fun i j hij ↦ (β_ (Y i) (X j)).hom ≫ ιTensorObj X Y j i k ⋯) =
    𝟙 (tensorObj X Y)