awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.PreservesEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
h₁ :
  Eq (α := (sigmaObj.{0, v_2, u_2} fun (a : α) ↦ F.obj (X a)) ⟶ F.obj B) (Sigma.desc fun (a : α) ↦ F.map (π a))
    (CategoryStruct.comp (Y := F.obj (sigmaObj.{0, v_1, u_1} X)) (sigmaComparison F X) (F.map (Sigma.desc π)))
⊢ EffectiveEpi.{v_2, u_2} (C := D) (X := F.obj B) (Y := sigmaObj.{0, v_2, u_2} fun (a : α) ↦ F.obj (X a))
    (Sigma.desc fun (a : α) ↦ F.map (π a))

Tactic:
convert! (inferInstance : EffectiveEpi ((sigmaComparison F X) ≫ (F.map (Sigma.desc π))))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : FinitaryPreExtensive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : PreservesFiniteCoproducts F
inst_5 : F.PreservesEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
⊢ Eq (α := (sigmaObj.{0, v_2, u_2} fun (a : α) ↦ F.obj (X a)) ⟶ F.obj B) (Sigma.desc fun (a : α) ↦ F.map (π a))
    (CategoryStruct.comp (Y := F.obj (sigmaObj.{0, v_1, u_1} X)) (sigmaComparison F X) (F.map (Sigma.desc π)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ e.functor.map g₁ ≫ e.functor.map (π a₁) = e.functor.map g₂ ≫ e.functor.map (π a₂) →
    e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂

Tactic:
have := h a₁ a₂ (e.functor.map g₁) (e.functor.map g₂)
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
this :
  e.functor.map g₁ ≫ e.functor.map (π a₁) = e.functor.map g₂ ≫ e.functor.map (π a₂) →
    e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
⊢ True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂

Tactic:
simp only [← Functor.map_comp, hg] at this

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
this : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
⊢ True

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
this : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
⊢ Eq (α := Z ⟶ e.inverse.obj W) (g₁ ≫ (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₁)
    (g₂ ≫ (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₂)

Tactic:
simpa using congrArg e.inverse.map (this (by trivial))

Premises used: congrArg, CategoryTheory.Functor.map, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
a : α
simp :
  e.functor.map (π a) ≫
      e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
        e.counit.app W =
    ε a
⊢ e.functor.map (π a) ≫
      ((e.toAdjunction.homEquiv B W).symm : (a : B ⟶ e.inverse.obj W) → e.functor.obj B ⟶ W)
        (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) =
    ε a

Tactic:
simp only [Functor.comp_obj, Adjunction.homEquiv_counit,
      Equivalence.toAdjunction_counit]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Equivalence.toAdjunction_counit, CategoryTheory.Adjunction.homEquiv_counit
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
a : α
⊢ Eq (α := e.functor.obj (X a) ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) W)
    (((fun (f : e.functor.obj (X a) ⟶ (e.inverse ⋙ e.functor).obj W) ↦ f ≫ e.counit.app W) ∘ e.functor.map)
      (π a ≫ EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯))
    (((fun (f : e.functor.obj (X a) ⟶ (e.inverse ⋙ e.functor).obj W) ↦ f ≫ e.counit.app W) ∘ e.functor.map)
      (e.unit.app (X a) ≫ e.inverse.map (ε a)))

Tactic:
have := congrArg ((fun f ↦ f ≫ e.counit.app _) ∘ e.functor.map)
      (EffectiveEpiFamily.fac X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
      (effectiveEpiFamilyStructOfEquivalence_aux e X π ε h) a)
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
a : α
this :
  Eq (α := e.functor.obj (X a) ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D) W)
    (((fun (f : e.functor.obj (X a) ⟶ (e.inverse ⋙ e.functor).obj W) ↦ f ≫ e.counit.app W) ∘ e.functor.map)
      (π a ≫ EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯))
    (((fun (f : e.functor.obj (X a) ⟶ (e.inverse ⋙ e.functor).obj W) ↦ f ≫ e.counit.app W) ∘ e.functor.map)
      (e.unit.app (X a) ≫ e.inverse.map (ε a)))
⊢ e.functor.map (π a) ≫
      e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
        e.counit.app W =
    e.functor.map (e.unit.app (X a)) ≫ e.counit.app (e.functor.obj (X a)) ≫ ε a

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, Function.comp_apply, Functor.map_comp,
        Category.assoc, Equivalence.fun_inv_map, Iso.inv_hom_id_app, Category.comp_id] at this

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Equivalence.fun_inv_map, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, Function.comp_apply, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
a : α
this :
  e.functor.map (π a) ≫
      e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
        e.counit.app W =
    e.functor.map (e.unit.app (X a)) ≫ e.counit.app (e.functor.obj (X a)) ≫ ε a
⊢ e.functor.map (π a) ≫
      e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
        e.counit.app W =
    ε a

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
simp :
  m =
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
      e.counit.app W
⊢ m =
    ((e.toAdjunction.homEquiv B W).symm : (a : B ⟶ e.inverse.obj W) → e.functor.obj B ⟶ W)
      (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯)

Tactic:
simp only [Functor.comp_obj, Adjunction.homEquiv_counit,
      Equivalence.toAdjunction_counit]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Equivalence.toAdjunction_counit, CategoryTheory.Adjunction.homEquiv_counit
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
⊢ ∀ (m : B ⟶ e.inverse.obj W) (hm : ∀ (a : α), π a ≫ m = e.unit.app (X a) ≫ e.inverse.map (ε a)),
    m = EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯

Tactic:
have := EffectiveEpiFamily.uniq X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
      (effectiveEpiFamilyStructOfEquivalence_aux e X π ε h)
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this :
  ∀ (m : B ⟶ e.inverse.obj W) (hm : ∀ (a : α), π a ≫ m = e.unit.app (X a) ≫ e.inverse.map (ε a)),
    m = EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
specialize : ∀ (a : α), π a ≫ e.unit.app B ≫ e.inverse.map m = e.unit.app (X a) ≫ e.inverse.map (ε a)
specialize₁ :
  ∀
    (this :
      e.unit.app B ≫ e.inverse.map m =
        EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯),
    m =
      e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
        e.counit.app W
⊢ m =
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
      e.counit.app W

Tactic:
specialize this (e.unit.app _ ≫ e.inverse.map m) fun a ↦ ?_

Premises used: CategoryTheory.Equivalence.unit, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.app, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this :
  ∀ (m : B ⟶ e.inverse.obj W) (hm : ∀ (a : α), π a ≫ m = e.unit.app (X a) ≫ e.inverse.map (ε a)),
    m = EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
a : α
rw : π a ≫ e.unit.app B ≫ e.inverse.map m = e.unit.app (X a) ≫ e.inverse.map (e.functor.map (π a) ≫ m)
⊢ π a ≫ e.unit.app B ≫ e.inverse.map m = e.unit.app (X a) ≫ e.inverse.map (ε a)

Tactic:
rw [← congrArg e.inverse.map (hm a)]

Premises used: congrArg, CategoryTheory.Functor.map, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this :
  ∀ (m : B ⟶ e.inverse.obj W) (hm : ∀ (a : α), π a ≫ m = e.unit.app (X a) ≫ e.inverse.map (ε a)),
    m = EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
a : α
⊢ π a ≫ e.unit.app B ≫ e.inverse.map m = e.unit.app (X a) ≫ e.inverse.map (e.functor.map (π a) ≫ m)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this :
  e.unit.app B ≫ e.inverse.map m = EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
⊢ m =
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
      e.counit.app W

Tactic:
simp [← this]
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst_2 : EffectiveEpiFamily X π
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.IsEquivalence
⊢ EffectiveEpiFamily.{v_2, u_2, u_3} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)

