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

Goal state before:
pp: 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 :=
  TwoSquare.StructuredArrowRightwards.mk (TwoSquare.overPost F X) g (Over.mk prod.fst)
    (Over.homMk
      (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z))
      ⋯)
    prod.snd ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ StructuredArrow.hom Q ≫
      ((TwoSquare.overPost F X).costructuredArrowRightwards Z).map
        (CostructuredArrow.homMk
          (Over.homMk (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom) ⋯) ⋯) =
    StructuredArrow.hom P

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: 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
⊢ IsConnected ((TwoSquare.overPost F X).StructuredArrowRightwards g)

Tactic:
by

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

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

Tactic:
by

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

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

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
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows 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
c d : C
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d

Tactic:
by
  constructor
  · intro h
    simpa only [inv_eq_inv, IsIso.inv_inv] using S.inv h
  · apply S.inv

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
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
this : Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e
⊢ g ∈ S.arrows d e

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 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
⊢ (associator X Y Z).hom ≫ (braiding X (tensorObj Y Z)).hom ≫ (associator Y Z X).hom =
    whiskerRight (braiding X Y).hom Z ≫ (associator Y X Z).hom ≫ whiskerLeft Y (braiding X Z).hom

Tactic:
by

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

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

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
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
this : (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d
⊢ f ∈ S.arrows c d

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
⊢ ∃ X, Nonempty ((functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑V)))

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
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e ↔ f ∈ S.arrows 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
c : C
⊢ c ∈ S.objs → 𝟙 c ∈ S.arrows c c

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul (Aut F) X.V.obj
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ 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 : ↑S.objs
p : c ⟶ d
⊢ ↑(inv p) = inv ↑p

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ Function.Injective S.hom.obj

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 : ↑S.objs), Function.Injective fun f ↦ S.hom.map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S✝ x✝¹ x✝ : Subgroupoid C
S : (c d : C) → Set (c ⟶ d)
inv✝¹ : ∀ {c d : C} {p : c ⟶ d}, p ∈ S c d → Groupoid.inv p ∈ S d c
mul✝¹ : ∀ {c d e : C} {p : c ⟶ d}, p ∈ S c d → ∀ {q : d ⟶ e}, q ∈ S d e → p ≫ q ∈ S c e
T : (c d : C) → Set (c ⟶ d)
inv✝ : ∀ {c d : C} {p : c ⟶ d}, p ∈ T c d → Groupoid.inv p ∈ T d c
mul✝ : ∀ {c d e : C} {p : c ⟶ d}, p ∈ T c d → ∀ {q : d ⟶ e}, q ∈ T d e → p ≫ q ∈ T c e
h : ↑{ arrows := S, inv := inv✝¹, mul := mul✝¹ } = ↑{ arrows := T, inv := inv✝, mul := mul✝ }
⊢ { arrows := S, inv := inv✝¹, mul := mul✝¹ } = { arrows := T, inv := inv✝, mul := mul✝ }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
⊢ S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows 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
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ univ → Groupoid.inv p ∈ univ

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 ∈ univ → ∀ {q : d ⟶ e}, q ∈ univ → p ≫ q ∈ univ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c : C
⊢ c ∈ ⊤.objs

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ ⋂ S ∈ s, S.arrows c✝ d✝
⊢ Groupoid.inv p✝ ∈ ⋂ S ∈ s, 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
s : Set (Subgroupoid C)
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ ⋂ S ∈ s, S.arrows c✝ d✝
x✝ : d✝ ⟶ e✝
hq : x✝ ∈ ⋂ S ∈ s, S.arrows d✝ e✝
⊢ p✝ ≫ x✝ ∈ ⋂ S ∈ s, 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 : Set (Subgroupoid C)), IsGLB s (sInf s)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
x✝¹ x✝ : ↑S.objs
s : C
hs : s ∈ S.objs
t : C
ht : t ∈ S.objs
⊢ (inclusion h).obj ⟨s, hs⟩ = (inclusion h).obj ⟨t, ht⟩ → ⟨s, hs⟩ = ⟨t, ht⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ (fun f ↦ (inclusion h).map f) ⟨f, hf⟩ = (fun f ↦ (inclusion h).map f) ⟨g, hg⟩ → ⟨f, hf⟩ = ⟨g, hg⟩

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 ∈ {p | Discrete.Arrows c d p} → Groupoid.inv p ∈ {p | Discrete.Arrows d c p}

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 ∈ {p | Discrete.Arrows c d p} →
      ∀ {q : d ⟶ e}, q ∈ {p | Discrete.Arrows d e p} → p ≫ q ∈ {p | Discrete.Arrows c e p}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
