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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
G : ShrinkHoms.{u} C
hG : IsCoseparator G
⊢ HasCoseparator (ShrinkHoms.{u} C)

Tactic:
exact ⟨G, hG⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
⊢ ∑ x ∈ F.attach, r x • (↑x).as = 0

Tactic:
simp only [← g.hom.map_eq_zero_iff ((ModuleCat.mono_iff_injective _).1 hg), map_sum, map_smul]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
r : ↥F → (End G)ᵐᵒᵖ :=
  fun x ↦
    MulOpposite.op
      (h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun x ↦ G) x)
⊢ ∑ x ∈ F.attach, r x • (ModuleCat.Hom.hom g) (↑x).as = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x)).hom =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯

Tactic:
change SmallShiftedHom.equiv _ _ (.comp _ (CohomologyClass.mk x).toSmallShiftedHom _) = _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ (SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q)
      ((SmallShiftedHom.mk₀Inv 0 ⋯ R.π' ⋯).comp (CohomologyClass.mk x).toSmallShiftedHom ⋯) =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: case e_g
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ inv (DerivedCategory.Q.map R.ι') ≫
      (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y ≫ (DerivedCategory.singleFunctor C 0).map g =
    DerivedCategory.Q.map φ.hom' ≫
      inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'

Tactic:
← NatTrans.naturality,

Goal state after:
case e_g
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ inv (DerivedCategory.Q.map R.ι') ≫
      (singleFunctor C 0 ⋙ DerivedCategory.Q).map g ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y' =
    DerivedCategory.Q.map φ.hom' ≫
      inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

Goal state before:
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 CokernelCofork.IsColimit.isZero_of_epi
      (CokernelCofork.mapIsColimit _ (cokernelIsCokernel f) G)

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: case hyp
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (F g).right = g
X✝ : ActionCategory G X
t✝ : X
g✝ : G
f : X✝ ⟶ ⟨(), g✝⁻¹ • t✝⟩
⊢ (F ↑(f ≫ homOfPair t✝ g✝)).left (ActionCategory.back ⟨(), t✝⟩) =
    (F ↑f).left (ActionCategory.back ⟨(), g✝⁻¹ • t✝⟩) ≫ (F ↑(homOfPair t✝ g✝)).left (ActionCategory.back ⟨(), t✝⟩)

Tactic:
simp [SingleObj.comp_as_mul, sane]

Goal state after:
case hyp
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (F g).right = g
X✝ : ActionCategory G X
t✝ : X
g✝ : G
f : X✝ ⟶ ⟨(), g✝⁻¹ • t✝⟩
⊢ (g✝ • (F ↑f).left) t✝ = (F ↑f).left (g✝⁻¹ • t✝)
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v a b : G
h : a ≈ b
⊢ a * v⁻¹ ≈ b * v⁻¹

Tactic:
apply (QuotientGroup.leftRel_apply).mpr
      -- We avoid `group` here to minimize imports while low in the hierarchy;
      -- typically it would be better to invoke the tactic.
      simpa [mul_assoc] using Subgroup.Normal.conj_mem ‹_› _ (QuotientGroup.leftRel_apply.mp h) _

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: V : Type (u + 1)
inst✝³ : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst✝² : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝¹ : ConcreteCategory V FV
G : Type u_3
inst✝ : Monoid G
X : Action V G
g h : G
x : ToType X
⊢ (g * h) • x = g • h • x

Tactic:
change ConcreteCategory.hom (X.ρ (g * h)) x =
      ConcreteCategory.hom (X.ρ g) ((ConcreteCategory.hom (X.ρ h)) x)

Goal state after:
V : Type (u + 1)
inst✝³ : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst✝² : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝¹ : ConcreteCategory V FV
G : Type u_3
inst✝ : Monoid G
X : Action V G
g h : G
x : ToType X
⊢ (ConcreteCategory.hom (X.ρ (g * h))) x = (ConcreteCategory.hom (X.ρ g)) ((ConcreteCategory.hom (X.ρ h)) x)
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.PreservesMonomorphisms
this : L.EssSurj
W : D
⊢ ∀ (z : W ⟶ L.obj X), z ≫ L.map f = 0 → ∃ l, l ≫ L.map (kernel.ι f) = z

Tactic:
w

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.PreservesMonomorphisms
this : L.EssSurj
W : D
w : W ⟶ L.obj X
⊢ w ≫ L.map f = 0 → ∃ l, l ≫ L.map (kernel.ι f) = w
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
⊢ ∀ (X Y Z : C ⥤ D) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g

Tactic:
intros
    ext
    apply smul_comp

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.PreservesEpimorphisms
this : L.EssSurj
W : D
⊢ ∀ (z : L.obj Y ⟶ W), L.map f ≫ z = 0 → ∃ l, L.map (cokernel.π f) ≫ l = z

Tactic:
w

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.PreservesEpimorphisms
this : L.EssSurj
W : D
w : L.obj Y ⟶ W
⊢ L.map f ≫ w = 0 → ∃ l, L.map (cokernel.π f) ≫ l = w
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ { V := F.obj X✝.V, ρ := { toFun := fun g ↦ F.map (X✝.ρ g), map_one' := ⋯, map_mul' := ⋯ } }.ρ g ≫ F.map f.hom =
    F.map f.hom ≫ { V := F.obj Y✝.V, ρ := { toFun := fun g ↦ F.map (Y✝.ρ g), map_one' := ⋯, map_mul' := ⋯ } }.ρ g

Tactic:
by dsimp; rw [← F.map_comp, f.comm, F.map_comp]

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝ : G
⊢ (leftRegular G ⊗ X).ρ x✝ ≫
      { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom =
    { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom ≫
      (leftRegular G ⊗ trivial G X.V).ρ x✝

Tactic:
by
      ext _
      simp only [tensorObj_V, tensor_ρ]
      simp [types_tensorObj_def]
      rfl

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

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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
⊢ { g // F.map (adj₁.unit.app (L.obj Y) ≫ U.map g) = g ≫ F.map (adj₁.unit.app X) } ≃
    { z // z ≫ U.map (F.map (adj₁.unit.app X)) = z ≫ adj₁.unit.app (U.obj (F.obj X)) }

Tactic:
apply (adj₁.homEquiv _ _).subtypeEquiv

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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
⊢ ∀ (a : F.obj (L.obj Y) ⟶ F.obj X),
    F.map (adj₁.unit.app (L.obj Y) ≫ U.map a) = a ≫ F.map (adj₁.unit.app X) ↔
      (adj₁.homEquiv (L.obj Y) (F.obj X)) a ≫ U.map (F.map (adj₁.unit.app X)) =
        (adj₁.homEquiv (L.obj Y) (F.obj X)) a ≫ adj₁.unit.app (U.obj (F.obj X))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
⊢ B ⥤ C

Tactic:
by
  refine Adjunction.rightAdjointOfEquiv
    (fun X Y => (constructRightAdjointEquiv L _ adj₁ adj₂ h X Y).symm) ?_
  intro X Y Y' g h
  rw [constructRightAdjointEquiv_symm_apply, constructRightAdjointEquiv_symm_apply,
    Equiv.symm_apply_eq, Subtype.ext_iff]
  dsimp
  simp only [Adjunction.homEquiv_counit]
  erw [Fork.IsLimit.homIso_natural, Fork.IsLimit.homIso_natural]
  simp only [Fork.ofι_pt, Functor.map_comp, assoc, limit.cone_x]
  erw [adj₂.homEquiv_naturality_left, Equiv.rightInverse_symm]
  simp

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

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
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this✝ : L'.IsLeftAdjoint
this : (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv).IsLeftAdjoint := inferInstance
⊢ L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv ≅ L

Tactic:
exact Functor.isoWhiskerLeft L (Comonad.comparison _).asEquivalence.unitIso.symm ≪≫ L.leftUnitor

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
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ τ = 𝟙 (u ≫ h) ⊗≫ rightZigzag adj.unit adj.counit ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension

Tactic:
adj.right_triangle

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ τ = 𝟙 (u ≫ h) ⊗≫ ((ρ_ u).hom ≫ (λ_ u).inv) ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u) = s.unit

Tactic:
adj.right_triangle

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ s.unit ⊗≫ s.lift ◁ ((ρ_ u).hom ≫ (λ_ u).inv) ⊗≫ 𝟙 (s.lift ≫ u) = s.unit
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ (fun f ↦ { hom := { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
      ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f) =
    f

Tactic:
ext (_ | _) : 4
            · exact f.hom.map_fst.symm
            · rfl

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsCartesian f φ
a' : 𝒳
ψ ψ' : a' ⟶ a
inst✝¹ : p.IsHomLift (𝟙 R) ψ
inst✝ : p.IsHomLift (𝟙 R) ψ'
h : ψ ≫ φ = ψ' ≫ φ
⊢ ψ = ψ'

Tactic:
by
  rw [map_uniq p f φ (ψ ≫ φ) ψ rfl, map_uniq p f φ (ψ ≫ φ) ψ' h.symm]

Goal state after:
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₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
⊢ (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
      enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄ =
    enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄

Tactic:
by
  ext j
  conv_lhs =>
    rw [assoc, assoc, enrichedComp_π,
      tensorHom_def_assoc, ← comp_whiskerRight_assoc, enrichedComp_π,
      comp_whiskerRight_assoc, ← whisker_exchange_assoc,
      ← whisker_exchange_assoc, ← tensorHom_def'_assoc, ← associator_inv_naturality_assoc]
  conv_rhs =>
    rw [assoc, enrichedComp_π, tensorHom_def'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
      enrichedComp_π, MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange_assoc,
      whisker_exchange_assoc, ← tensorHom_def_assoc]
  dsimp
  rw [e_assoc]

Goal state after:
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✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
⊢ (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j))) ≫
      eHomWhiskerLeft V (F₁.obj j) (F₂.map f) =
    (s.π.app j' ≫ enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j'))) ≫
      eHomWhiskerRight V (F₁.map f) (F₂.obj j')

Tactic:
rw [← s.w f, assoc, assoc, 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✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₁ F₂
s : Cone (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
⊢ s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) ≫
        eHomWhiskerLeft V (F₁.obj j) (F₂.map f) =
    s.π.app j ≫
      (functorEnrichedHom V F₁ F₂).map f ≫
        enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j')) ≫
          eHomWhiskerRight V (F₁.map f) (F₂.obj j')
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁴ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝³ : HasZeroMorphisms C
inst✝² : (i : I) → HasZeroMorphisms (D i)
inst✝¹ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝ : HasZeroObject C
X : C
⊢ IsZero X ↔ ∀ (i : I), IsZero ((F i).obj X)

Tactic:
refine ⟨fun hX _ ↦ Functor.map_isZero _ hX, fun hX ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁴ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝³ : HasZeroMorphisms C
inst✝² : (i : I) → HasZeroMorphisms (D i)
inst✝¹ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝ : HasZeroObject C
X : C
hX : ∀ (i : I), IsZero ((F i).obj X)
⊢ IsZero X
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
⊢ IsIso i

Tactic:
obtain ⟨(y : Y.V)⟩ := (not_initial_iff_fiber_nonempty (Action.forget _ _) Y).mp hni

Goal state after:
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
⊢ IsIso i
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
⊢ IsGalois X ↔ MulAction.IsPretransitive (Aut X) (F.obj X).obj

Tactic:
by
  rw [isGalois_iff_aux, Equiv.nonempty_congr <| quotientByAutTerminalEquivUniqueQuotient F X]
  exact (MulAction.pretransitive_iff_unique_quotient_of_nonempty (Aut X) (F.obj X)).symm

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
h : IsIso (𝟙 ((functorToAction F).obj X))
⊢ IsIso (i ≫ (functorToAction F).map prod.fst)

Tactic:
by simpa [i, u]

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 (t.app X)) ((ConcreteCategory.hom (F.map φ.hom)) y) =
    (ConcreteCategory.hom (F.map φ.hom)) ((ConcreteCategory.hom (t.app X)) y)

Tactic:
FunctorToFintypeCat.naturality

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
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)) ((ConcreteCategory.hom (t.app X)) y) =
    (ConcreteCategory.hom (F.map φ.hom)) ((ConcreteCategory.hom (t.app X)) y)
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

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

Tactic:
biprod.inl_desc_assoc,

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
f g : X ⟶ Y
h₁ : f.f = g.f
i : X.I
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
by rw [h₁]

Goal state after: