awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : MonoidalClosed.{v, u_1} C
X Y Z : C
h₁ :
  Eq.{v + 1} (α :=
    Y ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) (coprod.inl : Y ⟶ coprod.{v, u_1} Y Z)
        (curry (Iso.inv (∂L X Y Z)) :
          coprod.{v, u_1} Y Z ⟶
            Functor.obj.{v, v, u_1, u_1} (ihom X)
              (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))) :
      Y ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) coprod.inl (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
      Y ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
h₂ :
  Eq.{v + 1} (α :=
    Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) (coprod.inr : Z ⟶ coprod.{v, u_1} Y Z)
        (curry (Iso.inv (∂L X Y Z)) :
          coprod.{v, u_1} Y Z ⟶
            Functor.obj.{v, v, u_1, u_1} (ihom X)
              (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))) :
      Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) coprod.inr (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
      Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
⊢ Eq.{v + 1} (α :=
    coprod.{v, u_1} Y Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (curry (Iso.inv (∂L X Y Z)) :
      coprod.{v, u_1} Y Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (coprod.desc (curry coprod.inl) (curry coprod.inr) :
      coprod.{v, u_1} Y Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : MonoidalClosed.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Y ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) (coprod.inl : Y ⟶ coprod.{v, u_1} Y Z)
        (curry (Iso.inv (∂L X Y Z)) :
          coprod.{v, u_1} Y Z ⟶
            Functor.obj.{v, v, u_1, u_1} (ihom X)
              (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))) :
      Y ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) coprod.inl (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
      Y ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))

Tactic:
simp [← curry_natural_left]

Premises used: CategoryTheory.MonoidalClosed.curry_natural_left
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : MonoidalClosed.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) (coprod.inr : Z ⟶ coprod.{v, u_1} Y Z)
        (curry (Iso.inv (∂L X Y Z)) :
          coprod.{v, u_1} Y Z ⟶
            Functor.obj.{v, v, u_1, u_1} (ihom X)
              (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))) :
      Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) coprod.inr (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
      Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))

Tactic:
simp [← curry_natural_left]

Premises used: CategoryTheory.MonoidalClosed.curry_natural_left
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y W : C
f : Y ⟶ X
inst_1 : EffectiveEpi f
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
⊢ f ≫ desc f e ⋯ = e

Tactic:
(EffectiveEpi.getStruct f).fac e h

Premises used: CategoryTheory.EffectiveEpi.getStruct, CategoryTheory.EffectiveEpi.desc, CategoryTheory.EffectiveEpiStruct.fac
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y W : C
f : Y ⟶ X
inst_1 : EffectiveEpi f
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
⊢ m = desc f e ⋯

Tactic:
(EffectiveEpi.getStruct f).uniq e h _ hm

Premises used: CategoryTheory.EffectiveEpi.getStruct, CategoryTheory.EffectiveEpi.desc, CategoryTheory.EffectiveEpiStruct.uniq
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : Y ⟶ X
inst_1 : EffectiveEpi f
Z : C
m₁ m₂ : X ⟶ Z
h_1 : f ≫ m₁ = f ≫ m₂
Z_1 : C
x x_1 : Z_1 ⟶ Y
h : x ≫ f = x_1 ≫ f
⊢ x ≫ f ≫ m₂ = x_1 ≫ f ≫ m₂

Tactic:
simp [← assoc, h]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : Y ⟶ X
inst_1 : EffectiveEpi f
Z : C
m₁ m₂ : X ⟶ Z
h : f ≫ m₁ = f ≫ m₂
rw : m₁ = desc f (f ≫ m₂) ⋯
⊢ m₁ = m₂

Tactic:
rw [show m₂ = desc f (f ≫ m₂) (fun _ _ h => by simp [← assoc, h]) from uniq _ _ _ _ rfl]

Premises used: CategoryTheory.EffectiveEpi.uniq, CategoryTheory.CategoryStruct.comp, rfl
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : Y ⟶ X
inst_1 : EffectiveEpi f
Z : C
m₁ m₂ : X ⟶ Z
h : f ≫ m₁ = f ≫ m₂
⊢ m₁ = desc f (f ≫ m₂) ⋯

Tactic:
uniq _ _ _ _ h

Premises used: CategoryTheory.EffectiveEpi.uniq
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : Y ⟶ X
inst_1 : EffectiveEpi f
Z : C
m₁ m₂ : X ⟶ Z
h : f ≫ m₁ = f ≫ m₂
⊢ m₁ = desc f (f ≫ m₂) ⋯

