awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
⊢ ∀ (i : I), Mono ((F i).map S.f)

Tactic:
fun i ↦ (hS i).mono_f

Premises used: CategoryTheory.ShortComplex.ShortExact.mono_f
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
⊢ ∀ (i : I), Mono ((F i).map S.f)

Tactic:
exact fun i ↦ (hS i).mono_f

Premises used: CategoryTheory.ShortComplex.ShortExact.mono_f
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
⊢ Mono S.f

Tactic:
have : Mono S.f := by
      rw [hP.jointlyReflectMonomorphisms.mono_iff]
      exact fun i ↦ (hS i).mono_f
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
this : Mono S.f
rw : ∀ (i : I), Epi ((F i).map S.g)
⊢ Epi S.g

Tactic:
rw [hP.jointlyReflectEpimorphisms.epi_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectEpimorphisms, CategoryTheory.JointlyReflectEpimorphisms.epi_iff
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
this : Mono S.f
⊢ ∀ (i : I), Epi ((F i).map S.g)

Tactic:
fun i ↦ (hS i).epi_g

Premises used: CategoryTheory.ShortComplex.ShortExact.epi_g
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
this : Mono S.f
⊢ ∀ (i : I), Epi ((F i).map S.g)

Tactic:
exact fun i ↦ (hS i).epi_g

Premises used: CategoryTheory.ShortComplex.ShortExact.epi_g
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
this : Mono S.f
⊢ Epi S.g

Tactic:
have : Epi S.g := by
      rw [hP.jointlyReflectEpimorphisms.epi_iff]
      exact fun i ↦ (hS i).epi_g
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
this_1 : Mono S.f
this : Epi S.g
⊢ S.ShortExact

Tactic:
{ exact := (hP.exact_iff S).2 (fun i ↦ (hS i).exact) }

Premises used: Iff.mpr, CategoryTheory.ShortComplex.ShortExact.exact, CategoryTheory.JointlyReflectIsomorphisms.exact_iff, CategoryTheory.ShortComplex.ShortExact.mk
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
this_1 : Mono S.f
this : Epi S.g
⊢ S.ShortExact

Tactic:
exact { exact := (hP.exact_iff S).2 (fun i ↦ (hS i).exact) }
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
⊢ ShortComplex.QuasiIso f ↔
    ∀ (i : I), ShortComplex.QuasiIso (S₁ := Functor.obj (F i).mapShortComplex S₁) (Functor.map (F i).mapShortComplex f)

Tactic:
⟨fun hf i ↦ inferInstance, fun hf ↦ ?_⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
refine :
  ∀
    (hf :
      ∀ (i : I),
        ShortComplex.QuasiIso (S₁ := Functor.obj (F i).mapShortComplex S₁) (Functor.map (F i).mapShortComplex f)),
    ShortComplex.QuasiIso f
⊢ ShortComplex.QuasiIso f ↔
    ∀ (i : I), ShortComplex.QuasiIso (S₁ := Functor.obj (F i).mapShortComplex S₁) (Functor.map (F i).mapShortComplex f)

Tactic:
refine ⟨fun hf i ↦ inferInstance, fun hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
hf : ∀ (i : I), ShortComplex.QuasiIso (S₁ := Functor.obj (F i).mapShortComplex S₁) (Functor.map (F i).mapShortComplex f)
simp :
  ∀
    (hf :
      ∀ (i : I),
        IsIso (X := ShortComplex.homology (Functor.obj (F i).mapShortComplex S₁)) (Y :=
          ShortComplex.homology (Functor.obj (F i).mapShortComplex S₂))
          (ShortComplex.homologyMap (Functor.map (F i).mapShortComplex f))),
    IsIso (X := S₁.homology) (Y := S₂.homology) (ShortComplex.homologyMap f)
⊢ ShortComplex.QuasiIso f

Tactic:
simp only [ShortComplex.quasiIso_iff] at hf ⊢

Premises used: CategoryTheory.ShortComplex.quasiIso_iff
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
hf :
  ∀ (i : I),
    IsIso (X := ShortComplex.homology (Functor.obj (F i).mapShortComplex S₁)) (Y :=
      ShortComplex.homology (Functor.obj (F i).mapShortComplex S₂))
      (ShortComplex.homologyMap (Functor.map (F i).mapShortComplex f))
rw : ∀ (i : I), IsIso (X := (F i).obj S₁.homology) (Y := (F i).obj S₂.homology) ((F i).map (ShortComplex.homologyMap f))
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (ShortComplex.homologyMap f)

Tactic:
rw [hP.isIso_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.isIso_iff
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
hf :
  ∀ (i : I),
    IsIso (X := ShortComplex.homology (Functor.obj (F i).mapShortComplex S₁)) (Y :=
      ShortComplex.homology (Functor.obj (F i).mapShortComplex S₂))
      (ShortComplex.homologyMap (Functor.map (F i).mapShortComplex f))
⊢ ∀ (i : I), IsIso (X := (F i).obj S₁.homology) (Y := (F i).obj S₂.homology) ((F i).map (ShortComplex.homologyMap f))

Tactic:
fun i ↦ ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso (ShortComplex.homologyFunctorIso (F i))).app
      (Arrow.mk f))).1 (hf i)

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.ShortComplex.homology, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.homologyFunctorIso, Iff.mp, CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex.{v_1, u_1} C
f : S₁ ⟶ S₂
hf :
  ∀ (i : I),
    IsIso (X := ShortComplex.homology (Functor.obj (F i).mapShortComplex S₁)) (Y :=
      ShortComplex.homology (Functor.obj (F i).mapShortComplex S₂))
      (ShortComplex.homologyMap (Functor.map (F i).mapShortComplex f))
