awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
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 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
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 ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ = e a
have rw : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π)
Tactic: rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e),
      Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦
      effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
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 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
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 : α
rw : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π)
⊢ π a ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ = e a
have rw₁ : CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
    EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) sorry =
  e a
Tactic: rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e),
      Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦
      effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
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 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
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 : α
rw : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π)
rw₁ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
      EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ =
    e a
⊢ π a ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ = e a
have rw₂ : CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
    EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) sorry =
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
Tactic: rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e),
      Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦
      effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
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 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
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 : α
rw : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π)
rw₁ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
      EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ =
    e a
rw₂ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
      EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
⊢ π a ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ = e a
have rw₃ : CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a)
    (Sigma.desc π ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) sorry) =
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
Tactic: rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e),
      Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦
      effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
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 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
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 : α
rw : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π)
rw₁ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
      EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ =
    e a
rw₂ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π) ≫
      EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
rw₃ :
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a)
      (Sigma.desc π ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯) =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
⊢ π a ≫ EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc e) ⋯ = e a
have rw₄ : CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e) =
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
Tactic: rw [(by simp : π a = Sigma.ι X a ≫ Sigma.desc π), (by simp : e a = Sigma.ι X a ≫ Sigma.desc e),
      Category.assoc, EffectiveEpi.fac (Sigma.desc π) (Sigma.desc e) (fun g₁ g₂ hg ↦
      effectiveEpiFamilyStructOfEffectiveEpiDesc_aux h hg)]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
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 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
W : C
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), π a ≫ x_1 = x a
⊢ x_1 = EffectiveEpi.desc (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π) (Sigma.desc x) ⋯
have hm₁ : Eq (α := sigmaObj.{u_2, v_1, u_1} X ⟶ W) (Sigma.desc π ≫ x_1) (Sigma.desc x)
Tactic: apply EffectiveEpi.uniq (Sigma.desc π)
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
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 : EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
inst_3 : ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X) (a : α), HasPullback g (Sigma.ι X a)
inst_4 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    HasCoproduct.{u_2, v_1, u_1} (C := C) fun (a : α) ↦ pullback g (Sigma.ι X a)
inst_5 :
  ∀ {Z : C} (g : Z ⟶ sigmaObj.{u_2, v_1, u_1} X),
    Epi.{v_1, u_1} (C := C) (X := sigmaObj.{u_2, v_1, u_1} fun (a : α) ↦ pullback g (Sigma.ι X a)) (Y := Z)
      (Sigma.desc fun (a : α) ↦ pullback.fst g (Sigma.ι X a))
W : C
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
x_1 : B ⟶ W
hm : ∀ (a : α), π a ≫ x_1 = x a
⊢ Eq (α := sigmaObj.{u_2, v_1, u_1} X ⟶ W) (Sigma.desc π ≫ x_1) (Sigma.desc x)
have hm₁ : ∀ (b : α),
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X b) (Sigma.desc π ≫ x_1) =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X b) (Sigma.desc x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Extensive (goal)
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.ReflectsEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
⊢ EffectiveEpiFamily X π
have simp : EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)
Tactic: simp only [← effectiveEpi_desc_iff_effectiveEpiFamily]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Extensive (goal)
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.ReflectsEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
⊢ EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)
have h₁ : EffectiveEpi (Y := F.obj (sigmaObj.{0, v_1, u_1} X)) (F.map (Sigma.desc π))
Tactic: apply F.effectiveEpi_of_map
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Extensive (goal)
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.ReflectsEffectiveEpis
α : Type
h_1 : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
⊢ EffectiveEpi (Y := F.obj (sigmaObj.{0, v_1, u_1} X)) (F.map (Sigma.desc π))
have h₁ : Eq (α := F.obj (sigmaObj.{0, v_1, u_1} X) ⟶ F.obj B) (F.map (Sigma.desc π))
  (CategoryStruct.comp (Y := sigmaObj.{0, v_2, u_2} fun (b : α) ↦ F.obj (X b)) (inv (sigmaComparison F X))
    (Sigma.desc fun (a : α) ↦ F.map (π a)))
Tactic: convert!
      (inferInstance :
        EffectiveEpi (inv (sigmaComparison F X) ≫ (Sigma.desc (fun a ↦ F.map (π a)))))
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Extensive (goal)
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 π
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj B) (fun (a : α) ↦ F.obj (X a)) fun (a : α) ↦ F.map (π a)
have simp : 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: simp only [← effectiveEpi_desc_iff_effectiveEpiFamily]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Extensive (goal)
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 π
⊢ 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))
have 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 π)))
Tactic: convert! (inferInstance : EffectiveEpi ((sigmaComparison F X) ≫ (F.map (Sigma.desc π))))
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
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₂
⊢ 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₂)
have 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₂
Tactic: have := h a₁ a₂ (e.functor.map g₁) (e.functor.map g₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
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₂
⊢ 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₂)
have this₁ : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
Tactic: simp only [← Functor.map_comp, hg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
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 : α
⊢ 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
have simp : e.functor.map (π a) ≫
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) sorry) ≫
      e.counit.app W =
  ε a
Tactic: simp only [Functor.comp_obj, Adjunction.homEquiv_counit,
      Equivalence.toAdjunction_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
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 : α
⊢ 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
have 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)) sorry))
  (((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)
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
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 =
    ε a
have this₁ : e.functor.map (π a) ≫
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) sorry) ≫
      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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (goal)
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 =
    ((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)) ⋯)
have simp : m =
  e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) sorry) ≫ e.counit.app W
Tactic: simp only [Functor.comp_obj, Adjunction.homEquiv_counit,
      Equivalence.toAdjunction_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Preserves (hypothesis)
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 =
    e.functor.map (EffectiveEpiFamily.desc X π (fun (a : α) ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫
      e.counit.app W
have 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)) sorry
Tactic: have := EffectiveEpiFamily.uniq X π (fun a ↦ e.unit.app _ ≫ e.inverse.map (ε a))
      (effectiveEpiFamilyStructOfEquivalence_aux e X π ε h)