Tactic:
exact uniq _ _ _ _ h

Premises used: CategoryTheory.EffectiveEpi.uniq
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : EffectiveEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
Z : C
x x_1 : Z ⟶ X
h : x ≫ f = x_1 ≫ f
⊢ x ≫ u = x_1 ≫ u

Tactic:
simpa [← sq.w, cancel_mono_assoc_iff] using h =≫ v

Premises used: CategoryTheory.CommSq.w, CategoryTheory.cancel_mono_assoc_iff
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : EffectiveEpi f
A B : C
z : A ⟶ B
hz : Mono z
u : X ⟶ A
v : Y ⟶ B
sq : CommSq u f z v
this : ∀ {Z : C} (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ u = g₂ ≫ u
⊢ f ≫ desc f u ⋯ ≫ z = f ≫ v

Tactic:
simp [← sq.w]

Premises used: CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a ≫ desc X π e ⋯ = e a

Tactic:
(EffectiveEpiFamily.getStruct X π).fac e h a

Premises used: CategoryTheory.EffectiveEpiFamilyStruct.fac, CategoryTheory.EffectiveEpiFamily.getStruct, CategoryTheory.EffectiveEpiFamily.desc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
⊢ m = desc X π e ⋯

Tactic:
(EffectiveEpiFamily.getStruct X π).uniq e h m hm

Premises used: CategoryTheory.EffectiveEpiFamily.getStruct, CategoryTheory.EffectiveEpiFamilyStruct.uniq, CategoryTheory.EffectiveEpiFamily.desc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h_1 : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ Eq (α := Z ⟶ W) (g₁ ≫ (fun (a : α) ↦ π a ≫ m₂) a₁) (g₂ ≫ (fun (a : α) ↦ π a ≫ m₂) a₂)

Tactic:
simp only [← assoc, h]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
hm : ∀ (a : α), π a ≫ m₂ = π a ≫ m₂
⊢ m₂ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯

Tactic:
apply EffectiveEpiFamily.uniq

Premises used: CategoryTheory.EffectiveEpiFamily.uniq
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
a : α
⊢ π a ≫ m₂ = π a ≫ m₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ m₂ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯

Tactic:
have : m₂ = EffectiveEpiFamily.desc X π (fun a => π a ≫ m₂)
      (fun a₁ a₂ g₁ g₂ h => by simp only [← assoc, h]) := by
    apply EffectiveEpiFamily.uniq; intro; rfl
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
this : m₂ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯
rw : m₁ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯
⊢ m₁ = m₂

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
this : m₂ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯
⊢ m₁ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯

Tactic:
EffectiveEpiFamily.uniq _ _ _ _ _ h

Premises used: CategoryTheory.EffectiveEpiFamily.uniq
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
this : m₂ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯
⊢ m₁ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯

Tactic:
exact EffectiveEpiFamily.uniq _ _ _ _ _ h

Premises used: CategoryTheory.EffectiveEpiFamily.uniq
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
W : C
e : (a : Unit) → X ⟶ W
h :
  ∀ {Z : C} (a₁ a₂ : Unit) (g₁ g₂ : Z ⟶ X),
    Eq (α := Z ⟶ B)
        (g₁ ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a₁ with
          | PUnit.unit => f)
        (g₂ ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a₂ with
          | PUnit.unit => f) →
      g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm :
  ∀ (a : Unit),
    (match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a with
        | PUnit.unit => f) ≫
        m =
      e a
hm₁ : f ≫ m = e ()
⊢ m = desc f (e ()) ⋯

Tactic:
apply EffectiveEpi.uniq f (e ()) (h () ())

Premises used: Unit.unit, CategoryTheory.EffectiveEpi.uniq
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
W : C
e : (a : Unit) → X ⟶ W
h :
  ∀ {Z : C} (a₁ a₂ : Unit) (g₁ g₂ : Z ⟶ X),
    Eq (α := Z ⟶ B)
        (g₁ ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a₁ with
          | PUnit.unit => f)
        (g₂ ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a₂ with
          | PUnit.unit => f) →
      g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm :
  ∀ (a : Unit),
    (match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a with
        | PUnit.unit => f) ≫
        m =
      e a
⊢ f ≫ m = e ()

Tactic:
hm ()

Premises used: Unit.unit
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
W : C
e : (a : Unit) → X ⟶ W
h :
  ∀ {Z : C} (a₁ a₂ : Unit) (g₁ g₂ : Z ⟶ X),
    Eq (α := Z ⟶ B)
        (g₁ ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a₁ with
          | PUnit.unit => f)
        (g₂ ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a₂ with
          | PUnit.unit => f) →
      g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm :
  ∀ (a : Unit),
    (match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a with
        | PUnit.unit => f) ≫
        m =
      e a
⊢ f ≫ m = e ()

Tactic:
exact hm ()

Premises used: Unit.unit
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := B) (fun (x : Unit) ↦ X) fun (x : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
    | PUnit.unit => f

Tactic:
⟨⟨effectiveEpiFamilyStructSingletonOfEffectiveEpi f⟩⟩

Premises used: CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi, Nonempty.intro, CategoryTheory.EffectiveEpiFamily.mk
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst_1 :
  EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := B) (fun (x : Unit) ↦ X) fun (x : Unit) ↦
    match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
    | PUnit.unit => f