⊢ ∀ (i : I), IsIso (X := (F i).obj S₁.homology) (Y := (F i).obj S₂.homology) ((F i).map (ShortComplex.homologyMap f))

Tactic:
exact fun i ↦ ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
    (((Functor.mapArrowFunctor _ _).mapIso (ShortComplex.homologyFunctorIso (F i))).app
      (Arrow.mk f))).1 (hf i)

Premises used: CategoryTheory.ShortComplex, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.ShortComplex.homologyFunctorIso, Iff.mp, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
α : Type u_4
c : ComplexShape α
K L : HomologicalComplex.{v_1, u_1, u_4} C c
f : K ⟶ L
a : α
⊢ QuasiIsoAt f a ↔
    ∀ (i : I),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f) a

Tactic:
simpa only [quasiIsoAt_iff' _ _ _ _ rfl rfl] using
    hP.shortComplexQuasiIso_iff _

Premises used: CategoryTheory.JointlyReflectIsomorphisms.shortComplexQuasiIso_iff, quasiIsoAt_iff', rfl
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
α : Type u_4
c : ComplexShape α
K L : HomologicalComplex.{v_1, u_1, u_4} C c
f : K ⟶ L
simp :
  (∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i) ↔
    ∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1
⊢ QuasiIso f ↔
    ∀ (i : I),
      QuasiIso (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)

Tactic:
simp only [_root_.quasiIso_iff, hP.quasiIsoAt_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.quasiIsoAt_iff, quasiIso_iff
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
inst_2 : HasEqualizers.{u_4, u_1} C
inst_3 : ∀ (i : I), PreservesLimitsOfShape WalkingParallelPair (F i)
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [Mono f], (∀ (i : I), IsIso ((F i).map f)) → IsIso f
X Y : C
f g : X ⟶ Y
hfg : ∀ (i : I), (F i).map f = (F i).map g
i : I
hc : IsLimit (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) ⋯) :=
  isLimitForkMapOfIsLimit (F i) ⋯ (equalizerIsEqualizer f g)
⊢ 𝟙 ((F i).obj X) ≫ (F i).map f = 𝟙 ((F i).obj X) ≫ (F i).map g

Tactic:
simpa using hfg i
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
inst_2 : HasEqualizers.{u_4, u_1} C
inst_3 : ∀ (i : I), PreservesLimitsOfShape WalkingParallelPair (F i)
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [Mono f], (∀ (i : I), IsIso ((F i).map f)) → IsIso f
X Y : C
f g : X ⟶ Y
hfg : ∀ (i : I), (F i).map f = (F i).map g
i : I
hc : IsLimit (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) ⋯) :=
  isLimitForkMapOfIsLimit (F i) ⋯ (equalizerIsEqualizer f g)
obtain :
  ∀ (l : (F i).obj X ⟶ (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) ⋯).pt)
    (hl : l ≫ (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) ⋯).ι = 𝟙 ((F i).obj X)),
    IsIso (X := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g))
⊢ IsIso (X := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g))

Tactic:
obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hc (𝟙 _) (by simpa using hfg i)

Premises used: CategoryTheory.Limits.Fork.IsLimit.lift', CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
inst_2 : HasEqualizers.{u_4, u_1} C
inst_3 : ∀ (i : I), PreservesLimitsOfShape WalkingParallelPair (F i)
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [Mono f], (∀ (i : I), IsIso ((F i).map f)) → IsIso f
X Y : C
f g : X ⟶ Y
hfg : ∀ (i : I), (F i).map f = (F i).map g
i : I
hc : IsLimit (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) ⋯) :=
  isLimitForkMapOfIsLimit (F i) ⋯ (equalizerIsEqualizer f g)
l : (F i).obj X ⟶ (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) ⋯).pt
hl : l ≫ (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) ⋯).ι = 𝟙 ((F i).obj X)
⊢ IsIso (X := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g))

Tactic:
exact ⟨l, Fork.IsLimit.hom_ext hc (by cat_disch), by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (i : I), IsIso ((F i).map f)

Tactic:
⟨fun _ _ ↦ inferInstance, fun _ ↦ h.isIso f⟩

Premises used: inferInstance, CategoryTheory.JointlyReflectIsomorphisms.isIso, Iff.intro
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Mono ((F i).map f)
inst_2 : ∀ (i : I), PreservesLimit (cospan f f) (F i)
inst_3 : HasPullback f f
have : ∀ (hc : IsLimit (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) ⋯)), Mono f
⊢ Mono f

Tactic:
have hc := pullbackIsPullback f f
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Mono ((F i).map f)
inst_2 : ∀ (i : I), PreservesLimit (cospan f f) (F i)
inst_3 : HasPullback f f
hc : IsLimit (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) ⋯)
rw : ∀ (i : I), IsIso ((F i).map (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) ⋯).fst)
⊢ Mono f

Tactic:
rw [mono_iff_isIso_fst hc, h.isIso_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.isIso_iff, CategoryTheory.mono_iff_isIso_fst
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Mono ((F i).map f)
inst_2 : ∀ (i : I), PreservesLimit (cospan f f) (F i)
inst_3 : HasPullback f f
hc : IsLimit (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) ⋯)
i : I
⊢ IsIso ((F i).map (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) ⋯).fst)

Tactic:
(mono_iff_isIso_fst ((isLimitMapConePullbackConeEquiv (F i) pullback.condition).1
    (isLimitOfPreserves (F i) hc))).1 (hf i)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.toFun, CategoryTheory.Limits.limit, Iff.mp, CategoryTheory.Limits.pullback.condition, CategoryTheory.mono_iff_isIso_fst, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Mono ((F i).map f)
inst_2 : ∀ (i : I), PreservesLimit (cospan f f) (F i)
inst_3 : HasPullback f f
hc : IsLimit (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) ⋯)
i : I
⊢ IsIso ((F i).map (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) ⋯).fst)

Tactic:
exact (mono_iff_isIso_fst ((isLimitMapConePullbackConeEquiv (F i) pullback.condition).1
    (isLimitOfPreserves (F i) hc))).1 (hf i)

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.toFun, Iff.mp, CategoryTheory.Limits.pullback.condition, CategoryTheory.mono_iff_isIso_fst, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Epi ((F i).map f)
inst_2 : ∀ (i : I), PreservesColimit (span f f) (F i)
inst_3 : HasPushout f f
have : ∀ (hc : IsColimit (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) ⋯)), Epi f
⊢ Epi f

Tactic:
have hc := pushoutIsPushout f f
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Epi ((F i).map f)
inst_2 : ∀ (i : I), PreservesColimit (span f f) (F i)
inst_3 : HasPushout f f
hc : IsColimit (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) ⋯)
rw : ∀ (i : I), IsIso ((F i).map (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) ⋯).inl)
⊢ Epi f

Tactic:
rw [epi_iff_isIso_inl hc, h.isIso_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.isIso_iff, CategoryTheory.epi_iff_isIso_inl