awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
f : i ⟶ i
pos :
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) (𝟙 i) ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map (𝟙 i))
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)

Tactic:
obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _

Premises used: CategoryTheory.CategoryStruct.id, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) (𝟙 i) ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map (𝟙 i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
neg :
  ∀ (f : j ⟶ i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
      ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
⊢ IsIso (F.map f)

Tactic:
haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
neg :
  Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj j)
    ((Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) ≫ inv (F.map f))
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j))
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)

Tactic:
rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj j)
    ((Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) ≫ inv (F.map f))
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j))

Tactic:
apply (H _ h_1).hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
pos :
  ∀ (f : i ⟶ k),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
      (eqToHom ⋯ ≫ F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    (eqToHom ⋯ ≫ F.map f)

Tactic:
cases h_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
k : J
h : ¬k = i
f : i ⟶ k
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    (eqToHom ⋯ ≫ F.map f)

Tactic:
apply (H _ h).hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)

Tactic:
apply (H _ h).hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
refine_3 :
  ∀ (j : J),
    CategoryStruct.comp (Y := limit F)
        (limit.π F i ≫
          limit.lift F
            { pt := F.1 i,
              π :=
                {
                  app := fun (j : J) ↦
                    if h : j = i then eqToHom ⋯
                    else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                  naturality := ⋯ } })
        (limit.π F j) =
      𝟙 (limit F) ≫ limit.π F j
