awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.Exact
rw :
  Function.Exact (M := (↑(ShortComplex.X₁ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v))) (N :=
    (↑(ShortComplex.X₂ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v))) (P :=
    (↑(ShortComplex.X₃ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u_1 v)) →ₗ[R] (↑x2 : Type (max u_1 v)))
          (CC := carrier) (X := ShortComplex.X₁ (S.map (uliftFunctor.{u_1, v, u} R)))
          (ShortComplex.f (S.map (uliftFunctor.{u_1, v, u} R)))) :
      (a : (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₁ : Type (max u_1 v))) →
        (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₂ : Type (max u_1 v)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u_1 v)) →ₗ[R] (↑x2 : Type (max u_1 v)))
          (CC := carrier) (X := ShortComplex.X₂ (S.map (uliftFunctor.{u_1, v, u} R)))
          (ShortComplex.g (S.map (uliftFunctor.{u_1, v, u} R)))) :
      (a : (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₂ : Type (max u_1 v))) →
        (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₃ : Type (max u_1 v)))
⊢ ShortComplex.Exact (S.map (uliftFunctor.{u_1, v, u} R))

Tactic:
rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact]

Premises used: CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.Exact
dsimp :
  Function.Exact (M := ULift.{u_1, v} (↑S.X₁ : Type v)) (N := ULift.{u_1, v} (↑S.X₂ : Type v)) (P :=
    ULift.{u_1, v} (↑S.X₃ : Type v))
    (Function.comp (β := (↑S.X₂ : Type v))
      (⇑(LinearEquiv.symm ULift.moduleEquiv) : (a : (↑S.X₂ : Type v)) → ULift.{u_1, v} (↑S.X₂ : Type v))
      (Function.comp (β := (↑S.X₁ : Type v)) (⇑(Hom.hom S.f) : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
        (⇑ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v))))
    (Function.comp (β := (↑S.X₃ : Type v))
      (⇑(LinearEquiv.symm ULift.moduleEquiv) : (a : (↑S.X₃ : Type v)) → ULift.{u_1, v} (↑S.X₃ : Type v))
      (Function.comp (β := (↑S.X₂ : Type v)) (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
        (⇑ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v))))
⊢ Function.Exact (M := (↑(ShortComplex.X₁ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v))) (N :=
    (↑(ShortComplex.X₂ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v))) (P :=
    (↑(ShortComplex.X₃ (S.map (uliftFunctor.{u_1, v, u} R))) : Type (max u_1 v)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u_1 v)) →ₗ[R] (↑x2 : Type (max u_1 v)))
          (CC := carrier) (X := ShortComplex.X₁ (S.map (uliftFunctor.{u_1, v, u} R)))
          (ShortComplex.f (S.map (uliftFunctor.{u_1, v, u} R)))) :
      (a : (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₁ : Type (max u_1 v))) →
        (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₂ : Type (max u_1 v)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u_1 v)) →ₗ[R] (↑x2 : Type (max u_1 v)))
          (CC := carrier) (X := ShortComplex.X₂ (S.map (uliftFunctor.{u_1, v, u} R)))
          (ShortComplex.g (S.map (uliftFunctor.{u_1, v, u} R)))) :
      (a : (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₂ : Type (max u_1 v))) →
        (↑(S.map (uliftFunctor.{u_1, v, u} R)).X₃ : Type (max u_1 v)))

Tactic:
dsimp [uliftFunctor]

Premises used: ModuleCat.uliftFunctor
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.Exact
x : ULift.{u_1, v} (↑S.X₂ : Type v)
simp :
  Eq (α := (↑S.X₃ : Type v))
      ((Hom.hom S.g : (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
          ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v)) :
        (↑S.X₃ : Type v))
      (0 : (↑S.X₃ : Type v)) ↔
    ∃ (y : ULift.{u_1, v} (↑S.X₁ : Type v)),
      Eq (α := (↑S.X₂ : Type v))
        ((Hom.hom S.f : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
            ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v)) y : (↑S.X₁ : Type v)) :
          (↑S.X₂ : Type v))
        ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v))
