awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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)))
⊢ IsZero.{v_1, u_1} S.homology
have rw : ∀ (i : I), IsZero.{v_2, u_3} ((F i).obj S.homology)
Tactic: rw [hP.isZero_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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))
have refine_1 : ∀ (hS : S.ShortExact) (i : I), ShortComplex.ShortExact (S.map (F i))
Tactic: refine ⟨fun hS i ↦ ?_, fun hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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))
⊢ S.ShortExact ↔ ∀ (i : I), ShortComplex.ShortExact (S.map (F i))
have refine_2 : ∀ (hS : ∀ (i : I), ShortComplex.ShortExact (S.map (F i))), S.ShortExact
Tactic: refine ⟨fun hS i ↦ ?_, fun hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (hypothesis)
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
⊢ ShortComplex.ShortExact (S.map (F i))
have this : Mono S.f
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (hypothesis)
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
⊢ ShortComplex.ShortExact (S.map (F i))
have this₁ : Epi S.g
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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
have rw : ∀ (i : I), Mono ((F i).map S.f)
Tactic: rw [hP.jointlyReflectMonomorphisms.mono_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (hypothesis)
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))
⊢ S.ShortExact
have this : Mono S.f
Tactic: have : Mono S.f := by
      rw [hP.jointlyReflectMonomorphisms.mono_iff]
      exact fun i ↦ (hS i).mono_f
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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
have rw : ∀ (i : I), Epi ((F i).map S.g)
Tactic: rw [hP.jointlyReflectEpimorphisms.epi_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (hypothesis)
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
⊢ S.ShortExact
have this₁ : Epi S.g
Tactic: have : Epi S.g := by
      rw [hP.jointlyReflectEpimorphisms.epi_iff]
      exact fun i ↦ (hS i).epi_g
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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)
have refine : ∀
  (hf :
    ∀ (i : I),
      ShortComplex.QuasiIso (S₁ := Functor.obj (F i).mapShortComplex S₁) (Functor.map (F i).mapShortComplex f)),
  ShortComplex.QuasiIso f
Tactic: refine ⟨fun hf i ↦ inferInstance, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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)
⊢ ShortComplex.QuasiIso f
have 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)
Tactic: simp only [ShortComplex.quasiIso_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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))
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (ShortComplex.homologyMap f)
have rw : ∀ (i : I), IsIso (X := (F i).obj S₁.homology) (Y := (F i).obj S₂.homology) ((F i).map (ShortComplex.homologyMap f))
Tactic: rw [hP.isIso_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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
⊢ QuasiIso f ↔
    ∀ (i : I),
      QuasiIso (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
have 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
Tactic: simp only [_root_.quasiIso_iff, hP.quasiIsoAt_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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
⊢ (∀ (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
have mp : (∀ (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
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Exact (goal)
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
mp :
  (∀ (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
⊢ (∀ (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
have mpr : (∀ (i : I) (i_1 : α),
    QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
      i_1) →
  ∀ (i : α) (i_1 : I),
    QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K) (Functor.map ((F i_1).mapHomologicalComplex c) f)
      i
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly (goal)
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)
⊢ IsIso (X := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g))
have obtain : ∀ (l : (F i).obj X ⟶ (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) sorry).pt)
  (hl : l ≫ (Fork.ofι (P := (F i).obj (equalizer f g)) ((F i).map (equalizer.ι f g)) sorry).ι = 𝟙 ((F i).obj X)),
  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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly (goal)
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
⊢ Mono f
have have : ∀ (hc : IsLimit (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) sorry)), Mono f
Tactic: have hc := pullbackIsPullback f f
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly (goal)
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) ⋯)
⊢ Mono f
have rw : ∀ (i : I), IsIso ((F i).map (PullbackCone.mk (W := pullback f f) (pullback.fst f f) (pullback.snd f f) sorry).fst)
Tactic: rw [mono_iff_isIso_fst hc, h.isIso_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly (goal)
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
⊢ Epi f
have have : ∀ (hc : IsColimit (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) sorry)), Epi f
Tactic: have hc := pushoutIsPushout f f
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly (goal)
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) ⋯)
⊢ Epi f
have rw : ∀ (i : I), IsIso ((F i).map (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) sorry).inl)
Tactic: rw [epi_iff_isIso_inl hc, h.isIso_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Limits (goal)
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
⊢ IsLimit c
have suffices : IsIso (Y := limit G) (limit.lift G c)
Tactic: suffices IsIso (limit.lift _ c) from
    IsLimit.ofIsoLimit (limit.isLimit _)
      (Cone.ext (asIso (limit.lift _ c) :)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Limits (goal)
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
⊢ IsIso (Y := limit G) (limit.lift G c)
have rw : ∀ (i : I), IsIso (Y := (F i).obj (limit G)) ((F i).map (limit.lift G c))
Tactic: rw [hF.isIso_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Limits (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
e : ((F i).mapCone c).pt ≅ ((F i).mapCone (limit.cone G)).pt := (hc i).conePointUniqueUpToIso H
⊢ IsIso (Y := (F i).obj (limit G)) ((F i).map (limit.lift G c))
have this : e.hom = (F i).map (limit.lift G c)
Tactic: have : e.hom = (F i).map (limit.lift G c) :=
    H.hom_ext (fun j ↦ by
      simpa [← Functor.map_comp] using
        IsLimit.conePointUniqueUpToIso_hom_comp (hc i) H j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Limits (goal)
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
e : ((F i).mapCone c).pt ≅ ((F i).mapCone (limit.cone G)).pt := (hc i).conePointUniqueUpToIso H
this : e.hom = (F i).map (limit.lift G c)
⊢ IsIso (Y := (F i).obj (limit G)) ((F i).map (limit.lift G c))
have rw : IsIso e.hom
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Limits (goal)
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
⊢ IsColimit c
have suffices : IsIso (X := colimit G) (colimit.desc G c)
Tactic: suffices IsIso (colimit.desc _ c) from
    IsColimit.ofIsoColimit (colimit.isColimit _)
      (Cocone.ext (asIso (colimit.desc _ c) :))
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Limits (goal)
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
⊢ IsIso (X := colimit G) (colimit.desc G c)
have rw : ∀ (i : I), IsIso (X := (F i).obj (colimit G)) ((F i).map (colimit.desc G c))
Tactic: rw [hF.isIso_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Limits (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
e : ((F i).mapCocone (colimit.cocone G)).pt ≅ ((F i).mapCocone c).pt := H.coconePointUniqueUpToIso (hc i)
⊢ IsIso (X := (F i).obj (colimit G)) ((F i).map (colimit.desc G c))
have this : e.hom = (F i).map (colimit.desc G c)
Tactic: have : e.hom = (F i).map (colimit.desc G c) :=
    H.hom_ext (fun j ↦ by
      simpa [← Functor.map_comp] using
        IsColimit.comp_coconePointUniqueUpToIso_hom H (hc i) j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.ReflectsIso.Limits (goal)
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
e : ((F i).mapCocone (colimit.cocone G)).pt ≅ ((F i).mapCocone c).pt := H.coconePointUniqueUpToIso (hc i)
this : e.hom = (F i).map (colimit.desc G c)
⊢ IsIso (X := (F i).obj (colimit G)) ((F i).map (colimit.desc G c))
have rw : IsIso e.hom
Tactic: rw [← this]