Tactic:
⟨⟨effectiveEpiFamilyStructOfEquivalence F.asEquivalence _ _⟩⟩

Premises used: CategoryTheory.effectiveEpiFamilyStructOfEquivalence, CategoryTheory.Functor.asEquivalence, Nonempty.intro, CategoryTheory.EffectiveEpiFamily.mk
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
e : Equivalence.{v_1, v_2, u_1, u_2} C D
B_1 : C
α : Type u_3
X_1 : α → C
π_1 : (a : α) → X_1 a ⟶ B_1
inst_2 : EffectiveEpiFamily X_1 π_1
X B : C
π : X ⟶ B
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.IsEquivalence
inst_4 : EffectiveEpi π
⊢ EffectiveEpi (F.map π)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpis
X Y : C
f : X ⟶ Y
inst_3 : EffectiveEpi f
⊢ EffectiveEpi (F.map f)

Tactic:
PreservesEffectiveEpis.preserves f

Premises used: CategoryTheory.Functor.PreservesEffectiveEpis.preserves
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : IsRegularEpiCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.PreservesEpimorphisms
inst_4 : HasPullbacks.{v_2, u_2} D
X Y : C
x : X ⟶ Y
h : EffectiveEpi x
rw : IsRegularEpi (F.map x)
⊢ EffectiveEpi (F.map x)