⊢ Eq (α := ULift.{u_1, v} (↑S.X₃ : Type v))
      (Function.comp (β := (↑S.X₃ : Type v))
        (⇑(LinearEquiv.symm ULift.moduleEquiv) : (a : (↑S.X₃ : Type v)) → ULift.{u_1, v} (↑S.X₃ : Type v))
        (Function.comp (β := (↑S.X₂ : Type v)) (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
          (⇑ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)))
        x)
      0 ↔
    Membership.mem (γ := Set (ULift.{u_1, v} (↑S.X₂ : Type v)))
      (Set.range (ι := ULift.{u_1, v} (↑S.X₁ : Type v))
        (Function.comp (β := (↑S.X₂ : Type v))
          (⇑(LinearEquiv.symm ULift.moduleEquiv) : (a : (↑S.X₂ : Type v)) → ULift.{u_1, v} (↑S.X₂ : Type v))
          (Function.comp (β := (↑S.X₁ : Type v)) (⇑(Hom.hom S.f) : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
            (⇑ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v)))))
      x

Tactic:
simp only [Function.comp_apply, Set.mem_range, LinearEquiv.symm_apply_eq, map_zero]

Premises used: Set.mem_range, LinearEquiv.symm_apply_eq, map_zero, Function.comp_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.Exact
x : ULift.{u_1, v} (↑S.X₂ : Type v)
rw :
  Membership.mem (α := (↑S.X₂ : Type v)) (γ := Set (↑S.X₂ : Type v))
      (Set.range (ι := (↑S.X₁ : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) S.f) :
          (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v)))
      ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v)) ↔
    ∃ (y : ULift.{u_1, v} (↑S.X₁ : Type v)),
      Eq (α := (↑S.X₂ : Type v))
        ((Hom.hom S.f : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
            ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v)) y : (↑S.X₁ : Type v)) :
          (↑S.X₂ : Type v))
        ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v))
⊢ Eq (α := (↑S.X₃ : Type v))
      ((Hom.hom S.g : (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
          ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v)) :
        (↑S.X₃ : Type v))
      (0 : (↑S.X₃ : Type v)) ↔
    ∃ (y : ULift.{u_1, v} (↑S.X₁ : Type v)),
      Eq (α := (↑S.X₂ : Type v))
        ((Hom.hom S.f : (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
            ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₁ : Type v)) → (↑S.X₁ : Type v)) y : (↑S.X₁ : Type v)) :
          (↑S.X₂ : Type v))
        ((ULift.moduleEquiv : (a : ULift.{u_1, v} (↑S.X₂ : Type v)) → (↑S.X₂ : Type v)) x : (↑S.X₂ : Type v))

Tactic:
rw [(CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact S).mp h]

Premises used: CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
⊢ Limits.PreservesFiniteLimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R) ∧
    Limits.PreservesFiniteColimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)

Tactic:
have := ((CategoryTheory.Functor.exact_tfae (uliftFunctor.{v', v} R)).out 1 3).mp
    (uliftFunctor_map_exact R)
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
this :
  Limits.PreservesFiniteLimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R) ∧
    Limits.PreservesFiniteColimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)
⊢ Limits.PreservesFiniteColimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
this :
  Limits.PreservesFiniteLimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R) ∧
    Limits.PreservesFiniteColimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)
⊢ Limits.PreservesFiniteColimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)

Tactic:
exact this.2

