awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have obtain : ∀ (Z : C)
  (r :
    Z ⟶
      Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
        ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a))
  (q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left),
  Epi r →
    ∀ (eq : Epi q)
      (comm :
        r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom),
      Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Tactic: obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
⊢ CategoryStruct.comp (Y := kernel (Y := cokernel S.f) (cokernel.π S.f)) (r ≫ a.hom ≫ Abelian.factorThruImage S.f)
      (kernel.ι (cokernel.π S.f)) =
    q ≫ kernel.ι S.g
have simp : r ≫ a.hom ≫ S.f = q ≫ kernel.ι S.g
Tactic: simp only [Category.assoc, Abelian.image.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have obtain : ∀
  (z :
    Z ⟶
      pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
        (kernel.ι S.g)),
  z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f →
    ∀ (hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q),
      Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Tactic: obtain ⟨z, _, hz₂⟩ := @pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π S.f))
        (kernel.ι S.g) _ (r ≫ a.hom ≫ Abelian.factorThruImage S.f) q (by
          simp only [Category.assoc, Abelian.image.fac]
          exact comm)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
z :
  Z ⟶
    pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
      (kernel.ι S.g)
left : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
    (kernel.ι S.g) ⟶
  kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have pe : Epi j
Tactic: haveI pe : Epi j := epi_of_epi_fac hz₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
z :
  Z ⟶
    pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
      (kernel.ι S.g)
left : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
    (kernel.ι S.g) ⟶
  kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have this₁ : IsIso j
Tactic: haveI : IsIso j := isIso_of_mono_of_epi _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this_1 :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
z :
  Z ⟶
    pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
      (kernel.ι S.g)
left : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
    (kernel.ι S.g) ⟶
  kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have rw : Eq (α := kernel S.g ⟶ cokernel S.f)
  (((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
    cokernel.π S.f)
  0
Tactic: rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
⊢ Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a''))) (pseudoApply g ⟦a⟧)
have obtain : ∀ (X : C)
  (p' :
    X ⟶
      Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
        ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a'))
  (q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)) (ep' : Epi p'),
  Epi q' →
    ∀ (comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)),
      Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a''))) (pseudoApply g ⟦a⟧)
Tactic: obtain ⟨X, p', q', ep', _, comm'⟩ := Quotient.exact hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
⊢ a'.hom ≫ g = 0
have apply : p' ≫ a'.hom ≫ g = 0
Tactic: apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
⊢ Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a''))) (pseudoApply g ⟦a⟧)
have this : a'.hom ≫ g = 0
Tactic: have : a'.hom ≫ g = 0 := by
            apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)
            simpa using comm'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
this : a'.hom ≫ g = 0
⊢ Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a''))) (pseudoApply g ⟦a⟧)
have a₁ : HasEquiv.Equiv (α := Over.{v, u} Z) ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) (Over.mk a''))
  ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a)
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
⊢ ∃ (s : Pseudoelement.{v, u} (pullback f g)),
    pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
have obtain : ∀ (Z : C)
  (a :
    Z ⟶
      Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
        ((fun (g : Over.{v, u} P) ↦ app f g) x))
  (b :
    Z ⟶
      Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
        ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y))
  (ea : Epi a) (eb : Epi b)
  (comm :
    a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)),
  ∃ (s : Pseudoelement.{v, u} (pullback f g)),
    pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
Tactic: obtain ⟨Z, a, b, ea, eb, comm⟩ := Quotient.exact h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
⊢ (a ≫ x.hom) ≫ f = (b ≫ y.hom) ≫ g
have simp : a ≫ x.hom ≫ f = b ≫ y.hom ≫ g
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
⊢ ∃ (s : Pseudoelement.{v, u} (pullback f g)),
    pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
have obtain : ∀ (l : Z ⟶ pullback f g) (hl₁ : l ≫ pullback.fst f g = a ≫ x.hom) (hl₂ : l ≫ pullback.snd f g = b ≫ y.hom),
  ∃ (s : Pseudoelement.{v, u} (pullback f g)),
    pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
Tactic: obtain ⟨l, hl₁, hl₂⟩ := @pullback.lift' _ _ _ _ _ _ f g _ (a ≫ x.hom) (b ≫ y.hom) (by
      simp only [Category.assoc]
      exact comm)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ 𝟙 Z ≫ Over.hom ((fun (g_1 : Over.{v, u} (pullback f g)) ↦ app (pullback.fst f g) g_1) (Over.mk l)) = a ≫ x.hom
have rwa : Over.hom ((fun (g_1 : Over.{v, u} (pullback f g)) ↦ app (pullback.fst f g) g_1) (Over.mk l)) = a ≫ x.hom
Tactic: rwa [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement.{v, u} P
q : Pseudoelement.{v, u} Q
x : Over.{v, u} P
y : Over.{v, u} Q
h : Eq (α := Pseudoelement.{v, u} R) (pseudoApply f ⟦x⟧) (pseudoApply g ⟦y⟧)
Z : C
a :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g : Over.{v, u} P) ↦ app f g) x)
b :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit R)
      ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
ea : Epi a
eb : Epi b
comm : a ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) x) = b ≫ Over.hom ((fun (g_1 : Over.{v, u} Q) ↦ app g g_1) y)
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst f g = a ≫ x.hom
hl₂ : l ≫ pullback.snd f g = b ≫ y.hom
⊢ 𝟙 Z ≫ Over.hom ((fun (g_1 : Over.{v, u} (pullback f g)) ↦ app (pullback.snd f g) g_1) (Over.mk l)) = b ≫ y.hom
have rwa : Over.hom ((fun (g_1 : Over.{v, u} (pullback f g)) ↦ app (pullback.snd f g) g_1) (Over.mk l)) = b ≫ y.hom
Tactic: rwa [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
h : PseudoEqual G x y
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range
have obtain : ∀ (P : ModuleCat.{u_2, u_1} R) (p : P ⟶ x.left) (q : P ⟶ y.left) (hp : Epi p) (hq : Epi q) (H : p ≫ x.hom = q ≫ y.hom),
  (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range
Tactic: obtain ⟨P, p, q, hp, hq, H⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range
have refine_1 : ∀ (a : (↑G : Type u_2)) (ha : a ∈ (ModuleCat.Hom.hom x.hom).range), a ∈ (ModuleCat.Hom.hom y.hom).range
Tactic: refine Submodule.ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
refine_1 : ∀ (a : (↑G : Type u_2)) (ha : a ∈ (ModuleCat.Hom.hom x.hom).range), a ∈ (ModuleCat.Hom.hom y.hom).range
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range
have refine_2 : ∀ (a : (↑G : Type u_2)) (ha : a ∈ (ModuleCat.Hom.hom y.hom).range), a ∈ (ModuleCat.Hom.hom x.hom).range
Tactic: refine Submodule.ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
ha : a ∈ (ModuleCat.Hom.hom x.hom).range
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range
have refine_1 : ∀ (a' : (↑x.left : Type u_2)) (ha' : (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2)) a' = a),
  a ∈ (ModuleCat.Hom.hom y.hom).range
Tactic: obtain ⟨a', ha'⟩ := ha
Cleared hypotheses: ha