⊢ limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            {
              app := fun (j : J) ↦
                if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
              naturality := ⋯ } } =
    𝟙 (limit F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
refine_3 :
  limit.π F i ≫
      NatTrans.app
        (Cone.π
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
        j =
    𝟙 (limit F) ≫ limit.π F j
⊢ CategoryStruct.comp (Y := limit F)
      (limit.π F i ≫
        limit.lift F
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
      (limit.π F j) =
    𝟙 (limit F) ≫ limit.π F j

Tactic:
rw [assoc, limit.lift_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
refine_3 :
  (limit.π F i ≫
      if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) =
    𝟙 (limit F) ≫ limit.π F j
⊢ limit.π F i ≫
      NatTrans.app
        (Cone.π
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
        j =
    𝟙 (limit F) ≫ limit.π F j

Tactic:
dsimp only
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
pos : ∀ (h : j = i), limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F j
neg :
  ∀ (h : ¬j = i),
    limit.π F i ≫ (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) = 𝟙 (limit F) ≫ limit.π F j
⊢ (limit.π F i ≫
      if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) =
    𝟙 (limit F) ≫ limit.π F j

Tactic:
split_ifs with h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
h : j = i
pos : limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F i
⊢ limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F j

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
pos :
  Eq (α := limit F ⟶ F.obj i) (limit.π F i ≫ 𝟙 (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i)) (limit.π F i)
⊢ limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F i

Tactic:
rw [id_comp, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ Eq (α := limit F ⟶ F.obj i) (limit.π F i ≫ 𝟙 (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i)) (limit.π F i)

Tactic:
comp_id _

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ Eq (α := limit F ⟶ F.obj i) (limit.π F i ≫ 𝟙 (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i)) (limit.π F i)

Tactic:
exact comp_id _

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
h : ¬j = i
⊢ limit.π F i ≫ (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) = 𝟙 (limit F) ≫ limit.π F j

Tactic:
apply (H _ h).hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ Eq (α := F.obj i ⟶ F.obj i)
    (CategoryStruct.comp (Y := limit F)
        (limit.lift F
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
        (limit.π F i) :
      F.obj i ⟶ F.obj i)
    (𝟙 (F.obj i) : F.obj i ⟶ F.obj i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
J : Type v
inst_2 : SmallCategory J
inst_3 : HasTerminal.{v, u} C
A : C
f : terminal.{v, u} C ⟶ A
⊢ IsIso f

Tactic:
terminalIsTerminal.isIso_from _

Premises used: CategoryTheory.Limits.IsTerminal.isIso_from, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
inst_2 : HasTerminal.{v, u} C
A : C
f g : terminal.{v, u} C ⟶ A
⊢ f = g

Tactic:
terminalIsTerminal.strict_hom_ext _ _

Premises used: CategoryTheory.Limits.IsTerminal.strict_hom_ext, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
inst_2 : HasTerminal.{v, u} C
A : C
⊢ Subsingleton.{v + 1} (terminal.{v, u} C ⟶ A)

Tactic:
terminalIsTerminal.subsingleton_to

Premises used: CategoryTheory.Limits.IsTerminal.subsingleton_to, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal.{v, u} I'
this : IsIso (hI'.from I ≫ f)
rw : inv (hI'.from I ≫ f) ≫ hI'.from I ≫ f = 𝟙 A
rw₁ rw₂ : Eq.{v + 1} (α := A ⟶ A) (𝟙 A) (𝟙 A)
⊢ (inv (hI'.from I ≫ f) ≫ hI'.from I) ≫ f = 𝟙 A

Tactic:
rw [assoc, IsIso.inv_hom_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst_1 : Epi f
hf : ∀ (X Y : C) (z : X ⟶ Y), Mono z → ∀ (u : P ⟶ X) (v : Q ⟶ Y) (sq : CommSq u f z v), sq.HasLift
⊢ StrongEpi f

Tactic:
{ epi := inferInstance
    llp := fun {X Y} z hz => ⟨fun {u v} sq => hf X Y z hz u v sq⟩ }

Premises used: CategoryTheory.StrongEpi.mk, inferInstance, CategoryTheory.HasLiftingProperty.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst_1 : StrongEpi f
⊢ Epi f

Tactic:
StrongEpi.epi

Premises used: CategoryTheory.StrongEpi.epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst_1 : StrongMono f
⊢ Mono f

Tactic:
StrongMono.mono

Premises used: CategoryTheory.StrongMono.mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi f
inst_2 : StrongEpi g
X Y : C
z : X ⟶ Y
inst_3 : Mono z
⊢ HasLiftingProperty (f ≫ g) z

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono f
inst_2 : StrongMono g
X Y : C
z : X ⟶ Y
inst_3 : Epi z
⊢ HasLiftingProperty z (f ≫ g)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
h : Mono z
sq_hasLift : ∀ {f : Q ⟶ X} {g_1 : R ⟶ Y} (sq : CommSq f g z g_1), sq.HasLift
⊢ HasLiftingProperty g z

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
h : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ (f ≫ u) ≫ z = (f ≫ g) ≫ v

Tactic:
simp only [Category.assoc, sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
h : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ (f ≫ u) ≫ z = (f ≫ g) ≫ v

Tactic:
have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
h : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ g ≫ ⋯.lift = u

Tactic:
simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CommSq.fac_right, CategoryTheory.cancel_mono, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
h : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ ⋯.lift ≫ z = v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
h : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ sq.HasLift

Tactic:
exact
        CommSq.HasLift.mk'
          ⟨(CommSq.mk h₀).lift, by
            simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩

Premises used: CategoryTheory.CommSq.HasLift.mk', CategoryTheory.CommSq.lift, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.LiftStruct.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
sq_hasLift : ∀ {f_1 : X ⟶ P} {g : Y ⟶ Q} (sq : CommSq f_1 z f g), sq.HasLift
⊢ HasLiftingProperty z f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
rw : (u ≫ f) ≫ g = z ≫ v ≫ g
rw₁ : (z ≫ v) ≫ g = z ≫ v ≫ g
rw₂ rw₃ : z ≫ v ≫ g = z ≫ v ≫ g
⊢ u ≫ f ≫ g = z ≫ v ≫ g

Tactic:
rw [← Category.assoc, eq_whisker sq.w, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
⊢ u ≫ f ≫ g = z ≫ v ≫ g

Tactic:
have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by
        rw [← Category.assoc, eq_whisker sq.w, Category.assoc]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ z ≫ ⋯.lift = u

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ ⋯.lift ≫ f = v

Tactic:
simp [← cancel_epi z, sq.w]

Premises used: CategoryTheory.CommSq.w, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : StrongMono (f ≫ g)
X Y : C
z : X ⟶ Y
inst_2 : Epi z
u : X ⟶ P
v : Y ⟶ Q
sq : CommSq u z f v
h₀ : u ≫ f ≫ g = z ≫ v ≫ g
⊢ sq.HasLift

Tactic:
exact CommSq.HasLift.mk' ⟨(CommSq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩

Premises used: CategoryTheory.CommSq.HasLift.mk', CategoryTheory.CommSq.lift, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.LiftStruct.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : IsIso f
⊢ Epi f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_1 : IsIso f
⊢ Mono f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
rw : Epi (Arrow.Hom.left e.inv ≫ f ≫ Arrow.Hom.right e.hom)
⊢ Epi g

Tactic:
rw [Arrow.iso_w' e]

Premises used: CategoryTheory.Arrow.iso_w'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi (Arrow.Hom.left e.inv ≫ f ≫ Arrow.Hom.right e.hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
X Y : C
z : X ⟶ Y
inst_1 : Mono z
⊢ HasLiftingProperty g z

Tactic:
apply HasLiftingProperty.of_arrow_iso_left e z

Premises used: CategoryTheory.HasLiftingProperty.of_arrow_iso_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
rw : Mono (Arrow.Hom.left e.inv ≫ f ≫ Arrow.Hom.right e.hom)
⊢ Mono g

Tactic:
rw [Arrow.iso_w' e]

Premises used: CategoryTheory.Arrow.iso_w'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono (Arrow.Hom.left e.inv ≫ f ≫ Arrow.Hom.right e.hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
inst_1 : Epi z
⊢ HasLiftingProperty z g

Tactic:
apply HasLiftingProperty.of_arrow_iso_right z e

Premises used: CategoryTheory.HasLiftingProperty.of_arrow_iso_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
mp : StrongEpi f → StrongEpi g
mpr : StrongEpi g → StrongEpi f
⊢ StrongEpi f ↔ StrongEpi g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ StrongEpi g

Tactic:
StrongEpi.of_arrow_iso e

Premises used: CategoryTheory.StrongEpi.of_arrow_iso