⊢ f ∈ discrete.arrows c d → ∃ (h : c = d), f = eqToHom h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
⊢ (∃ (h : c = d), f = eqToHom h) → f ∈ discrete.arrows 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
⊢ S.IsWide ↔ S.objs = univ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c d : C
h : c = d
⊢ eqToHom h ∈ S.arrows 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
Sn : S.IsNormal
c✝ d✝ : C
p : d✝ ⟶ c✝
γ : c✝ ⟶ c✝
hs : γ ∈ S.arrows c✝ c✝
⊢ p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d✝ d✝

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
Sn : S.IsNormal
c d : C
p : c ⟶ d
⊢ BijOn (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (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 : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), 𝟙 c ∈ (sInf s).arrows c c

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, γ ∈ (sInf s).arrows c c → Groupoid.inv p ≫ γ ≫ p ∈ (sInf s).arrows d d

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c : C
⊢ 𝟙 c ∈ discrete.arrows c c

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ discrete.arrows c✝ c✝
⊢ Groupoid.inv f ≫ γ ≫ f ∈ discrete.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
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
⊢ y * x * y⁻¹ ∈ S.vertexSubgroup cS

Tactic:
by

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
⊢ X c d ⊆ (generated X).arrows c d

Tactic:
by

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)
⊢ generated X ≤ generatedNormal 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
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
⊢ ((biproduct.map fun j ↦ (F j).p) ≫ biproduct.map fun j ↦ (F j).p) = biproduct.map fun j ↦ (F j).p

Tactic:
by

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)
S : Subgroupoid C
Sn : S.IsNormal
⊢ generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d

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
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ { X := ⨁ fun j ↦ (F j).X, p := biproduct.map fun j ↦ (F j).p, idem := ⋯ }.p ≫
      ((biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j) ≫ (F j).p =
    (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j

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
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ (F j).p ≫
      (biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p) ≫
        { X := ⨁ fun j ↦ (F j).X, p := biproduct.map fun j ↦ (F j).p, idem := ⋯ }.p =
    biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p

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

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
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j 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 := ⋯ } =
    if h : j = j' then eqToHom ⋯ else 0

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
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ 𝟙 c ∈ (comap φ S).arrows c c

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
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ HasBiproduct F

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
⊢ P.decompId_i ≫ P.complement.decompId_p = 0

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
f : IsoCat D E
⊢ 𝟭 C = (e.functor ⋙ f.functor) ⋙ f.inverse ⋙ e.inverse

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
⊢ P.complement.decompId_i ≫ P.decompId_p = 0

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
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:
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
f : IsoCat D E
⊢ (f.inverse ⋙ e.inverse) ⋙ e.functor ⋙ f.functor = 𝟭 E

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
Y : D
⊢ F.obj (F.objEquiv.symm Y) = Y

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✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ F.obj (F.objEquiv.symm X✝) = 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
⊢ { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p, inl := P.decompId_i,
            inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.fst ≫
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inl +
      { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.snd ≫
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inr =
    𝟙
      { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
          inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
          inr_snd := ⋯ }.pt

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✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ Y✝ = F.obj (F.objEquiv.symm Y✝)

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✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ F.preimage (eqToHom ⋯ ≫ (x✝¹ ≫ x✝) ≫ eqToHom ⋯) =
    F.preimage (eqToHom ⋯ ≫ x✝¹ ≫ eqToHom ⋯) ≫ F.preimage (eqToHom ⋯ ≫ x✝ ≫ eqToHom ⋯)

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
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

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 : C
⊢ (𝟭 C).obj x = (F ⋙ F.strictInv).obj x

Tactic:
by

Goal state after: