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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
⊢ (snd L R).Final

Tactic:
have : (fst R.op L.op).Initial := initial_fst_of_isCofiltered_costructuredArrow _ _

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this✝ : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
this : (fst R.op L.op).Initial
⊢ (snd L R).Final
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : L.Initial
⊢ (fst L R).Initial

Tactic:
by
  have := L.initial_iff_isCofiltered_costructuredArrow.mp inferInstance
  exact initial_fst_of_isCofiltered_costructuredArrow L R

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x✝¹ x✝ : K f g P₁ P₂
h : x✝¹ ⟶ x✝
this :
  (Prod.mkHom ((CostructuredArrow.map f).map (P₁.toCostructuredArrow.map h.left))
              ((CostructuredArrow.map g).map (P₁.toCostructuredArrow.map h.left)) ≫
            x✝.hom).1.left =
      (x✝¹.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).1.left ∧
    (Prod.mkHom ((CostructuredArrow.map f).map (P₁.toCostructuredArrow.map h.left))
              ((CostructuredArrow.map g).map (P₁.toCostructuredArrow.map h.left)) ≫
            x✝.hom).2.left =
      (x✝¹.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).2.left
⊢ (F₁ f g P₁ P₂).map h ≫ x✝.hom.2.left = x✝¹.hom.2.left ≫ (F₂ f g P₁ P₂).map h

Tactic:
exact this.2

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y' : (fun X ↦ X) (colimit (pointwiseProduct F))
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = y'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : (pointwiseProduct F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : (pointwiseProduct F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) y'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
⊢ y' = (hom (colimit.ι (pointwiseProduct F) k)) yk'

Tactic:
by
      simp only [k, yk', colimit.w_apply, hyk₀']

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

Goal state before:
pp: case left
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.monoModSerre f

pp: case right
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.epiModSerre f

Tactic:
· exact KernelFork.IsLimit.isZero_of_mono
      (KernelFork.mapIsLimit _ (kernelIsKernel f) G)

Goal state after:
case right
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.epiModSerre f
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ ((beckAlgebraCofork X).π ≫ { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }).f = s.π.f

Tactic:
simpa [← T.η.naturality_assoc, T.left_unit_assoc] using! T.η.app ((T : C ⥤ C).obj X.A) ≫= h₁

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: case refine_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ F.map (U.map (h X).left) ≫ F.map (U.map (adj₁.counit.app X)) ≫ s.π = adj₁.counit.app (h X).W ≫ (h X).right ≫ s.π

Tactic:
← F.map_comp_assoc,