Premises used: And.right
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
proj : Projective M
⊢ Small.{max v v', u} R

Tactic:
have := small_lift.{u, v'} R
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
proj : Projective M
this : Small.{max v v', u} R
⊢ Projective (C := ModuleCat R) (of R (ULift.{v', v} (↑M : Type v)))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.MonCat.Adjunctions
Goal:
X' X : Semigrp
Y : MonCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) Semigrp (FD :=
        fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CD := Semigrp.carrier))
      Y
⊢ Eq (α := (↑Y : Type u))
    ((Hom.hom
            ((Equiv.symm
                  (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier)) :
                (a : ToHom (adjoinOne.obj X') Y) → adjoinOne.obj X' ⟶ Y)
              ((Equiv.symm
                      (Equiv.trans (Equiv.symm WithOne.lift)
                        (Equiv.symm
                          (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦
                            (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := Semigrp.carrier)))) :
                    (a : X' ⟶ (forget₂ MonCat Semigrp).obj Y) → ToHom (adjoinOne.obj X') Y)
                  (f ≫ g) :
                ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                  (adjoinOne.obj X') Y)) :
          (a : WithOne (↑X' : Type u)) → (↑Y : Type u))
        none :
      (↑Y : Type u))
    ((MonoidHom.comp
            (Hom.hom
              ((Equiv.symm
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                      (CC := carrier)) :
                  (a : ToHom (adjoinOne.obj X) Y) → adjoinOne.obj X ⟶ Y)
                ((Equiv.symm
                        (Equiv.trans (Equiv.symm WithOne.lift)
                          (Equiv.symm
                            (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦
                              (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := Semigrp.carrier)))) :
                      (a : X ⟶ (forget₂ MonCat Semigrp).obj Y) → ToHom (adjoinOne.obj X) Y)
                    g :
                  ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    (adjoinOne.obj X) Y)))
            (Hom.hom (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f)))) :
          (a : WithOne (↑X' : Type u)) → (↑Y : Type u))
        none :
      (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.MonCat.Adjunctions
Goal:
X' X : Semigrp
Y : MonCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) Semigrp (FD :=
        fun (x1 x2 : Semigrp.{u}) ↦ (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CD := Semigrp.carrier))
      Y
val : (↑X' : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((Hom.hom
            ((Equiv.symm
                  (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier)) :
                (a : ToHom (adjoinOne.obj X') Y) → adjoinOne.obj X' ⟶ Y)
              ((Equiv.symm
                      (Equiv.trans (Equiv.symm WithOne.lift)
                        (Equiv.symm
                          (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦
                            (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := Semigrp.carrier)))) :
                    (a : X' ⟶ (forget₂ MonCat Semigrp).obj Y) → ToHom (adjoinOne.obj X') Y)
                  (f ≫ g) :
                ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                  (adjoinOne.obj X') Y)) :
          (a : WithOne (↑X' : Type u)) → (↑Y : Type u))
        (some val) :
      (↑Y : Type u))
    ((MonoidHom.comp
            (Hom.hom
              ((Equiv.symm
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                      (CC := carrier)) :
                  (a : ToHom (adjoinOne.obj X) Y) → adjoinOne.obj X ⟶ Y)
                ((Equiv.symm
                        (Equiv.trans (Equiv.symm WithOne.lift)
                          (Equiv.symm
                            (ConcreteCategory.homEquiv (FC := fun (x1 x2 : Semigrp.{u}) ↦
                              (↑x1 : Type u) →ₙ* (↑x2 : Type u)) (CC := Semigrp.carrier)))) :
                      (a : X ⟶ (forget₂ MonCat Semigrp).obj Y) → ToHom (adjoinOne.obj X) Y)
                    g :
                  ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                    (adjoinOne.obj X) Y)))
            (Hom.hom (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f)))) :
          (a : WithOne (↑X' : Type u)) → (↑Y : Type u))
        (some val) :
      (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.MonCat.Adjunctions
Goal:
X' X : Type u
Y : MonCat
x : X' ⟶ X
x_1 :
  X ⟶ Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y
x_2 : X'
⊢ Eq (α := (↑Y : Type u))
    (((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) carrier _ _
              (free.obj X') Y
              ((Equiv.symm
                    (Equiv.trans (β :=
                      ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                        (free.obj X') Y)
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeMonoid.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X' ⟶ (forget MonCat).obj Y) → free.obj X' ⟶ Y)
                (x ≫ x_1)) :
            (↑(free.obj X') : Type u) →* (↑Y : Type u)) :
          (a : FreeMonoid X') → (↑Y : Type u))
        (FreeMonoid.of x_2) :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (Y := Y)
            (free.map x ≫
              (Equiv.symm
                    (Equiv.trans (β :=
                      ToHom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                        (free.obj X) Y)
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeMonoid.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X ⟶ (forget MonCat).obj Y) → free.obj X ⟶ Y)
                x_1) :
          (a : FreeMonoid X') → (↑Y : Type u))
        (FreeMonoid.of x_2) :
      (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.MonCat.Adjunctions
Goal:
⊢ Functor.IsRightAdjoint
    (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: Nonempty.intro, Exists.intro, MonCat.adj, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.Category.MonCat.Adjunctions
Goal:
⊢ free.IsLeftAdjoint

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: AddCommMonCat.adj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.Algebra.Category.MonCat.Adjunctions
Goal:
⊢ Functor.IsRightAdjoint
    (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: AddCommMonCat.adj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.Category.MonCat.Adjunctions
Goal:
⊢ Functor.IsRightAdjoint
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
⟨_, ⟨AddCommMonCat.adj.comp AddCommMonCat.equivalence.toAdjunction⟩⟩

Premises used: AddCommMonCat.equivalence, AddCommMonCat.adj, Nonempty.intro, Exists.intro, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.Adjunction.comp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X : MonCat
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y Z : MonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : MonCat
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget MonCat (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget MonCat (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget MonCat (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget MonCat).obj X)) → (fun (X : Type u_1) ↦ X) ((forget MonCat).obj Y))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          f) :
      (a : (↑X : Type u_1)) → (↑Y : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : MonCat
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M : Type u
inst : Monoid M
⊢ (↑(of M) : Type u) = M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M : MonCat
⊢ Hom.hom (𝟙 M) = MonoidHom.id (↑M : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M : MonCat
x : (↑M : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 M) :
        (a : (↑M : Type u_1)) → (↑M : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N T : MonCat
f : M ⟶ N
g : N ⟶ T
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N T : MonCat
f : M ⟶ N
g : N ⟶ T
x : (↑M : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑M : Type u_1)) → (↑T : Type u_1))
        x :
      (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier) g :
          (a : (↑N : Type u_1)) → (↑T : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
                f :
              (a : (↑M : Type u_1)) → (↑N : Type u_1))
            x :
          (↑N : Type u_1)) :
      (↑T : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : MonCat
f g : M ⟶ N
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: MonCat.Hom.ext
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : Type u
inst : Monoid M
inst_1 : Monoid N
f : M →* N
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : MonCat
f : M ⟶ N
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M : Type u
inst : Monoid M
⊢ ofHom (MonoidHom.id M) = 𝟙 (of M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N P : Type u
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
f : M →* N
g : N →* P
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : Type u
inst : Monoid X
inst_1 : Monoid Y
f : X →* Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of X) : Type u)) → (↑(of Y) : Type u))
        x :
      (↑(of Y) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : MonCat
e : M ≅ N
x : (↑M : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑N : Type u_1)) → (↑M : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              e.hom :
            (a : (↑M : Type u_1)) → (↑N : Type u_1))
          x :
        (↑N : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
M N : MonCat
e : M ≅ N
s : (↑N : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑M : Type u_1)) → (↑N : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              e.inv :
            (a : (↑N : Type u_1)) → (↑M : Type u_1))
          s :
        (↑M : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : MonCat
⊢ Eq.{u + 1} (α := (↑X : Type u) →* (↑Y : Type u)) (Hom.hom 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
X Y : MonCat
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u)) ((Hom.hom 1 : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)) (1 : (↑Y : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.MonCat.Basic
Goal:
A : Type u_1
inst : Monoid A
⊢ Eq.{u_1 + 1} (α := (↑(of A) : Type u_1)) 1 1

Tactic:
rfl

Premises used: rfl