⊢ EffectiveEpi f

Tactic:
⟨⟨effectiveEpiStructOfEffectiveEpiFamilySingleton f⟩⟩

Premises used: Nonempty.intro, CategoryTheory.effectiveEpiStructOfEffectiveEpiFamilySingleton, CategoryTheory.EffectiveEpi.mk
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
⊢ EffectiveEpi f ↔
    EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := B) (fun (x : Unit) ↦ X) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) x with
      | PUnit.unit => f

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Iso.hom (asIso (Sigma.desc π)))

Tactic:
simp only [asIso_hom,
      colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.asIso_hom
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Iso.hom (asIso (Sigma.desc π)))

Tactic:
have : π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom := by simp only [asIso_hom,
      colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
this : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Iso.hom (asIso (Sigma.desc π)))
rw :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a)
      (Iso.hom (asIso (Sigma.desc π)) ≫
        CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Iso.inv (asIso (Sigma.desc π))) (Sigma.desc e)) =
    e a
⊢ π a ≫ CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Iso.inv (asIso (Sigma.desc π))) (Sigma.desc e) = e a

Tactic:
rw [this, assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
this : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Iso.hom (asIso (Sigma.desc π)))
⊢ CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a)
      (Iso.hom (asIso (Sigma.desc π)) ≫
        CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Iso.inv (asIso (Sigma.desc π))) (Sigma.desc e)) =
    e a

Tactic:
simp only [asIso_hom, asIso_inv, IsIso.hom_inv_id_assoc, colimit.ι_desc, Cofan.mk_pt,
      Cofan.mk_ι_app]

Premises used: CategoryTheory.asIso_inv, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.asIso_hom
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
simp : Eq (α := sigmaObj.{u_2, v_1, u_1} X ⟶ W) (Sigma.desc π ≫ m) (Sigma.desc e)
⊢ m = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Iso.inv (asIso (Sigma.desc π))) (Sigma.desc e)

Tactic:
simp only [asIso_inv, IsIso.eq_inv_comp]

Premises used: CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.asIso_inv
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
h₁ :
  ∀ (a : α),
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π ≫ m) =
      CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
⊢ Eq (α := sigmaObj.{u_2, v_1, u_1} X ⟶ W) (Sigma.desc π ≫ m) (Sigma.desc e)

Tactic:
ext a
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
a : α
h₁ : π a ≫ m = e a
⊢ CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π ≫ m) =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)

Tactic:
simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app,
      colimit.ι_desc]

Premises used: CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.ι_desc_assoc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
a : α
⊢ π a ≫ m = e a

Tactic:
hm a
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
a : α
⊢ π a ≫ m = e a

Tactic:
exact hm a
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
⟨⟨effectiveEpiFamilyStructOfIsIsoDesc X π⟩⟩

Premises used: Nonempty.intro, CategoryTheory.EffectiveEpiFamily.mk, CategoryTheory.effectiveEpiFamilyStructOfIsIsoDesc
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
W : C
x : X ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ x = g₂ ≫ x
⊢ f ≫ inv f ≫ x = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
W : C
x : X ⟶ W
h_1 : ∀ {Z : C} (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ x = g₂ ≫ x
x_1 : Y ⟶ W
h : f ≫ x_1 = x
⊢ x_1 = inv f ≫ x

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ EffectiveEpi f

Tactic:
⟨⟨effectiveEpiStructOfIsIso f⟩⟩

Premises used: CategoryTheory.effectiveEpiStructOfIsIso, Nonempty.intro, CategoryTheory.EffectiveEpi.mk
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := X) (fun (x : Unit) ↦ X) fun (x : Unit) ↦ 𝟙 X

Tactic:
inferInstance

Premises used: inferInstance