Goal state after:
case refine_1
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ F.map (U.map (h X).left ≫ U.map (adj₁.counit.app X)) ≫ s.π = adj₁.counit.app (h X).W ≫ (h X).right ≫ s.π
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ (α.naturality g).hom = (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom

Tactic:
rw [naturality_naturality_hom α η]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv ▷ α.app b ≫ (α.naturality f).hom ≫ α.app a ◁ G.map₂ η.hom =
    (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ eqToHom ⋯ ≫ (𝟙 a ≫ f).fiber = f.fiber

Tactic:
simp [F.mapComp_id_left_hom_app, Strict.leftUnitor_eqToIso, ← Functor.map_comp_assoc,
        ← Cat.Hom₂.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
⊢ (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv = (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u

Tactic:
rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝ : Cat
⊢ ↾(𝟙 x✝).toFunctor.mapConnectedComponents = 𝟙 (ConnectedComponents ↑x✝)

Tactic:
ext x; simpa using (Quotient.exists_rep x).elim (fun _ h ↦ by subst h; rfl)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = t.unit ≫ f ◁ H.desc σs'

Tactic:
Hτ',

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = t.unit ≫ f ◁ H.desc σs'
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
x✝ : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ (fun f ↦ ⟨fun a ↦ (f a).Dom, f.asSubtype⟩) ((fun f x ↦ { Dom := f.fst x, get := fun h ↦ f.snd ⟨x, h⟩ }) ⟨p, f⟩) =
    ⟨p, f⟩

Tactic:
by dsimp; congr

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
f : (hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y
⊢ (hom (↾fun g ↦ eqToHom ⋯ ≫ (F.map (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯)).toFun f =
    (hom (𝟙 ((hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y))).toFun f

Tactic:
let : Category (objects.obj (F.obj X)) := (inferInstance : Category (F.obj X))

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
f : (hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y
this : Category.{v, v} (objects.obj (F.obj X)) := inferInstance
⊢ (hom (↾fun g ↦ eqToHom ⋯ ≫ (F.map (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯)).toFun f =
    (hom (𝟙 ((hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y))).toFun f
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₂.Q ⋙ (curry.obj (prodLift F hF)).flip = (prodLift₁ F hF).flip

Tactic:
simp only [prodLift, Functor.curry_obj_uncurry_obj, Functor.flip_flip]
  apply Construction.fac

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C ⊕ C'
f g : x ⟶ y
⊢ f = g

Tactic:
by
        cases f <;> cases g
        · case inl x y f g => rw [((by assumption : IsDiscrete C).subsingleton x y).allEq f g]
        · case inr x y f g => rw [((by assumption : IsDiscrete C').subsingleton x y).allEq f g]

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

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
C : Type u'
inst✝² : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasCoend F
X : C
f✝ : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f✝ i = (F.obj (op j)).map g ≫ f✝ j
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasCoend F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
⊢ (F.map φ.op).app j ≫ (f.app (op j)).app j ≫ ι F' j = (F.obj (op j')).map φ ≫ (f.app (op j')).app j' ≫ ι F' j'

Tactic:
by
    simp [coend.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ (Algebra.toCoalgebraOf adj).map ((AlgCoalgEquiv.unitIso adj).hom.app A) ≫
      (AlgCoalgEquiv.counitIso adj).hom.app ((Algebra.toCoalgebraOf adj).obj A) =
    𝟙 ((Algebra.toCoalgebraOf adj).obj A)

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∃! χ, p.IsHomLift h χ ∧ ψ ≫ χ = τ

Tactic:
use map p (f ≫ g) (φ ≫ ψ) (f' := f ≫ g ≫ h) (assoc f g h).symm (φ ≫ τ)

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ (fun χ ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)) ∧
    ∀ (y : c ⟶ c'), (fun χ ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
⊢ IsFiltered (Grothendieck F)

Tactic:
by
  have : Nonempty (Grothendieck F) := by
    obtain ⟨c⟩ : Nonempty C := IsFiltered.nonempty
    obtain ⟨f⟩ : Nonempty (F.obj c) := IsFiltered.nonempty
    exact ⟨⟨c, f⟩⟩
  apply IsFiltered.mk

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
this : F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom = 𝟙 F'
Y₂ : D₂
⊢ η.app (F'.obj Y₂) ≫ F'.map (ε.app Y₂) = 𝟙 (F'.obj Y₂)

Tactic:
simpa using congr_app this Y₂

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : ∀ (a : IsInitial X), False
he : IsEmpty (F.obj X).obj
⊢ False

Tactic:
exact Nonempty.elim ((initial_iff_fiber_empty F X).mpr he) h

Goal state after:
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✝³ x✝² : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝¹ x✝ : { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ { obj := B, pt := b, isGalois := isGalois✝ }
f : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hf :
  (ConcreteCategory.hom (F.map f)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
g : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hg :
  (ConcreteCategory.hom (F.map g)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
⊢ ∃ W h, h ≫ { val := f, comp := hf } = h ≫ { val := g, comp := hg }

Tactic:
obtain ⟨Z, h, z, hgal, hhz⟩ := exists_hom_from_galois_of_fiber F A a
    refine ⟨⟨Z, z, hgal⟩, ⟨h, hhz⟩, hom_ext ?_⟩
    apply evaluation_injective_of_isConnected F Z B z
    simp [hhz, hf, hg]

Goal state after:
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
y : (F.obj X).obj
φ : Aut X
hg :
  g • (ConcreteCategory.hom (F.map φ.hom)) y = (ConcreteCategory.hom (t.app X)) ((ConcreteCategory.hom (F.map φ.hom)) y)
this : Function.Injective ⇑(ConcreteCategory.hom (F.map φ.hom))
⊢ (ConcreteCategory.hom (F.map φ.hom)) (g • y) =
    (ConcreteCategory.hom (F.map φ.hom)) ((ConcreteCategory.hom (t.app X)) y)

Tactic:
rw [IsNaturalSMul.naturality, hg, FunctorToFintypeCat.naturality]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
e : C ≌ C'
e' : D ≌ D'
x : C ⋆ D
⊢ (mapPair e.functor e'.functor).map
        ((mapPairId.symm ≪≫
                mapIsoWhiskerRight e.unitIso (𝟭 D) ≪≫
                  mapIsoWhiskerLeft (e.functor ⋙ e.inverse) e'.unitIso ≪≫
                    mapPairComp e.functor e'.functor e.inverse e'.inverse).hom.app
          x) ≫
      ((mapPairComp e.inverse e'.inverse e.functor e'.functor).symm ≪≫
              mapIsoWhiskerRight e.counitIso (e'.inverse ⋙ e'.functor) ≪≫
                mapIsoWhiskerLeft (𝟭 C') e'.counitIso ≪≫ mapPairId).hom.app
        ((mapPair e.functor e'.functor).obj x) =
    𝟙 ((mapPair e.functor e'.functor).obj x)

Tactic:
cases x <;>
    simp [← (inclLeft C' D').map_comp, ← (inclRight C' D').map_comp]

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

Goal state before:
pp: case inst
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun i ↦
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)

pp: case inst
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun i ↦
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
· apply +allowSynthFailures Pi.map_epi
    intro ⟨_, _⟩
    split
    all_goals infer_instance

Goal state after:
case inst
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (Pi.map fun i ↦
      if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
⊢ Function.Bijective (⇑(coconeCompShrinkYonedaHomEquiv hc').symm ∘ Types.sectionOfCone (P.mapCone c)) ↔
    Function.Bijective fun g ↦ coconePtToShrinkYoneda c hc' ≫ g

Tactic:
← Function.Bijective.of_comp_iff _ shrinkYonedaEquiv.bijective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
⊢ Function.Bijective
      ((⇑(coconeCompShrinkYonedaHomEquiv hc').symm ∘ Types.sectionOfCone (P.mapCone c)) ∘ ⇑shrinkYonedaEquiv) ↔
    Function.Bijective fun g ↦ coconePtToShrinkYoneda c hc' ≫ g
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ (L'.obj X) (L'.obj Y) (L'.obj Z)).hom ≫
      (((braidingNatIso L W ε).app (L'.obj X)).app (L'.obj Y ⊗ L'.obj Z)).hom ≫
        (α_ (L'.obj Y) (L'.obj Z) (L'.obj X)).hom =
    (((braidingNatIso L W ε).app (L'.obj X)).app (L'.obj Y)).hom ▷ L'.obj Z ≫
      (α_ (L'.obj Y) (L'.obj X) (L'.obj Z)).hom ≫
        L'.obj Y ◁ (((braidingNatIso L W ε).app (L'.obj X)).app (L'.obj Z)).hom

Tactic:
simp only [associator_hom, Iso.app_hom, braidingNatIso_hom_app]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫
        LaxMonoidal.μ L' (X ⊗ Y) Z ≫
          L'.map (α_ X Y Z).hom ≫ OplaxMonoidal.δ L' X (Y ⊗ Z) ≫ L'.obj X ◁ OplaxMonoidal.δ L' Y Z) ≫
      ((braidingNatIso L W ε).hom.app (L'.obj X)).app (L'.obj Y ⊗ L'.obj Z) ≫
        LaxMonoidal.μ L' Y Z ▷ L'.obj X ≫
          LaxMonoidal.μ L' (Y ⊗ Z) X ≫
            L'.map (α_ Y Z X).hom ≫ OplaxMonoidal.δ L' Y (Z ⊗ X) ≫ L'.obj Y ◁ OplaxMonoidal.δ L' Z X =
    (LaxMonoidal.μ L' X Y ≫ L'.map (β_ X Y).hom ≫ OplaxMonoidal.δ L' Y X) ▷ L'.obj Z ≫
      (LaxMonoidal.μ L' Y X ▷ L'.obj Z ≫
          LaxMonoidal.μ L' (Y ⊗ X) Z ≫
            L'.map (α_ Y X Z).hom ≫ OplaxMonoidal.δ L' Y (X ⊗ Z) ≫ L'.obj Y ◁ OplaxMonoidal.δ L' X Z) ≫
        L'.obj Y ◁ (LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom ≫ OplaxMonoidal.δ L' Z X)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case mk.mk.mk.mk
C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₁✝ : X₁ ⟶ Y₁
f₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₂✝ : X₂ ⟶ Y₂
f₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g₁✝ : Y₁ ⟶ Z₁
g₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g₂✝ : Y₂ ⟶ Z₂
g₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(X₁.setoidHom Y₁)) f₁) (Quot.mk (⇑(X₂.setoidHom Y₂)) f₂) ≫
      Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(Y₁.setoidHom Z₁)) g₁) (Quot.mk (⇑(Y₂.setoidHom Z₂)) g₂) =
    Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(X₁.setoidHom Y₁)) f₁ ≫ Quot.mk (⇑(Y₁.setoidHom Z₁)) g₁)
      (Quot.mk (⇑(X₂.setoidHom Y₂)) f₂ ≫ Quot.mk (⇑(Y₂.setoidHom Z₂)) g₂)

Tactic:
exact Quotient.sound (tensorHom_comp_tensorHom _ _ _ _)

Goal state after: