awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n : ℕ
inst :
  Epi.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
inst₁ :
  Epi.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
⊢ Epi.{v_1, u_1} (C := C) (X :=
    Cone.pt.{0, v_1, 0, u_1} (F :=
      pair
        (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
        (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
          if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
      (BinaryFan.mk (P :=
        prod.{v_1, u_1}
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
            if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
            if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
        prod.fst prod.snd))
    (Y :=
    prod.{v_1, u_1}
      (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
      (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))
    (prod.map
      (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
        if h : (↑i : ℕ) < n then eqToHom ⋯
        else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
      (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
        if h : (↑i : ℕ) < n then eqToHom ⋯
        else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯))

Tactic:
apply +allowSynthFailures prod.map_epi

Premises used: CategoryTheory.Limits.prod.map_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n : ℕ
inst :
  ∀ (j : { x : ℕ // x < n + 1 }),
    Epi.{v_1, u_1} (C := C) (X := if x : (↑j : ℕ) < n + 1 then M (↑j : ℕ) else N (↑j : ℕ)) (Y :=
      if x : (↑j : ℕ) < n then M (↑j : ℕ) else N (↑j : ℕ))
      (if h : (↑j : ℕ) < n then eqToHom ⋯
      else if h' : (↑j : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑j : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
⊢ Epi.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
apply +allowSynthFailures Pi.map_epi

Premises used: CategoryTheory.Limits.Pi.map_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : val < n + 1
inst :
  ∀ (h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n),
    Epi.{v_1, u_1} (C := C) (X :=
      if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
        M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
      else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
      (eqToHom ⋯)
inst₁ :
  ∀ (h : ¬(↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n),
    Epi (X :=
      if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
        M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
      else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
      (Y :=
      if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then
        M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
      else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
      (eqToHom ⋯ ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) ≫ eqToHom ⋯)
⊢ Epi.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (Y :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (if h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then eqToHom ⋯
    else
      if h' : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
        eqToHom ⋯ ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) ≫ eqToHom ⋯
      else eqToHom ⋯)

Tactic:
split
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : val < n + 1
h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n
⊢ Epi.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (eqToHom ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : val < n + 1
h : ¬(↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n
⊢ Epi (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (Y :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (eqToHom ⋯ ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) ≫ eqToHom ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n : ℕ
inst :
  IsIso.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
⊢ Epi.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
apply +allowSynthFailures IsIso.epi_of_iso

Premises used: CategoryTheory.IsIso.epi_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n : ℕ
inst :
  ∀ (b : { x : ℕ // ¬x < n + 1 }),
    IsIso.{v_1, u_1} (C := C) (X := if x : (↑b : ℕ) < n + 1 then M (↑b : ℕ) else N (↑b : ℕ)) (Y :=
      if x : (↑b : ℕ) < n then M (↑b : ℕ) else N (↑b : ℕ))
      (if h : (↑b : ℕ) < n then eqToHom ⋯
      else if h' : (↑b : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑b : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
⊢ IsIso.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)

Tactic:
apply +allowSynthFailures Pi.map_isIso

Premises used: CategoryTheory.Limits.Pi.map_isIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : ¬val < n + 1
inst :
  ∀ (h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n),
    IsIso.{v_1, u_1} (C := C) (X :=
      if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
        M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
      else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
      (eqToHom ⋯)
inst₁ :
  ∀ (h : ¬(↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n),
    IsIso.{v_1, u_1} (C := C) (X :=
      if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
        M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
      else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
      (eqToHom ⋯)
⊢ IsIso.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (Y :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (if h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n then eqToHom ⋯
    else
      if h' : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
        eqToHom ⋯ ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) ≫ eqToHom ⋯
      else eqToHom ⋯)

Tactic:
split
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : ¬val < n + 1
h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n
⊢ IsIso.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (eqToHom ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : ¬val < n + 1
h : ¬(↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n
⊢ IsIso.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ ¬x < n + 1) val property) : ℕ))
    (eqToHom ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
g h : M
x : J.obj (SingleObj.star M)
change :
  Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (g * h)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
⊢ (g * h) • x = g • h • x

Tactic:
change J.map (g * h) x = (J.map h ≫ J.map g) x

Premises used: HMul.hMul, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
g h : M
x : J.obj (SingleObj.star M)
rw :
  Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (CategoryStruct.comp (Y := SingleObj.star M) h g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
y : SingleObj M
⊢ Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (g * h)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))

Tactic:
rw [← SingleObj.comp_as_mul]

Premises used: CategoryTheory.SingleObj.comp_as_mul
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
g h : M
x : J.obj (SingleObj.star M)
simp :
  Eq (α := J.obj (SingleObj.star M))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map g) : (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map h) :
              (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
            x :
          J.obj (SingleObj.star M)) :
      J.obj (SingleObj.star M))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map g) : (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map h) :
              (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
            x :
          J.obj (SingleObj.star M)) :
      J.obj (SingleObj.star M))
⊢ Eq (α := (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (CategoryStruct.comp (Y := SingleObj.star M) h g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := J.obj (SingleObj.star M)) (J.map h) (J.map g)) :
          (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
        x :
      (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
g h : M
x : J.obj (SingleObj.star M)
⊢ Eq (α := J.obj (SingleObj.star M))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map g) : (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map h) :
              (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
            x :
          J.obj (SingleObj.star M)) :
      J.obj (SingleObj.star M))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map g) : (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (J.map h) :
              (a : J.obj (SingleObj.star M)) → J.obj (SingleObj.star M))
            x :
          J.obj (SingleObj.star M)) :
      J.obj (SingleObj.star M))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
x : J.obj (SingleObj.star M)
change :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (𝟙 (SingleObj.star M))) :
        (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
      x =
    x
⊢ HSMul.hSMul.{v, u, u} (α := M) 1 x = x

Tactic:
change J.map (𝟙 _) x = x

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
M G : Type v
inst : Monoid M
inst_1 : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj M) (Type u)
x : J.obj (SingleObj.star M)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (J.map (𝟙 (SingleObj.star M))) :
        (a : (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M))) → (fun (X : Type u) ↦ X) (J.obj (SingleObj.star M)))
      x =
    x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
rhs : (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y
| J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y

Tactic:
rhs
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
rw : (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) y x
| (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y

Tactic:
rw [Setoid.comm']

Premises used: Setoid.comm'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
rw : (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) y x
| J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y

Tactic:
rhs; rw [Setoid.comm']

Premises used: Setoid.comm'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
conv :
  J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) y x
⊢ J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) x y

Tactic:
conv => rhs; rw [Setoid.comm']

Premises used: Setoid.comm'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
change : (∃ (g : G), y = g • x) ↔ ∃ (g : G), g • x = y
⊢ J.ColimitTypeRel (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) x)
      (Sigma.mk (β := fun (j : SingleObj G) ↦ J.obj j) (SingleObj.star G) y) ↔
    (MulAction.orbitRel G (J.obj (SingleObj.star G)) : J.obj (SingleObj.star G) → J.obj (SingleObj.star G) → Prop) y x

Tactic:
change (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)

Premises used: Exists, HSMul.hSMul, Eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj
Goal:
G : Type v
inst : Group G
J : Functor.{v, u, 0, u + 1} (SingleObj G) (Type u)
x y : J.obj (SingleObj.star G)
⊢ (∃ (g : G), y = g • x) ↔ ∃ (g : G), g • x = y

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (f ≫ π) = F.map g ≫ F.map π
rw₁ : F.map (g ≫ π) = F.map g ≫ F.map π
rw₂ rw₃ : F.map g ≫ F.map π = F.map g ≫ F.map π
⊢ F.map f ≫ F.map π = F.map g ≫ F.map π

Tactic:
rw [← F.map_comp, q.condition, F.map_comp]

Premises used: CategoryTheory.IsSplitCoequalizer.condition, CategoryTheory.Functor.map_comp