awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
z : (CatCenter.{v, u} C)ˣ
X Y : C
f : X ≅ Y
⊢ (z • f).hom = f.hom ≫ (↑z : CatCenter C).app Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
z : (CatCenter.{v, u} C)ˣ
X Y : C
f : X ≅ Y
⊢ (z • f).hom = (↑z : CatCenter C).app X ≫ f.hom

Tactic:
z.1.naturality f.hom

Premises used: Units.val, CategoryTheory.CatCenter.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
z : (CatCenter.{v, u} C)ˣ
X Y : C
f : X ≅ Y
⊢ (z • f).inv = f.inv ≫ (↑z⁻¹ : CatCenter C).app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
z : (CatCenter.{v, u} C)ˣ
X Y : C
f : X ≅ Y
⊢ (z • f).inv = (↑z⁻¹ : CatCenter C).app Y ≫ f.inv

Tactic:
z.2.naturality f.inv

Premises used: CategoryTheory.CatCenter.naturality, Units.inv, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
rw :
  { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } =
    HMul.hMul (α := CatCenter.{v, u} C)
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
⊢ { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } =
    HMul.hMul (α := CatCenter.{v, u} C)
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
h :
  ∀ (X : C),
    CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } X =
      (HMul.hMul (α := CatCenter.{v, u} C)
            { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ :
              NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
            { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ :
              NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }).app
        X
⊢ { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } =
    HMul.hMul (α := CatCenter.{v, u} C)
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
X : C
h :
  Eq.{v + 1} (α := X ⟶ X)
    (CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } X)
    (CatCenter.app
        { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
        X ≫
      CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ } X)
⊢ CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } X =
    (HMul.hMul (α := CatCenter.{v, u} C)
          { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
          { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ :
            NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }).app
      X

Tactic:
dsimp only [CatCenter.mul_app']

Premises used: CategoryTheory.CatCenter.mul_app'
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
X : C
h :
  CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } X =
    HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X ≫ 𝟙 X)
⊢ Eq.{v + 1} (α := X ⟶ X)
    (CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } X)
    (CatCenter.app
        { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
        X ≫
      CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ } X)

Tactic:
rw [Linear.smul_comp, Linear.comp_smul, smul_smul]

Premises used: smul_smul, CategoryTheory.Linear.comp_smul, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
X : C
⊢ CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X), naturality := ⋯ } X =
    HSMul.hSMul (β := X ⟶ X) (a * b) (𝟙 X ≫ 𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
h :
  ∀ (X : C),
    CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a + b) (𝟙 X), naturality := ⋯ } X =
      (HAdd.hAdd (α := CatCenter.{v, u} C)
            { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ :
              NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
            { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ :
              NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }).app
        X
⊢ { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a + b) (𝟙 X), naturality := ⋯ } =
    HAdd.hAdd (α := CatCenter.{v, u} C)
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
      { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
a b : R
X : C
⊢ CatCenter.app { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) (a + b) (𝟙 X), naturality := ⋯ } X =
    (HAdd.hAdd (α := CatCenter.{v, u} C)
          { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) a (𝟙 X), naturality := ⋯ : NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }
          { app := fun (X : C) ↦ HSMul.hSMul (β := X ⟶ X) b (𝟙 X), naturality := ⋯ :
            NatTrans.{v, v, u, u} (𝟭 C) (𝟭 C) }).app
      X

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
a : R
f : X ⟶ Y
⊢ a • f = CatCenter.app ((φ : (a : R) → CatCenter C) a) X ≫ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
a : R
f : X ⟶ Y
rw : CatCenter.app ((φ : (a : R) → CatCenter C) a) X ≫ f = f ≫ CatCenter.app ((φ : (a : R) → CatCenter C) a) Y
⊢ a • f = f ≫ CatCenter.app ((φ : (a : R) → CatCenter C) a) Y

Tactic:
rw [smulOfRingMorphism_smul_eq]

Premises used: CategoryTheory.Linear.smulOfRingMorphism_smul_eq
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
a : R
f : X ⟶ Y
⊢ CatCenter.app ((φ : (a : R) → CatCenter C) a) X ≫ f = f ≫ CatCenter.app ((φ : (a : R) → CatCenter C) a) Y

Tactic:
((φ a).naturality f).symm

Premises used: CategoryTheory.CatCenter.naturality, Eq.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
a : R
f : X ⟶ Y
⊢ CatCenter.app ((φ : (a : R) → CatCenter C) a) X ≫ f = f ≫ CatCenter.app ((φ : (a : R) → CatCenter C) a) Y

