mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.rightDerivedToHomotopyCategory.map f ≫ (J.isoRightDerivedToHomotopyCategoryObj F).hom =
    (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ

Tactic:
by
  dsimp [Functor.rightDerivedToHomotopyCategory, isoRightDerivedToHomotopyCategoryObj]
  rw [← Functor.map_comp_assoc, iso_hom_naturality f I J φ comm, Functor.map_comp,
    assoc, assoc]
  erw [(F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.naturality]
  rfl

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ Y' s, ∃ (_ : P.monoModSerre s), f ≫ s = 0) → P (Abelian.image f)

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), f ≫ s = 0

Tactic:
· rintro ⟨Y', s, hs, eq⟩
    apply P.prop_of_iso (Abelian.coimageIsoImage f)
    have := P.monoModSerre.comp_mem (Abelian.factorThruCoimage f) s
      (monoModSerre_of_mono _ _) hs
    rwa [show Abelian.factorThruCoimage f ≫ s = 0 by cat_disch,
      monoModSerre_zero_iff] at this

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), f ≫ s = 0
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ IsColimit
    ((Cocone.precompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).hom).obj (Cofork.ofπ (cokernel.π f.hom) ⋯))

Tactic:
exact (IsColimit.precomposeHomEquiv _ _).symm (cokernelIsCokernel f.hom)

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ L.map φ.s ≫ φ.map L ⋯ = 0

Tactic:
MorphismProperty.RightFraction.map_s_comp_map

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ L.map φ.f = 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.s ≫ φ.map L ⋯
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w

Tactic:
MorphismProperty.RightFraction.map_s_comp_map

Goal state after:
case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.f
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ w = φ.map L ⋯
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w

Tactic:
rw [← cancel_epi (L.map φ.s),
      MorphismProperty.RightFraction.map_s_comp_map] at hφ

Goal state after:
case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.f
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w
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) ≫ adj₁.counit.app (F.obj (U.obj X)) ≫ s.π = adj₁.counit.app (h X).W ≫ (h X).right ≫ s.π

Tactic:
rw [← dsimp% s.condition, ← F.map_comp_assoc, ← U.map_comp, RegularEpi.w, U.map_comp,
        F.map_comp_assoc, s.condition, ← adj₁.counit_naturality_assoc (h X).right]

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

Goal state before:
pp: 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
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
⊢ (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint

Tactic:
refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint

Goal state after:
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
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
⊢ R ⋙ U ≅ R' ⋙ (monadicAdjunction U).toMonad.forget
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X : PartialFun
o : { X := Option X, point := none }.X
a : X
⊢ (Part.some a).toOption = some a

Tactic:
convert! Part.some_toOption a

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1 ∈ f a, ⟨some b, hb⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨some b, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩

Tactic:
simp only [ne_eq, Part.mem_some_iff]

Goal state after:
case some
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1 ∈ f a, ⟨some b, hb⟩ = ⟨some a_1, ⋯⟩) ↔ some b = (partialFunToPointed.map f).toFun (some a)
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X✝ Y✝ : Type ?u.12
f : X✝ ⟶ Y✝
a✝ : ((typeToPartialFun ⋙ partialFunToPointed).obj X✝).X
a : typeToPartialFun.obj X✝
⊢ (typeToPartialFun.map f a).Dom

