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

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.snd =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.snd

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.snd =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.snd
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c → f ∈ S.arrows c d

pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c → f ∈ S.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e

pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d

pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsWide → S.objs = univ

pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.objs = univ → S.IsWide

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsWide → S.objs = univ
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.objs = univ → S.IsWide

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.objs = univ → S.IsWide
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
γ₁ : c ⟶ c
x✝¹ : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
x✝ : γ₂ ∈ S.arrows c c
h : (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₂
⊢ γ₁ = γ₂

pp: case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
δ : d ⟶ d
δS : δ ∈ S.arrows d d
⊢ (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
γ₁ : c ⟶ c
x✝¹ : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
x✝ : γ₂ ∈ S.arrows c c
h : (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₂
⊢ γ₁ = γ₂
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
δ : d ⟶ d
δS : δ ∈ S.arrows d d
⊢ (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
δ : d ⟶ d
δS : δ ∈ S.arrows d d
⊢ (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
⊢ generated X ≤ generatedNormal X

Tactic:
apply @sInf_le_sInf (Subgroupoid C) _
  exact fun S ⟨h, _⟩ => h

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ generatedNormal X ≤ S → ∀ (c d : C), X c d ⊆ S.arrows c d

pp: case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ generatedNormal X ≤ S → ∀ (c d : C), X c d ⊆ S.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : j = j'
⊢ { f := biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p, comm := ⋯ } ≫
      { f := (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j', comm := ⋯ } =
    eqToHom ⋯

pp: case neg
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : ¬j = j'
⊢ { f := biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p, comm := ⋯ } ≫
      { f := (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j', comm := ⋯ } =
    0

Tactic:
·

Goal state after:
case pos
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : j = j'
⊢ { f := biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p, comm := ⋯ } ≫
      { f := (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j', comm := ⋯ } =
    eqToHom ⋯
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : ¬j = j'
⊢ { f := biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p, comm := ⋯ } ≫
      { f := (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j', comm := ⋯ } =
    0

Tactic:
·

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : ¬j = j'
⊢ { f := biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p, comm := ⋯ } ≫
      { f := (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j', comm := ⋯ } =
    0
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ (∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb) →
    Arrows φ hφ S c d f
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

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

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

Tactic:
·

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inl ≫ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    biprod.inl ≫ 𝟙 (P ⊞ P.complement)
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

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

Tactic:
·

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inr ≫ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    biprod.inr ≫ 𝟙 (P ⊞ P.complement)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

pp: case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty → ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

pp: case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ (∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d) → {x | Map.Arrows φ hφ S d d x}.Nonempty

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty → ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ (∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d) → {x | Map.Arrows φ hφ S d d x}.Nonempty

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ (∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d) → {x | Map.Arrows φ hφ S d d x}.Nonempty
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ (∀ (c d : C), (S.arrows c d).Nonempty → c = d) → S.IsTotallyDisconnected

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected → ∀ (c d : C), (S.arrows c d).Nonempty → c = d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ (∀ (c d : C), (S.arrows c d).Nonempty → c = d) → S.IsTotallyDisconnected
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
  ext k i₁ i₂ i₃ h
  dsimp [braiding]
  conv_lhs => rw [ιTensorObj₃_associator_inv_assoc, ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc,
    ι_tensorObjDesc_assoc, assoc, ← MonoidalCategory.tensorHom_id,
    BraidedCategory.braiding_naturality_assoc,
    BraidedCategory.braiding_tensor_left_hom, assoc, assoc, assoc, assoc, Iso.inv_hom_id_assoc,
    MonoidalCategory.id_tensorHom,
    ← ιTensorObj₃_eq_assoc Z X Y i₃ i₁ i₂ k (by rw [add_assoc, add_comm i₃, h]) _ rfl,
    ιTensorObj₃_associator_inv, Iso.hom_inv_id_assoc]
  conv_rhs => rw [ιTensorObj₃_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc, ι_tensorHom_assoc,
    ← MonoidalCategory.id_tensorHom,
    MonoidalCategory.tensorHom_comp_tensorHom_assoc, id_comp, ι_tensorObjDesc,
    categoryOfGradedObjects_id, MonoidalCategory.id_tensor_comp, assoc,
    MonoidalCategory.id_tensorHom, MonoidalCategory.id_tensorHom,
    ← ιTensorObj₃_eq_assoc X Z Y i₁ i₃ i₂ k
      (by rw [add_assoc, add_comm i₃, ← add_assoc, h]) (i₂ + i₃) (add_comm _ _),
    ιTensorObj₃_associator_inv_assoc,
    ιTensorObj₃'_eq X Z Y i₁ i₃ i₂ k (by rw [add_assoc, add_comm i₃, ← add_assoc, h]) _ rfl,
    assoc, ι_tensorHom, categoryOfGradedObjects_id, ← MonoidalCategory.tensorHom_id,
    ← MonoidalCategory.comp_tensor_id_assoc,
    ι_tensorObjDesc, MonoidalCategory.comp_tensor_id, assoc,
    MonoidalCategory.tensorHom_id, MonoidalCategory.tensorHom_id,
    ← ιTensorObj₃'_eq Z X Y i₃ i₁ i₂ k (by rw [add_assoc, add_comm i₃, h])
      (i₁ + i₃) (add_comm _ _)]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: case left
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 g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).L
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ g

pp: case right
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 g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).R
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ g

Tactic:
·

Goal state after:
case left
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 g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).L
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ g
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: case right
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 g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).R
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ g

Tactic:
·

Goal state after:
case right
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 g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend J).R
⊢ (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ f =
    (ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ g
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj zero ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := zero, right := { as := as✝ }, hom := φ } (mk ⋯.some)

pp: case one
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := one, right := { as := as✝ }, hom := φ } (mk ⋯.some)

Tactic:
·

Goal state after:
case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj zero ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := zero, right := { as := as✝ }, hom := φ } (mk ⋯.some)
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: case one
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := one, right := { as := as✝ }, hom := φ } (mk ⋯.some)

Tactic:
·

Goal state after:
case one
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := one, right := { as := as✝ }, hom := φ } (mk ⋯.some)
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    NatTrans.toCatHom₂ (mapWhiskerRight (η ▷ h).toNatTrans (𝟭 D)) =
      (Cat.Hom.isoMk (mapCompLeft D f.toFunctor h.toFunctor)).hom ≫
        NatTrans.toCatHom₂ (mapWhiskerRight η.toNatTrans (𝟭 D)) ▷ (mapPair h.toFunctor (𝟭 D)).toCatHom ≫
          (Cat.Hom.isoMk (mapCompLeft D g.toFunctor h.toFunctor)).inv

Tactic:
by intros; exact congr($(mapWhiskerRight_whiskerRight D _ _).toCatHom₂)

Goal state after: