mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsLeftDerivedFunctor α W ↔ LF.IsRightKanExtension α

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsLeftDerivedFunctor α W → LF.IsRightKanExtension α

case mpr
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsRightKanExtension α → LF.IsLeftDerivedFunctor α W
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (φ ≫ L.map f)) =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))

Tactic:
have eq := s.π.naturality
        (StructuredArrow.homMk f : StructuredArrow.mk φ ⟶ StructuredArrow.mk (φ ≫ L.map f))

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
eq :
  ((const (StructuredArrow (L.obj Y) L)).obj s.pt).map (StructuredArrow.homMk f ⋯) ≫
      s.π.app (StructuredArrow.mk (φ ≫ L.map f)) =
    s.π.app (StructuredArrow.mk φ) ≫ (StructuredArrow.proj (L.obj Y) L ⋙ F).map (StructuredArrow.homMk f ⋯)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (φ ≫ L.map f)) =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))
Module: Mathlib.CategoryTheory.Limits.FintypeCat

Goal state before:
pp: J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Type u_1
inst✝ : ∀ (j : J), Finite (K.obj j)
⊢ Fintype (limit K)

Tactic:
have : Fintype (sections K) := Fintype.ofFinite (sections K)
  exact Fintype.ofEquiv (sections K) (Types.limitEquivSections K).symm

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

Goal state before:
pp: case pos
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
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
let ⟨ι₁, f₁, g₁, hc₁, hf₁, he₁⟩ := hi (Nat.card (F.obj Y)) hn1 Y rfl

Goal state after:
case pos
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 ι₁
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
hf : Finite ι
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)

Tactic:
exact ⟨ι, hf, f, colimit.isoColimitCocone ⟨Cofan.mk X g, hl⟩, hc⟩

Goal state after:
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 B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b

Tactic:
have hn : IsInitial Y → False := not_initial_of_inhabited F y

Goal state after:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (a Y).hom = (a X).hom ≫ F.map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom
X Y : C
f : X ⟶ Y
x✝ : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map f ≫ (a Y).hom)) x✝ = (ConcreteCategory.hom ((a X).hom ≫ F.map f)) x✝
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
⊢ IsGalois A ∧ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
constructor

Goal state after:
case h.left
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
⊢ IsGalois A

case h.right
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
⊢ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
⊢ ContinuousSMul (Aut (F.obj X)) (F.obj X).obj

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
⊢ Continuous fun p ↦ p.1 • p.2
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X✝ Y✝ : PointedGaloisObject F
f : X✝ ⟶ Y✝
⊢ (autGaloisSystem F ⋙ forget GrpCat).map f ≫ (evaluationEquivOfIsGalois F Y✝.obj Y✝.pt).toIso.hom =
    (evaluationEquivOfIsGalois F X✝.obj X✝.pt).toIso.hom ≫ (incl F ⋙ F ⋙ FintypeCat.incl).map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X✝ Y✝ : PointedGaloisObject F
f : X✝ ⟶ Y✝
x✝ : (autGaloisSystem F ⋙ forget GrpCat).obj X✝
⊢ (ConcreteCategory.hom
          ((autGaloisSystem F ⋙ forget GrpCat).map f ≫ (evaluationEquivOfIsGalois F Y✝.obj Y✝.pt).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((evaluationEquivOfIsGalois F X✝.obj X✝.pt).toIso.hom ≫ (incl F ⋙ F ⋙ FintypeCat.incl).map f)).toFun
      x✝
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
g : G
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (isoOnObj F g Y).hom = (isoOnObj F g X).hom ≫ F.map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
g : G
X Y : C
f : X ⟶ Y
x✝ : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map f ≫ (isoOnObj F g Y).hom)) x✝ =
    (ConcreteCategory.hom ((isoOnObj F g X).hom ≫ F.map f)) x✝
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
⊢ NatIso.ofComponents (isoOnObj F 1) ⋯ = 1

Tactic:
ext

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
x✝¹ : C
x✝ : (F.obj x✝¹).obj
⊢ (ConcreteCategory.hom ((NatIso.ofComponents (isoOnObj F 1) ⋯).hom.app x✝¹)) x✝ =
    (ConcreteCategory.hom ((Iso.hom 1).app x✝¹)) x✝
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).obj
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
t : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
x : (F.obj X).obj
hg : g • x = (ConcreteCategory.hom (t.app X)) x
y : (F.obj X).obj
⊢ g • y = (ConcreteCategory.hom (t.app X)) y

Tactic:
by
  obtain ⟨φ, (rfl : F.map φ.hom y = x)⟩ := MulAction.exists_smul_eq (Aut X) y x
  have : Function.Injective (F.map φ.hom) :=
    ConcreteCategory.injective_of_mono_of_preservesPullback (F.map φ.hom)
  apply this
  rw [IsNaturalSMul.naturality, hg, FunctorToFintypeCat.naturality]

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
⊢ HomRel.CompClosure redStep (Path.reverse WY ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)

Tactic:
constructor

Goal state after:
V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
⊢ redStep (𝟙 ((Paths.of (Symmetrify V)).obj X✝)) (f.toPath ≫ (reverse f).toPath)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
⊢ redStep (𝟙 ((Paths.of (Symmetrify V)).obj X✝)) (f.toPath ≫ (reverse f).toPath)

Tactic:
constructor

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
⊢ g = 1

Tactic:
ext X x
    exact h X x

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
X✝ Y✝ : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
⊢ 𝟙 ((Symmetrify.lift φ).obj ((Paths.of (Symmetrify V)).obj X)) =
    (Paths.lift (Symmetrify.lift φ)).map (f.toPath.comp Path.nil) ≫ (Symmetrify.lift φ).map (reverse f)

Tactic:
Quiver.Path.comp_nil,

Goal state after:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
X✝ Y✝ : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
⊢ 𝟙 ((Symmetrify.lift φ).obj ((Paths.of (Symmetrify V)).obj X)) =
    (Paths.lift (Symmetrify.lift φ)).map f.toPath ≫ (Symmetrify.lift φ).map (reverse f)
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:
ext

Goal state after:
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 ≫
          ((TwoSquare.overPost F X).costructuredArrowRightwards Z).map
            (CostructuredArrow.homMk
              (Over.homMk (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom) ⋯) ⋯)).left =
    Over.Hom.left (StructuredArrow.hom P).left
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
⊢ (Over.Hom.left (StructuredArrow.hom Q).left ≫
        F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
      prodComparison F X Z =
    Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z

Tactic:
ext

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.fst =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.fst

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

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

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

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

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

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

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: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d : C
⊢ 𝟙 c✝ ∈ {p | Discrete.Arrows c✝ c✝ p}

Tactic:
constructor

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ d : C
⊢ 𝟙 c✝ ∈ {p | Discrete.Arrows c✝ c✝ p}

Tactic:
constructor

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

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

Tactic:
constructor

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

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

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 mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs ↔ x ∈ univ

Tactic:
constructor

Goal state after:
case mp.mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs → x ∈ univ

case mp.mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ univ → x ∈ S.objs
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

Tactic:
constructor

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

Goal state before:
pp: case id
C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
⊢ 𝟙 d✝ ∈ discrete.arrows d✝ d✝

Tactic:
constructor

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

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

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

Goal state after:
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
⊢ biproduct.ι (fun j ↦ (F j).X) j✝ ≫
      ((biproduct.map fun j ↦ (F j).p) ≫ biproduct.map fun j ↦ (F j).p) ≫ biproduct.π (fun j ↦ (F j).X) j✝¹ =
    biproduct.ι (fun j ↦ (F j).X) j✝ ≫ (biproduct.map fun j ↦ (F j).p) ≫ biproduct.π (fun j ↦ (F j).X) j✝¹