Tactic:
rw [← isRegularEpi_iff_effectiveEpi]

Premises used: CategoryTheory.isRegularEpi_iff_effectiveEpi
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : IsRegularEpiCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.PreservesEpimorphisms
inst_4 : HasPullbacks.{v_2, u_2} D
X Y : C
x : X ⟶ Y
h : EffectiveEpi x
⊢ IsRegularEpi (F.map x)

Tactic:
apply IsRegularEpiCategory.regularEpiOfEpi

Premises used: CategoryTheory.IsRegularEpiCategory.regularEpiOfEpi
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
rw : F.map (c.snd ≫ f) = F.map c.snd ≫ F.map f
⊢ F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f

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

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ F.map (c.snd ≫ f) = F.map c.snd ≫ F.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
refine_1 : F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f
refine_2 : IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)
⊢ IsColimit (Cofork.ofπ (F.map f) ⋯)

Tactic:
refine isColimitCoforkOfEffectiveEpi (F.map f) (.mk (F.map c.fst) (F.map c.snd) ?_) ?_

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.isColimitCoforkOfEffectiveEpi, CategoryTheory.Functor.map, CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f

Tactic:
simp [← Functor.map_comp, c.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
refine_2 : cospan f f ⋙ F ≅ cospan (F.map f) (F.map f)
refine_2₁ :
  (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
              (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left)) (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right))
              ⋯ ⋯).hom).obj
      (F.mapCone c) ≅
    PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯
⊢ IsLimit (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯)

Tactic:
refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (isLimitOfPreserves F hc)

Premises used: DFunLike.coe, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ cospan f f ⋙ F ≅ cospan (F.map f) (F.map f)

Tactic:
exact cospanIsoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.cospanIsoMk
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
D_1 : Type u_2
inst_1 : Category.{v_2, u_2} D_1
C : Type u_3
D : Type u_4
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst_4 : EffectiveEpi f
F : Functor.{v_3, v_4, u_3, u_4} C D
inst_5 : F.PreservesEffectiveEpis
inst_6 : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
              (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left)) (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right))
              ⋯ ⋯).hom).obj
      (F.mapCone c) ≅
    PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯

Tactic:
exact Cone.ext (Iso.refl _) <| by rintro (_ | _ | _) <;> cat_disch

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesEffectiveEpiFamilies
α : Type u
B : C
X : α → C
π : (a : α) → X a ⟶ B
inst_3 : EffectiveEpiFamily X π
⊢ EffectiveEpiFamily.{v_2, u_2, u} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)

Tactic:
PreservesEffectiveEpiFamilies.preserves X π

Premises used: CategoryTheory.Functor.PreservesEffectiveEpiFamilies.preserves