Tactic:
trivial

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := (Subobject.pullback (prod.map π₂ π₂ :
        (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le g)
      rw [← Subobject.pullback_comp, ← Subobject.pullback_comp] at this
      convert! this using 3 <;> simp

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₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ (adj.homEquiv A₁.a A₂.a) (A₁.str ≫ f.f) = (adj.homEquiv A₁.a A₂.a) (F.map f.f ≫ A₂.str)

Tactic:
f.h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ (adj.homEquiv A₁.a A₂.a) (A₁.str ≫ f.f) = (adj.homEquiv A₁.a A₂.a) (A₁.str ≫ f.f)
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ (adj.homEquiv V₁.V V₂.V).symm (f.f ≫ V₂.str) = (adj.homEquiv V₁.V V₂.V).symm (V₁.str ≫ G.map f.f)

Tactic:
f.h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ (adj.homEquiv V₁.V V₂.V).symm (f.f ≫ V₂.str) = (adj.homEquiv V₁.V V₂.V).symm (f.f ≫ V₂.str)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
    eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ≫
      (λ_ (F₁.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₃.obj j)

Tactic:
tensorHom_def'_assoc

Goal state after:
V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    (end_.π (diagram V F₁ F₂) j ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
      eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ≫
        (λ_ (F₁.obj j ⟶[V] F₃.obj j)).inv ≫
          ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₃.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

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

Tactic:
φ'

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
c : 𝒳
g : p.obj c ⟶ R
φ' : c ⟶ b
⊢ ∀ [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ ((ρ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂) ≫
      end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j

Tactic:
rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def', assoc,
    ← MonoidalCategory.whiskerLeft_comp_assoc, enrichedId_π,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id, assoc, assoc,
    Iso.inv_hom_id_assoc]

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j ≫
      (ρ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv ≫
        ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁ eId V (F₂.obj j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j
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 Y : C
f g : X ⟶ Y
x : (F.obj X).obj
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
⊢ (ConcreteCategory.hom (F.map (equalizer.ι f g))) ((fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x

Tactic:
by
  simp only [fiberEqualizerEquiv, Functor.comp_map]
  change ((Types.equalizerIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map (equalizer.ι f g)) _ = _
  erw [PreservesEqualizer.iso_inv_ι, Types.equalizerIso_inv_comp_ι]
  rfl

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

Goal state before:
pp: G : Type v
inst✝¹ : Group G
inst✝ : Finite G
⊢ PreservesColimitsOfShape (SingleObj G) FintypeCat.incl

Tactic:
choose G' hg hf e using Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.preservesColimitsOfShape_of_equiv (Classical.choice e).toSingleObjEquiv.symm _

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

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

Tactic:
cases i
      · exact Cofan.IsColimit.desc h₁ (fun a ↦ s.inj (.inl a))
      · exact Cofan.IsColimit.desc h₂ (fun a ↦ s.inj (.inr a))

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

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

Tactic:
(v : (B : C) ⟶ X)

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
u : A ⟶ X
v : B ⟶ X
⊢ (ConcreteCategory.hom
          ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
            (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })))
        u =
      (ConcreteCategory.hom
          ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
            (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })))
        v →
    ∃ k f g,
      (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) u =
        (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) v
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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
X : C
x✝ : IsGalois X
x : (F.obj X).obj
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ } • s ∈ c
⊢ (gi { obj := X, pt := x, isGalois := ⋯ } • s) • x = (ConcreteCategory.hom (t.hom.app X)) x

Tactic:
rw [smul_eq_mul, mul_smul, hsmem]

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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
X : C
x✝ : IsGalois X
x : (F.obj X).obj
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ } • s ∈ c
⊢ gi { obj := X, pt := x, isGalois := ⋯ } • x = (ConcreteCategory.hom (t.hom.app X)) x
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
a✝ : p✝ ∈ univ
⊢ Groupoid.inv p✝ ∈ univ

Tactic:
trivial

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✝
a✝¹ : p✝ ∈ univ
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ univ
⊢ p✝ ≫ q✝ ∈ univ

Tactic:
trivial

Goal state after:
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:
· rintro h
    ext x; constructor <;> simp only [mem_univ, imp_true_iff, forall_true_left]
    apply mem_objs_of_src S (h.wide x)

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: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ g ∈ ⊤.arrows (φ.obj c) (φ.obj c')

Tactic:
trivial

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
a b c d : C ⋆ D
f : a.Hom b
g : b.Hom c
h : c.Hom d
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases a <;>
    cases b <;>
    cases c <;>
    cases d <;>
    simp only [Hom, comp, Category.assoc] <;>
    tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₁ = g₁

Tactic:
rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]

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

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
x : (F.obj (op j')).obj j
⊢ ∃ f_1 y,
    (hom ((F.map f_1.op).app j)) y = (Hom.hom ((F.map f.op).app j)) x ∧
      (hom ((F.obj (op j')).map f_1)) y = (Hom.hom ((F.obj (op j')).map f)) x

Tactic:
exact ⟨f, x, by simp⟩

Goal state after: