awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
A B : C
f : A ⟶ B
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : IsIso (F.map f)
inst_3 : F.ReflectsIsomorphisms
⊢ IsIso f

Tactic:
ReflectsIsomorphisms.reflects F f

Premises used: CategoryTheory.Functor.ReflectsIsomorphisms.reflects
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
A B : C
f : A ⟶ B
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.ReflectsIsomorphisms
⊢ IsIso (F.map f) ↔ IsIso f

Tactic:
⟨fun _ => isIso_of_reflects_iso f F, fun _ => inferInstance⟩

Premises used: CategoryTheory.isIso_of_reflects_iso, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : F.Full
inst_4 : F.Faithful
⊢ F.ReflectsIsomorphisms

Tactic:
(Functor.FullyFaithful.ofFullyFaithful F).reflectsIsomorphisms

Premises used: CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
inst_4 : G.ReflectsIsomorphisms
A B : C
f : A ⟶ B
hf : IsIso (G.map (F.map f))
⊢ IsIso (F.map f)

Tactic:
haveI := isIso_of_reflects_iso (F.map f) G
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
inst_4 : G.ReflectsIsomorphisms
A B : C
f : A ⟶ B
hf : IsIso (G.map (F.map f))
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
isIso_of_reflects_iso f F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
inst_4 : G.ReflectsIsomorphisms
A B : C
f : A ⟶ B
hf : IsIso (G.map (F.map f))
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
exact isIso_of_reflects_iso f F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : (F ⋙ G).ReflectsIsomorphisms
A B : C
f : A ⟶ B
h : IsIso (F.map f)
rw : IsIso ((F ⋙ G).map f)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (F ⋙ G)]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.isIso_iff_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : (F ⋙ G).ReflectsIsomorphisms
A B : C
f : A ⟶ B
h : IsIso (F.map f)
dsimp : IsIso (G.map (F.map f))
⊢ IsIso ((F ⋙ G).map f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : (F ⋙ G).ReflectsIsomorphisms
A B : C
f : A ⟶ B
h : IsIso (F.map f)
⊢ IsIso (G.map (F.map f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
h : IsIso (X := obj (obj (whiskeringRight C D E) F) X) (map (obj (whiskeringRight C D E) F) f)
rw : ∀ (X_1 : C), IsIso (f.app X_1)
⊢ IsIso f

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
h : IsIso (X := obj (obj (whiskeringRight C D E) F) X) (map (obj (whiskeringRight C D E) F) f)
Z : C
rw : IsIso (F.map (f.app Z))
⊢ IsIso (f.app Z)

Tactic:
rw [← isIso_iff_of_reflects_iso _ F]

Premises used: CategoryTheory.isIso_iff_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
h : IsIso (X := obj (obj (whiskeringRight C D E) F) X) (map (obj (whiskeringRight C D E) F) f)
Z : C
change :
  IsIso (X := (obj (obj (whiskeringRight C D E) F) X).obj Z) (NatTrans.app (map (obj (whiskeringRight C D E) F) f) Z)
⊢ IsIso (F.map (f.app Z))

Tactic:
change IsIso ((((whiskeringRight C D E).obj F).map f).app Z)

Premises used: CategoryTheory.IsIso, CategoryTheory.Functor.map, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.ReflectsIsomorphisms
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
h : IsIso (X := obj (obj (whiskeringRight C D E) F) X) (map (obj (whiskeringRight C D E) F) f)
Z : C
⊢ IsIso (X := (obj (obj (whiskeringRight C D E) F) X).obj Z) (NatTrans.app (map (obj (whiskeringRight C D E) F) f) Z)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 G : Functor.{v_1, v_2, u_1, u_2} C D
α : F ≅ G
inst_2 : F.ReflectsIsomorphisms
A B : C
f : A ⟶ B
h : IsIso (G.map f)
rw : IsIso (α.hom.app A ≫ G.map f ≫ α.inv.app B)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ F, ← NatIso.naturality_2 α f]

Premises used: CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.NatIso.naturality_2
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 G : Functor.{v_1, v_2, u_1, u_2} C D
α : F ≅ G
inst_2 : F.ReflectsIsomorphisms
A B : C
f : A ⟶ B
h : IsIso (G.map f)
⊢ IsIso (α.hom.app A ≫ G.map f ≫ α.inv.app B)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
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 G : Functor.{v_1, v_2, u_1, u_2} C D
α : F ≅ G
⊢ F.ReflectsIsomorphisms ↔ G.ReflectsIsomorphisms

Tactic:
⟨fun _ => reflectsIsomorphisms_of_iso α,
  fun _ => reflectsIsomorphisms_of_iso α.symm⟩

Premises used: CategoryTheory.reflectsIsomorphisms_of_iso, Iff.intro, CategoryTheory.Iso.symm
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
⊢ IsZero.{v_1, u_1} X ↔ ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)

Tactic:
⟨fun hX _ ↦ Functor.map_isZero _ hX, fun hX ↦ ?_⟩

Premises used: CategoryTheory.Functor.map_isZero, 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
refine : ∀ (hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)), IsZero.{v_1, u_1} X
⊢ IsZero.{v_1, u_1} X ↔ ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)

Tactic:
refine ⟨fun hX _ ↦ Functor.map_isZero _ hX, fun hX ↦ ?_⟩
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
φ : 0 ⟶ X := 0
rw : ∀ (i : I), IsIso ((F i).map φ)
⊢ IsIso φ

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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
φ : 0 ⟶ X := 0
⊢ ∀ (i : I), IsIso ((F i).map φ)

Tactic:
fun i ↦ (Functor.map_isZero _ (isZero_zero _)).isIso (hX i) _

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Functor.map_isZero, CategoryTheory.Functor.map, CategoryTheory.Limits.IsZero.isIso
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
φ : 0 ⟶ X := 0
⊢ ∀ (i : I), IsIso ((F i).map φ)

Tactic:
exact fun i ↦ (Functor.map_isZero _ (isZero_zero _)).isIso (hX i) _

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Functor.map_isZero, CategoryTheory.Limits.IsZero.isIso
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
φ : 0 ⟶ X := 0
⊢ IsIso φ

Tactic:
have : IsIso φ := by
    rw [hP.isIso_iff]
    exact fun i ↦ (Functor.map_isZero _ (isZero_zero _)).isIso (hX i) _
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
φ : 0 ⟶ X := 0
this : IsIso φ
⊢ IsZero.{v_1, u_1} X

Tactic:
(isZero_zero C).of_iso (asIso φ).symm

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : HasZeroObject.{v_1, u_1} C
X : C
hX : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj X)
φ : 0 ⟶ X := 0
this : IsIso φ
⊢ IsZero.{v_1, u_1} X

Tactic:
exact (isZero_zero C).of_iso (asIso φ).symm

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
⊢ S.Exact ↔ ∀ (i : I), ShortComplex.Exact (S.map (F i))

Tactic:
⟨fun hS i ↦ hS.map _, fun hS ↦ ?_⟩

Premises used: CategoryTheory.ShortComplex.Exact.map, 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
refine : ∀ (hS : ∀ (i : I), ShortComplex.Exact (S.map (F i))), S.Exact
⊢ S.Exact ↔ ∀ (i : I), ShortComplex.Exact (S.map (F i))

Tactic:
refine ⟨fun hS i ↦ hS.map _, fun hS ↦ ?_⟩
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), ShortComplex.Exact (S.map (F i))
simp : ∀ (hS : ∀ (i : I), IsZero.{v_2, u_3} (ShortComplex.homology (S.map (F i)))), IsZero.{v_1, u_1} S.homology
⊢ S.Exact

Tactic:
simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), IsZero.{v_2, u_3} (ShortComplex.homology (S.map (F i)))
rw : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj S.homology)
⊢ IsZero.{v_1, u_1} S.homology

Tactic:
rw [hP.isZero_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.isZero_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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), IsZero.{v_2, u_3} (ShortComplex.homology (S.map (F i)))
⊢ ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj S.homology)

Tactic:
fun i ↦ (hS i).of_iso (S.mapHomologyIso (F i)).symm

Premises used: CategoryTheory.ShortComplex.mapHomologyIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ (i : I), IsZero.{v_2, u_3} (ShortComplex.homology (S.map (F i)))
⊢ ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj S.homology)

Tactic:
exact fun i ↦ (hS i).of_iso (S.mapHomologyIso (F i)).symm

Premises used: CategoryTheory.ShortComplex.mapHomologyIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm
-- 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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : (i : I) → HasZeroMorphisms.{v_2, u_3} (D i)
inst_4 : ∀ (i : I), (F i).PreservesZeroMorphisms
inst_5 : CategoryWithHomology.{v_1, u_1} C
inst_6 : ∀ (i : I), (F i).PreservesHomology
inst_7 : HasZeroObject.{v_1, u_1} C
α : Type u_4
c : ComplexShape α
K : HomologicalComplex.{v_1, u_1, u_4} C c
a : α
⊢ K.ExactAt a ↔ ∀ (i : I), HomologicalComplex.ExactAt (Functor.obj ((F i).mapHomologicalComplex c) K) a

Tactic:
hP.exact_iff _

Premises used: HomologicalComplex.ExactAt, CategoryTheory.JointlyReflectIsomorphisms.exact_iff, CategoryTheory.ShortComplex.map
-- 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
⊢ S.ShortExact ↔ ∀ (i : I), ShortComplex.ShortExact (S.map (F i))

Tactic:
⟨fun hS i ↦ ?_, fun hS ↦ ?_⟩

Premises used: 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 : ShortComplex.{v_1, u_1} C
refine_1 : ∀ (hS : S.ShortExact) (i : I), ShortComplex.ShortExact (S.map (F i))
refine_2 : ∀ (hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))), S.ShortExact
⊢ S.ShortExact ↔ ∀ (i : I), ShortComplex.ShortExact (S.map (F i))

Tactic:
refine ⟨fun hS i ↦ ?_, fun hS ↦ ?_⟩
-- 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 : S.ShortExact
i : I
⊢ Mono S.f

Tactic:
have := hS.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 : S.ShortExact
i : I
this : Mono S.f
⊢ Epi S.g

Tactic:
have := hS.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 : S.ShortExact
i : I
this_1 : Mono S.f
this : Epi S.g
⊢ ShortComplex.ShortExact (S.map (F i))

Tactic:
hS.map (F i)

Premises used: CategoryTheory.ShortComplex.ShortExact.map
-- 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 : S.ShortExact
i : I
this_1 : Mono S.f
this : Epi S.g
⊢ ShortComplex.ShortExact (S.map (F i))

Tactic:
exact hS.map (F i)

Premises used: CategoryTheory.ShortComplex.ShortExact.map
-- 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))
rw : ∀ (i : I), Mono ((F i).map S.f)
⊢ Mono S.f

Tactic:
rw [hP.jointlyReflectMonomorphisms.mono_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectMonomorphisms, CategoryTheory.JointlyReflectMonomorphisms.mono_iff