awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
S : ShortComplex.{v, u} C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this : Epi d.left.f'
⊢ P S.X₂
have this₁ : Mono d.right.g'
Tactic: have := hS.mono_g' d.right
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
⊢ G.kernel.isoModSerre = inverseImage (isomorphisms C) G
have h : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), G.kernel.isoModSerre f ↔ inverseImage (isomorphisms C) G f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
⊢ G.kernel.isoModSerre f ↔ inverseImage (isomorphisms C) G f
have h : ∀ (hf : inverseImage (isomorphisms C) G f), G.kernel.isoModSerre f
Tactic: refine ⟨(G.kernel.isoModSerre_isInvertedBy_iff G).2 (by rfl) _, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : inverseImage (isomorphisms C) G f
⊢ G.kernel.isoModSerre f
have hf₁ : IsIso (G.map f)
Tactic: simp only [inverseImage_iff, isomorphisms.iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.isoModSerre f
have h : G.kernel.monoModSerre f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
h : G.kernel.monoModSerre f
⊢ G.kernel.isoModSerre f
have h₁ : G.kernel.epiModSerre f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
F : Functor.{v_1, v_2, u_1, u_2} C D
adj : G ⊣ F
inst_6 : F.Full
inst_7 : F.Faithful
⊢ G.kernel.isoModSerre = ObjectProperty.isLocal fun (x : D) ↦ x ∈ Set.range F.obj
have rw : G.kernel.isoModSerre = inverseImage (isomorphisms C) G
Tactic: rw [ObjectProperty.isLocal_eq_inverseImage_isomorphisms adj,
    isoModSerre_kernel_eq_inverseImage_isomorphisms]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
F : Functor.{v_1, v_2, u_1, u_2} C D
adj : G ⊣ F
inst_6 : F.Full
inst_7 : F.Faithful
rw : G.kernel.isoModSerre = inverseImage (isomorphisms C) G
⊢ G.kernel.isoModSerre = ObjectProperty.isLocal fun (x : D) ↦ x ∈ Set.range F.obj
have rw₁ : inverseImage (isomorphisms C) G = inverseImage (isomorphisms C) G
Tactic: rw [ObjectProperty.isLocal_eq_inverseImage_isomorphisms adj,
    isoModSerre_kernel_eq_inverseImage_isomorphisms]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : PreservesFiniteLimits G
inst_5 : PreservesFiniteColimits G
F : Functor.{v_1, v_2, u_1, u_2} C D
adj : G ⊣ F
inst_6 : F.Full
inst_7 : F.Faithful
⊢ G.IsLocalization G.kernel.isoModSerre
have rw : G.IsLocalization (inverseImage (isomorphisms C) G)
Tactic: rw [isoModSerre_kernel_eq_inverseImage_isomorphisms G]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)
have refine_1 : (∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0) → P (Abelian.image f)
Tactic: refine ⟨?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
refine_1 : (∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0) → P (Abelian.image f)
⊢ (∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)
have refine_2 : ∀ (hf : P (Abelian.image f)), ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0
Tactic: refine ⟨?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
X' : C
s : X' ⟶ X
hs : P.epiModSerre s
eq : s ≫ f = 0
⊢ P (Abelian.image f)
have refine_1 : ∀ (this : P.epiModSerre (Y := Abelian.image f) (s ≫ Abelian.factorThruImage f)), P (Abelian.image f)
Tactic: have := P.epiModSerre.comp_mem s (Abelian.factorThruImage f) hs
      (epiModSerre_of_epi _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
X' : C
s : X' ⟶ X
hs : P.epiModSerre s
eq : s ≫ f = 0
this : P.epiModSerre (Y := Abelian.image f) (s ≫ Abelian.factorThruImage f)
⊢ P (Abelian.image f)
have refine_1 : ∀ (this : P.epiModSerre (X := X') (Y := Abelian.image f) 0), P (Abelian.image f)
Tactic: rwa [show s ≫ Abelian.factorThruImage f = 0 by cat_disch,
      epiModSerre_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
X' : C
s : X' ⟶ X
hs : P.epiModSerre s
eq : s ≫ f = 0
this : P.epiModSerre (Y := Abelian.image f) (s ≫ Abelian.factorThruImage f)
refine_1 : ∀ (this : P.epiModSerre (X := X') (Y := Abelian.image f) 0), P (Abelian.image f)
⊢ P (Abelian.image f)
have refine_1₁ : ∀ (this : P (Abelian.image f)), P (Abelian.image f)
Tactic: rwa [show s ≫ Abelian.factorThruImage f = 0 by cat_disch,
      epiModSerre_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)
have refine_1 : (∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0) → P (Abelian.image f)
Tactic: refine ⟨?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
refine_1 : (∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0) → P (Abelian.image f)
⊢ (∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)
have refine_2 : ∀ (hf : P (Abelian.image f)), ∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0
Tactic: refine ⟨?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f = 0
⊢ P (Abelian.image f)
have refine_1 : ∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), s ≫ f = 0
Tactic: rw [← exists_epiModSerre_comp_eq_zero_iff P]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), s ≫ f = 0
have refine_2 : P.isoModSerre (X := kernel f) (kernel.ι f)
Tactic: refine ⟨_, kernel.ι f, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0) ↔ P (Abelian.image f)
have refine_1 : (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0) → P (Abelian.image f)
Tactic: refine ⟨?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
refine_1 : (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0) → P (Abelian.image f)
⊢ (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0) ↔ P (Abelian.image f)
have refine_2 : ∀ (hf : P (Abelian.image f)), ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0
Tactic: refine ⟨?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
⊢ P (Abelian.image f)
have refine_1 : P (Abelian.coimage f)
Tactic: apply P.prop_of_iso (Abelian.coimageIsoImage f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
⊢ P (Abelian.coimage f)
have refine_1 : ∀ (this : P.monoModSerre (X := Abelian.coimage f) (Abelian.factorThruCoimage f ≫ s)), P (Abelian.coimage f)
Tactic: have := P.monoModSerre.comp_mem (Abelian.factorThruCoimage f) s
      (monoModSerre_of_mono _ _) hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
this : P.monoModSerre (X := Abelian.coimage f) (Abelian.factorThruCoimage f ≫ s)
⊢ P (Abelian.coimage f)
have refine_1 : ∀ (this : P.monoModSerre (X := Abelian.coimage f) (Y := Y') 0), P (Abelian.coimage f)
Tactic: rwa [show Abelian.factorThruCoimage f ≫ s = 0 by cat_disch,
      monoModSerre_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
this : P.monoModSerre (X := Abelian.coimage f) (Abelian.factorThruCoimage f ≫ s)
refine_1 : ∀ (this : P.monoModSerre (X := Abelian.coimage f) (Y := Y') 0), P (Abelian.coimage f)
⊢ P (Abelian.coimage f)
have refine_1₁ : ∀ (this : P (Abelian.coimage f)), P (Abelian.coimage f)
Tactic: rwa [show Abelian.factorThruCoimage f ≫ s = 0 by cat_disch,
      monoModSerre_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0) ↔ P (Abelian.image f)
have refine_1 : (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0) → P (Abelian.image f)
Tactic: refine ⟨?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
refine_1 : (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0) → P (Abelian.image f)
⊢ (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0) ↔ P (Abelian.image f)
have refine_2 : ∀ (hf : P (Abelian.image f)), ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), f ≫ s = 0
Tactic: refine ⟨?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f ≫ s = 0
⊢ P (Abelian.image f)
have refine_1 : ∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), f ≫ s = 0
Tactic: rw [← exists_comp_monoModSerre_eq_zero_iff P]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ P.isoModSerre (Y := cokernel f) (cokernel.π f)
have rwa : P.monoModSerre (Y := cokernel f) (cokernel.π f)
Tactic: rwa [isoModSerre_iff_of_epi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
⊢ P.isoModSerre (Y := Abelian.image f) (Abelian.factorThruImage f)
have rw : P.monoModSerre (Y := Abelian.image f) (Abelian.factorThruImage f)
Tactic: rw [isoModSerre_iff_of_epi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ P.isoModSerre (X := Abelian.image f) (Abelian.image.ι f)
have rw : P.epiModSerre (X := Abelian.image f) (Abelian.image.ι f)
Tactic: rw [isoModSerre_iff_of_mono]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ P.epiModSerre (X := Abelian.image f) (Abelian.image.ι f)
have dsimp : P (cokernel (X := Abelian.image f) (kernel.ι (cokernel.π f)))
Tactic: dsimp [epiModSerre] at hf ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.isoModSerre t), f₁ ≫ t = f₂ ≫ t
have refine_1 : P.isoModSerre (Y := cokernel (f₁ - f₂)) (cokernel.π (f₁ - f₂))
Tactic: refine ⟨_, cokernel.π (f₁ - f₂), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
refine_1 : P.isoModSerre (Y := cokernel (f₁ - f₂)) (cokernel.π (f₁ - f₂))
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : P.isoModSerre t), f₁ ≫ t = f₂ ≫ t
have refine_2 : Eq (α := X ⟶ cokernel (f₁ - f₂)) (f₁ ≫ cokernel.π (f₁ - f₂)) (f₂ ≫ cokernel.π (f₁ - f₂))
Tactic: refine ⟨_, cokernel.π (f₁ - f₂), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ P.isoModSerre (Y := cokernel (f₁ - f₂)) (cokernel.π (f₁ - f₂))
have refine_1 : P.monoModSerre (Y := cokernel (f₁ - f₂)) (cokernel.π (f₁ - f₂))
Tactic: rw [isoModSerre_iff_of_epi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ ∃ (X' : C) (t : X' ⟶ X) (_ : P.isoModSerre t), t ≫ f₁ = t ≫ f₂
have refine_1 : P.isoModSerre (X := kernel (f₁ - f₂)) (kernel.ι (f₁ - f₂))
Tactic: refine ⟨_, kernel.ι (f₁ - f₂), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
refine_1 : P.isoModSerre (X := kernel (f₁ - f₂)) (kernel.ι (f₁ - f₂))
⊢ ∃ (X' : C) (t : X' ⟶ X) (_ : P.isoModSerre t), t ≫ f₁ = t ≫ f₂
have refine_2 : Eq (α := kernel (f₁ - f₂) ⟶ Y) (kernel.ι (f₁ - f₂) ≫ f₁) (kernel.ι (f₁ - f₂) ≫ f₂)
Tactic: refine ⟨_, kernel.ι (f₁ - f₂), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
E : Type u''
inst_4 : Category.{v'', u''} E
inst_5 : Abelian.{v'', u''} E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ P.isoModSerre (X := kernel (f₁ - f₂)) (kernel.ι (f₁ - f₂))
have refine_1 : P.epiModSerre (X := kernel (f₁ - f₂)) (kernel.ι (f₁ - f₂))
Tactic: rw [isoModSerre_iff_of_mono]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X : C
⊢ IsZero.{v', u'} (L.obj X) ↔ P X
have simp : (∃ (X_1 : C), P.isoModSerre (X := X_1) (Y := X) 0) ↔ P X
Tactic: simp only [IsZero.iff_id_eq_zero, ← L.map_id, ← L.map_zero,
    MorphismProperty.map_eq_iff_precomp L P.isoModSerre,
    Category.comp_id, comp_zero, exists_prop, exists_eq_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X : C
⊢ (∃ (X_1 : C), P.isoModSerre (X := X_1) (Y := X) 0) ↔ P X
have refine : (∃ (X_1 : C), P.isoModSerre (X := X_1) (Y := X) 0) → P X
Tactic: refine ⟨?_, fun _ ↦ ⟨X, by simpa⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : C
f : X ⟶ Y
⊢ L.map f = 0 ↔ P (Abelian.image f)
have rw : (∃ (X_1 : C) (s : X_1 ⟶ X) (_ : P.isoModSerre s), s ≫ f = s ≫ 0) ↔ P (Abelian.image f)
Tactic: rw [← L.map_zero, MorphismProperty.map_eq_iff_precomp L P.isoModSerre]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst_7 : Epi f
inst_8 : Mono g
⊢ L.map f ≫ L.map g = 0 ↔ P Z
have rw : P (Abelian.image (f ≫ g)) ↔ P Z
Tactic: rw [← L.map_comp, map_eq_zero_iff L P]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
inst_7 : Epi f
inst_8 : Mono g
⊢ P (Abelian.image (f ≫ g)) ↔ P Z
have this : StrongEpi f
Tactic: have := strongEpi_of_epi f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : C
f : X ⟶ Y
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0].TFAE
have this : L.EssSurj
Tactic: have := Localization.essSurj L P.isoModSerre
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Localization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
L : Functor.{v, v', u, u'} C D
P : ObjectProperty.{v, u} C
inst_3 : P.IsSerreClass
inst_4 : L.IsLocalization P.isoModSerre
inst_5 : Preadditive.{v', u'} D
inst_6 : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
h : Mono (L.map f)
⊢ Eq (α := L.obj (kernel f) ⟶ L.obj X) (L.map (kernel.ι f)) 0
have rw : Eq (α := L.obj (kernel f) ⟶ L.obj Y) (L.map (kernel.ι f) ≫ L.map f) (0 ≫ L.map f)
Tactic: rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]