Tactic:
exact ((φ a).naturality f).symm

Premises used: CategoryTheory.CatCenter.naturality, Eq.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
this : SMul.{w, v} R (X ⟶ Y) := smulOfRingMorphism φ X Y
a b : R
f : X ⟶ Y
⊢ (a * b) • f = a • b • f

Tactic:
simp only [smulOfRingMorphism_smul_eq', Functor.id_obj, map_mul, End.mul_def,
        NatTrans.comp_app, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.smulOfRingMorphism_smul_eq', CategoryTheory.End.mul_def, map_mul, CategoryTheory.Functor.id_obj, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
this : SMul.{w, v} R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : X ⟶ Y
⊢ HSMul.hSMul.{w, v, v} (α := R) 1 a = a

Tactic:
simp only [smulOfRingMorphism_smul_eq,
        Functor.id_obj, map_one, End.one_def, NatTrans.id_app, id_comp]

Premises used: CategoryTheory.Linear.smulOfRingMorphism_smul_eq, map_one, CategoryTheory.Functor.id_obj, CategoryTheory.End.one_def, CategoryTheory.NatTrans.id_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
this : SMul.{w, v} R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : R
⊢ HSMul.hSMul (β := X ⟶ Y) a 0 = 0

Tactic:
simp only [smulOfRingMorphism_smul_eq, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Linear.smulOfRingMorphism_smul_eq
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
this : SMul.{w, v} R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : R
b : X ⟶ Y
⊢ ∀ (y : X ⟶ Y), a • (b + y) = a • b + a • y

Tactic:
simp [smulOfRingMorphism_smul_eq]

Premises used: CategoryTheory.Linear.smulOfRingMorphism_smul_eq
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
this : SMul.{w, v} R (X ⟶ Y) := smulOfRingMorphism φ X Y
a b : R
f : X ⟶ Y
⊢ (a + b) • f = a • f + b • f

Tactic:
simp [smulOfRingMorphism_smul_eq]

Premises used: CategoryTheory.Linear.smulOfRingMorphism_smul_eq
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
this : SMul.{w, v} R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : X ⟶ Y
⊢ HSMul.hSMul.{w, v, v} (α := R) 0 a = 0

Tactic:
simp only [smulOfRingMorphism_smul_eq, map_zero,
        zero_app, zero_comp]

Premises used: CategoryTheory.Linear.smulOfRingMorphism_smul_eq, map_zero, CategoryTheory.Limits.zero_app, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
this : SMul.{w, v} R (X ⟶ Y) := smulOfRingMorphism φ X Y
⊢ Module.{w, v} R (X ⟶ Y)

Tactic:
exact
  { one_smul := fun a => by
      simp only [smulOfRingMorphism_smul_eq,
        Functor.id_obj, map_one, End.one_def, NatTrans.id_app, id_comp]
    mul_smul := fun a b f => by
      simp only [smulOfRingMorphism_smul_eq', Functor.id_obj, map_mul, End.mul_def,
        NatTrans.comp_app, assoc]
    smul_zero := fun a => by
      simp only [smulOfRingMorphism_smul_eq, comp_zero]
    zero_smul := fun a => by
      simp only [smulOfRingMorphism_smul_eq, map_zero,
        zero_app, zero_comp]
    smul_add := fun a b => by
      simp [smulOfRingMorphism_smul_eq]
    add_smul := fun a b f => by
      simp [smulOfRingMorphism_smul_eq] }
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X_1 Y_1 : C
this : (X Y : C) → Module.{w, v} R (X ⟶ Y) := homModuleOfRingMorphism φ
X Y Z : C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
simp only [smulOfRingMorphism_smul_eq, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.smulOfRingMorphism_smul_eq
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X_1 Y_1 : C
this : (X Y : C) → Module.{w, v} R (X ⟶ Y) := homModuleOfRingMorphism φ
X Y Z : C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
simp only [smulOfRingMorphism_smul_eq', assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.smulOfRingMorphism_smul_eq'
-- Module: Mathlib.CategoryTheory.Center.Linear
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
φ : R →+* CatCenter.{v, u} C
X Y : C
this : (X Y : C) → Module.{w, v} R (X ⟶ Y) := homModuleOfRingMorphism φ
⊢ Linear.{w, v, u} R C

Tactic:
exact
    { smul_comp := fun X Y Z r f g => by simp only [smulOfRingMorphism_smul_eq, assoc]
      comp_smul := fun X Y Z f r g => by simp only [smulOfRingMorphism_smul_eq', assoc] }
-- Module: Mathlib.CategoryTheory.Center.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
r : CatCenter.{v₁, u₁} C
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
X : C
dsimp : app (Localization.liftNatTrans L W L L (𝟭 D) (𝟭 D) (Functor.whiskerRight r L)) (L.obj X) = L.map (r.app X)
⊢ (r.localization L W).app (L.obj X) = L.map (r.app X)

Tactic:
dsimp [localization]

Premises used: CategoryTheory.CatCenter.localization
-- Module: Mathlib.CategoryTheory.Center.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
r : CatCenter.{v₁, u₁} C
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
X : C
⊢ app (Localization.liftNatTrans L W L L (𝟭 D) (𝟭 D) (Functor.whiskerRight r L)) (L.obj X) = L.map (r.app X)

Tactic:
simp only [Localization.liftNatTrans_app, Functor.id_obj, Functor.whiskerRight_app,
    NatTrans.naturality, Functor.comp_map, Functor.id_map, Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Functor.id_map, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Center.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
r s : CatCenter.{v₂, u₂} D
h : ∀ (X : C), Eq (α := L.obj X ⟶ L.obj X) (r.app (L.obj X)) (s.app (L.obj X))
⊢ r = s

Tactic:
Localization.natTrans_ext L W h

Premises used: CategoryTheory.Localization.natTrans_ext, CategoryTheory.End
-- Module: Mathlib.CategoryTheory.Center.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
X : C
⊢ (localization 1 L W).app (L.obj X) = app 1 (L.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Center.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
r s : CatCenter.{v₁, u₁} C
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
X : C
⊢ Eq (α := L.obj X ⟶ L.obj X) (((r * s).localization L W).app (L.obj X))
    ((r.localization L W * s.localization L W).app (L.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Center.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
inst_3 : Preadditive.{v₁, u₁} C
inst_4 : Preadditive.{v₂, u₂} D
inst_5 : L.Additive
X : C
⊢ (localization 0 L W).app (L.obj X) = app 0 (L.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Center.Localization
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
r s : CatCenter.{v₁, u₁} C
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
inst_3 : Preadditive.{v₁, u₁} C
inst_4 : Preadditive.{v₂, u₂} D
inst_5 : L.Additive
⊢ ∀ (X : C),
    Eq (α := L.obj X ⟶ L.obj X) (((r + s).localization L W).app (L.obj X))
      ((r.localization L W + s.localization L W).app (L.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Center.NegOnePow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
n : ℤ
X : C
inl :
  ∀ (n : ℤ),
    (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (n + n)) : CatCenter C).app X =
      HSMul.hSMul (β := X ⟶ X) (n + n).negOnePow (𝟙 X)
inr :
  ∀ (n : ℤ),
    (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (2 * n + 1)) : CatCenter C).app X =
      HSMul.hSMul (β := X ⟶ X) (2 * n + 1).negOnePow (𝟙 X)
⊢ (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) n) : CatCenter C).app X = HSMul.hSMul (β := X ⟶ X) n.negOnePow (𝟙 X)

Tactic:
obtain ⟨n, rfl⟩ | ⟨n, rfl⟩ := Int.even_or_odd n

Premises used: Int.even_or_odd, rfl
-- Module: Mathlib.CategoryTheory.Center.NegOnePow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
n : ℤ
⊢ (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (n + n)) : CatCenter C).app X =
    HSMul.hSMul (β := X ⟶ X) (n + n).negOnePow (𝟙 X)

Tactic:
simp [zpow_add, ← mul_zpow, Int.negOnePow_even _ (Even.add_self n)]

Premises used: Even.add_self, zpow_add, mul_zpow, Int.negOnePow_even
-- Module: Mathlib.CategoryTheory.Center.NegOnePow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
n : ℤ
⊢ Odd (2 * n + 1)

Tactic:
odd_two_mul_add_one n

Premises used: odd_two_mul_add_one
-- Module: Mathlib.CategoryTheory.Center.NegOnePow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
n : ℤ
⊢ Odd (2 * n + 1)

Tactic:
exact odd_two_mul_add_one n

Premises used: odd_two_mul_add_one
-- Module: Mathlib.CategoryTheory.Center.NegOnePow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
n : ℤ
inr :
  (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (2 * n + 1)) : CatCenter C).app X =
    HSMul.hSMul (α := ℤˣ) (β := X ⟶ X) (-1) (𝟙 X)
⊢ (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (2 * n + 1)) : CatCenter C).app X =
    HSMul.hSMul (β := X ⟶ X) (2 * n + 1).negOnePow (𝟙 X)

Tactic:
rw [Int.negOnePow_odd _ (by exact odd_two_mul_add_one n)]

Premises used: Int.negOnePow_odd
-- Module: Mathlib.CategoryTheory.Center.NegOnePow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
n : ℤ
⊢ (↑(HPow.hPow (α := (CatCenter.{v, u} C)ˣ) (-1) (2 * n + 1)) : CatCenter C).app X =
    HSMul.hSMul (α := ℤˣ) (β := X ⟶ X) (-1) (𝟙 X)

Tactic:
simp [Units.smul_def, zpow_add, Int.two_mul, ← mul_zpow]

Premises used: zpow_add, mul_zpow, Units.smul_def, Int.two_mul
-- Module: Mathlib.CategoryTheory.Center.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
z₁ z₂ : CatCenter.{v, u} C
X : C
⊢ (z₁ + z₂).app X = z₁.app X + z₂.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Center.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
z₁ z₂ : CatCenter.{v, u} C
X : C
⊢ (z₁ - z₂).app X = z₁.app X - z₂.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Center.Preadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
z : CatCenter.{v, u} C
X : C
⊢ (-z).app X = -z.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.CodiscreteCategory
Goal:
α : Type u
X : Codiscrete α
⊢ { as := X.as : Codiscrete α } = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.CodiscreteCategory
Goal:
A : Type u_1
x : (Codiscrete A)ᵒᵖ
⊢ Functor.obj (𝟭 (Codiscrete A)ᵒᵖ) x ≅
    Functor.obj
      (Functor.comp (D := Codiscrete A) (functor fun (x : (Codiscrete A)ᵒᵖ) ↦ (unop x).as)
        (Functor.rightOp (functor fun (x : (Codiscrete A)ᵒᵖ) ↦ (unop x).as)))
      x

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.CodiscreteCategory
Goal:
X : Cat
⊢ adj.unit.app X = Functor.toCatHom (unitApp (↑X : Type u))

Tactic:
rfl

Premises used: CategoryTheory.Codiscrete.functor, CategoryTheory.Functor.toCatHom, rfl, CategoryTheory.Codiscrete.unitApp
-- Module: Mathlib.CategoryTheory.CodiscreteCategory
Goal:
A : Type u
⊢ adj.counit.app A = ↾counitApp A

Tactic:
rfl

Premises used: CategoryTheory.Codiscrete.invFunctor, CategoryTheory.Codiscrete.counitApp, rfl
-- Module: Mathlib.CategoryTheory.CodiscreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
⊢ counitApp C ∘ Functor.obj.{v, 0, u, u} (unitApp C) = _root_.id

Tactic:
rfl

Premises used: CategoryTheory.Codiscrete.counitApp, rfl
-- Module: Mathlib.CategoryTheory.CodiscreteCategory
Goal:
X : Type u
⊢ unitApp (Codiscrete X) ⋙ functorOfFun (counitApp X) = 𝟭 (Codiscrete X)

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, CategoryTheory.Codiscrete.counitApp, rfl
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
⊢ ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)

Tactic:
haveI : ∀ j, DiscreteTopology (F'.obj j) := fun _ => ⟨rfl⟩
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
⊢ ∀ (j : J), Finite.{u + 1} (↑(F'.obj j) : Type u)

Tactic:
haveI : ∀ j, Finite (F'.obj j) := hf
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this_1 : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
this : ∀ (j : J), Finite.{u + 1} (↑(F'.obj j) : Type u)
⊢ ∀ (j : J), Nonempty.{u + 1} (↑(F'.obj j) : Type u)

Tactic:
haveI : ∀ j, Nonempty (F'.obj j) := hne
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this_1 : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
this_2 : ∀ (j : J), Finite.{u + 1} (↑(F'.obj j) : Type u)
this : ∀ (j : J), Nonempty.{u + 1} (↑(F'.obj j) : Type u)
obtain :
  ∀ (u : (j : J) → (↑(F'.obj j) : Type u))
    (hu :
      Membership.mem (γ := Set ((j : J) → (↑(F'.obj j) : Type u)))
        {u : (j : J) → (↑(F'.obj j) : Type u) |
          ∀ {i j : J} (f : i ⟶ j),
            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) (F'.map f) :
                  (a : (↑(F'.obj i) : Type u)) → (↑(F'.obj j) : Type u))
                (u i) =
              u j}
        u),
    F.sections.Nonempty
⊢ F.sections.Nonempty

Tactic:
obtain ⟨⟨u, hu⟩⟩ := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u} F'