awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 g : X ⟶ Y
f g₁ g₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r g₁ g₂
⊢ r (f + g₁) (f + g₂)

Tactic:
exact hr _ _ _ _ (Congruence.equivalence.refl f) h₁₂

Premises used: Equivalence.refl, CategoryTheory.Congruence.equivalence
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f g_1 : X ⟶ Y
f₁ f₂ g : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : HomRel.CompClosure r f₁ f₂
⊢ r f₁ f₂

Tactic:
simp only [HomRel.compClosure_iff_self] at h₁₂

Premises used: CategoryTheory.HomRel.compClosure_iff_self
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f g_1 : X ⟶ Y
f₁ f₂ g : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
erw : r (f₁ + g) (f₂ + g)
⊢ Eq.{v_1 + 1} (α := X ⟶ Y)
    ((fun (a b : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (a + b) : Quot (α := X.as (r := r) ⟶ Y.as (r := r)) (HomRel.CompClosure r)))
      f₁ g)
    ((fun (a b : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (a + b) : Quot (α := X.as (r := r) ⟶ Y.as (r := r)) (HomRel.CompClosure r)))
      f₂ g)

Tactic:
erw [functor_map_eq_iff]

Premises used: CategoryTheory.Quotient.functor_map_eq_iff
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f g_1 : X ⟶ Y
f₁ f₂ g : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
⊢ r (f₁ + g) (f₂ + g)

Tactic:
hr _ _ _ _ h₁₂ (Congruence.equivalence.refl g)

Premises used: Equivalence.refl, CategoryTheory.Congruence.equivalence
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f g_1 : X ⟶ Y
f₁ f₂ g : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
⊢ r (f₁ + g) (f₂ + g)

Tactic:
exact hr _ _ _ _ h₁₂ (Congruence.equivalence.refl g)

Premises used: Equivalence.refl, CategoryTheory.Congruence.equivalence
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : HomRel.CompClosure r f g
⊢ r f g

Tactic:
simp only [HomRel.compClosure_iff_self] at hfg

Premises used: CategoryTheory.HomRel.compClosure_iff_self
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
erw : r (-f) (-g)
⊢ Eq.{v_1 + 1} (α := X ⟶ Y)
    ((fun (a : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (-a) : Quot (α := X.as (r := r) ⟶ Y.as (r := r)) (HomRel.CompClosure r)))
      f)
    ((fun (a : X.as (r := r) ⟶ Y.as (r := r)) ↦
        (Quot.mk (HomRel.CompClosure r) (-a) : Quot (α := X.as (r := r) ⟶ Y.as (r := r)) (HomRel.CompClosure r)))
      g)

Tactic:
erw [functor_map_eq_iff]

Premises used: CategoryTheory.Quotient.functor_map_eq_iff
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
apply : r (-g) (-f)
⊢ r (-f) (-g)

Tactic:
apply Congruence.equivalence.symm

Premises used: Equivalence.symm, CategoryTheory.Congruence.equivalence
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
⊢ r (f + (-f - g)) (g + (-f - g))

Tactic:
hr f g _ _ hfg (Congruence.equivalence.refl (-f - g))

Premises used: Equivalence.refl, CategoryTheory.Congruence.equivalence, HSub.hSub, Neg.neg
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
h : -g = f + (-f - g)
h₁ : -f = g + (-f - g)
⊢ r (-g) (-f)

Tactic:
convert! hr f g _ _ hfg (Congruence.equivalence.refl (-f - g)) using 1

Premises used: Equivalence.refl, CategoryTheory.Congruence.equivalence, HSub.hSub, Neg.neg
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
⊢ -g = f + (-f - g)

Tactic:
abel
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f_1 : X ⟶ Y
f g : X.as (r := r) ⟶ Y.as (r := r)
hfg : r f g
⊢ -f = g + (-f - g)

Tactic:
abel
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
b : P ⟶ Q
a_2 : P.as (r := r) ⟶ Q.as (r := r)
c : P ⟶ Q
a_3 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a_2) +
      Quot.mk (HomRel.CompClosure r) a_3 =
    Quot.mk (HomRel.CompClosure r) a_1 +
      HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_2) (Quot.mk (HomRel.CompClosure r) a_3)

Tactic:
congr_arg (functor r).map (add_assoc _ _ _)

Premises used: add_assoc, CategoryTheory.Quotient.functor, Quot.lift₂, Quot.liftOn₂, CategoryTheory.Functor.map, congr_arg, CategoryTheory.Quotient.Preadditive.add
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
b : P ⟶ Q
a_2 : P.as (r := r) ⟶ Q.as (r := r)
c : P ⟶ Q
a_3 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a_2) +
      Quot.mk (HomRel.CompClosure r) a_3 =
    Quot.mk (HomRel.CompClosure r) a_1 +
      HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_2) (Quot.mk (HomRel.CompClosure r) a_3)

Tactic:
exact congr_arg (functor r).map (add_assoc _ _ _)

Premises used: add_assoc, CategoryTheory.Quotient.functor, CategoryTheory.Functor.map, congr_arg
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) 0 (Quot.mk (HomRel.CompClosure r) a_1) = Quot.mk (HomRel.CompClosure r) a_1

Tactic:
congr_arg (functor r).map (zero_add _)

Premises used: CategoryTheory.Quotient.functor, Quot.lift₂, Quot.liftOn₂, zero_add, CategoryTheory.Functor.map, congr_arg, CategoryTheory.Quotient.Preadditive.add
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) 0 (Quot.mk (HomRel.CompClosure r) a_1) = Quot.mk (HomRel.CompClosure r) a_1

Tactic:
exact congr_arg (functor r).map (zero_add _)

Premises used: CategoryTheory.Quotient.functor, zero_add, CategoryTheory.Functor.map, congr_arg
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_1) 0 = Quot.mk (HomRel.CompClosure r) a_1

Tactic:
congr_arg (functor r).map (add_zero _)

Premises used: CategoryTheory.Quotient.functor, Quot.lift₂, Quot.liftOn₂, CategoryTheory.Functor.map, congr_arg, CategoryTheory.Quotient.Preadditive.add, add_zero
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_1) 0 = Quot.mk (HomRel.CompClosure r) a_1

Tactic:
exact congr_arg (functor r).map (add_zero _)

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Functor.map, congr_arg, add_zero
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (-Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a_1) = 0

Tactic:
congr_arg (functor r).map (neg_add_cancel _)

Premises used: CategoryTheory.Quotient.functor, Quot.lift₂, Quot.liftOn₂, CategoryTheory.Functor.map, congr_arg, CategoryTheory.Quotient.Preadditive.add, neg_add_cancel
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (-Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a_1) = 0

Tactic:
exact congr_arg (functor r).map (neg_add_cancel _)

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Functor.map, congr_arg, neg_add_cancel
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
b : P ⟶ Q
a_2 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a_2) =
    HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_2) (Quot.mk (HomRel.CompClosure r) a_1)

Tactic:
congr_arg (functor r).map (add_comm _ _)

Premises used: CategoryTheory.Quotient.functor, Quot.lift₂, Quot.liftOn₂, add_comm, CategoryTheory.Functor.map, congr_arg, CategoryTheory.Quotient.Preadditive.add
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
b : P ⟶ Q
a_2 : P.as (r := r) ⟶ Q.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a_2) =
    HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a_2) (Quot.mk (HomRel.CompClosure r) a_1)

Tactic:
exact congr_arg (functor r).map (add_comm _ _)

Premises used: CategoryTheory.Quotient.functor, add_comm, CategoryTheory.Functor.map, congr_arg
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q R : Quotient r
f : P ⟶ Q
a : P.as (r := r) ⟶ Q.as (r := r)
f' : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
g : Q ⟶ R
a_2 : Q.as (r := r) ⟶ R.as (r := r)
⊢ (a + a_1) ≫ a_2 = a ≫ a_2 + a_1 ≫ a_2

Tactic:
apply Preadditive.add_comp

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q R : Quotient r
f : P ⟶ Q
a : P.as (r := r) ⟶ Q.as (r := r)
f' : P ⟶ Q
a_1 : P.as (r := r) ⟶ Q.as (r := r)
g : Q ⟶ R
a_2 : Q.as (r := r) ⟶ R.as (r := r)
⊢ HAdd.hAdd (α := P ⟶ Q) (Quot.mk (HomRel.CompClosure r) a) (Quot.mk (HomRel.CompClosure r) a_1) ≫
      Quot.mk (HomRel.CompClosure r) a_2 =
    HAdd.hAdd (α := P ⟶ R) (Quot.mk (HomRel.CompClosure r) a ≫ Quot.mk (HomRel.CompClosure r) a_2)
      (Quot.mk (HomRel.CompClosure r) a_1 ≫ Quot.mk (HomRel.CompClosure r) a_2)

Tactic:
exact congr_arg (functor r).map (by apply Preadditive.add_comp)

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Functor.map, congr_arg
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q R : Quotient r
f : P ⟶ Q
a : P.as (r := r) ⟶ Q.as (r := r)
g : Q ⟶ R
a_1 : Q.as (r := r) ⟶ R.as (r := r)
g' : Q ⟶ R
a_2 : Q.as (r := r) ⟶ R.as (r := r)
⊢ a ≫ (a_1 + a_2) = a ≫ a_1 + a ≫ a_2

Tactic:
apply Preadditive.comp_add

Premises used: CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q R : Quotient r
f : P ⟶ Q
a : P.as (r := r) ⟶ Q.as (r := r)
g : Q ⟶ R
a_1 : Q.as (r := r) ⟶ R.as (r := r)
g' : Q ⟶ R
a_2 : Q.as (r := r) ⟶ R.as (r := r)
⊢ Quot.mk (HomRel.CompClosure r) a ≫
      HAdd.hAdd (α := Q ⟶ R) (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a_2) =
    HAdd.hAdd (α := P ⟶ R) (Quot.mk (HomRel.CompClosure r) a ≫ Quot.mk (HomRel.CompClosure r) a_1)
      (Quot.mk (HomRel.CompClosure r) a ≫ Quot.mk (HomRel.CompClosure r) a_2)

Tactic:
exact congr_arg (functor r).map (by apply Preadditive.comp_add)

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Functor.map, congr_arg
-- Module: Mathlib.CategoryTheory.Quotient.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_2 : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
⊢ (functor r).Additive

Tactic:
letI := preadditive r hr
  { map_add := rfl }

Premises used: CategoryTheory.Functor.Additive.mk, rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y : C
f g : X ⟶ Y
⊢ F.homRel f g ↔ F.map f = F.map g

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.Functor.homRel
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
⊢ CompClosure r m₁ m₂

Tactic:
simpa using CompClosure.intro _ _ (𝟙 _) m₁ m₂ (𝟙 _) h

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.HomRel.CompClosure.intro
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
a b e : C
f : a ⟶ b
X Y c d : C
h₁ h₂ : c ⟶ d
h : r h₁ h₂
g : b ⟶ c
i : d ⟶ e
⊢ CompClosure r (f ≫ g ≫ h₁ ≫ i) (f ≫ g ≫ h₂ ≫ i)

Tactic:
simpa using CompClosure.intro _ _ (f ≫ g) _ _ i h

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.HomRel.CompClosure.intro
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
a d e : C
g : d ⟶ e
X Y b c : C
g₁ g₂ : b ⟶ c
h : r g₁ g₂
f : a ⟶ b
i : c ⟶ d
⊢ CompClosure r ((f ≫ g₁ ≫ i) ≫ g) ((f ≫ g₂ ≫ i) ≫ g)

Tactic:
simpa using CompClosure.intro _ _ f _ _ (i ≫ g) h

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.HomRel.CompClosure.intro
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : IsStableUnderPrecomp r
inst_2 : IsStableUnderPostcomp r
X Y : C
f g : X ⟶ Y
⊢ CompClosure r f g ↔ r f g

Tactic:
⟨?_, CompClosure.of⟩

Premises used: CategoryTheory.HomRel.CompClosure.of, Iff.intro
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : IsStableUnderPrecomp r
inst_2 : IsStableUnderPostcomp r
X Y : C
f g : X ⟶ Y
refine : CompClosure r f g → r f g
⊢ CompClosure r f g ↔ r f g

Tactic:
refine ⟨?_, CompClosure.of⟩
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : IsStableUnderPrecomp r
inst_2 : IsStableUnderPostcomp r
X_1 Y_1 X Y a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
f : X_1 ⟶ a
g : b ⟶ Y_1
⊢ r (f ≫ m₁ ≫ g) (f ≫ m₂ ≫ g)

Tactic:
HomRel.comp_left _ (HomRel.comp_right _ h)

Premises used: CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left, CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : IsStableUnderPrecomp r
inst_2 : IsStableUnderPostcomp r
X_1 Y_1 X Y a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
f : X_1 ⟶ a
g : b ⟶ Y_1
⊢ r (f ≫ m₁ ≫ g) (f ≫ m₂ ≫ g)

Tactic:
exact HomRel.comp_left _ (HomRel.comp_right _ h)

Premises used: CategoryTheory.HomRel.IsStableUnderPrecomp.comp_left, CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : IsStableUnderPrecomp r
inst_2 : IsStableUnderPostcomp r
h : ∀ (x x_1 : C) (x_2 x_3 : x ⟶ x_1), CompClosure r x_2 x_3 ↔ r x_2 x_3
⊢ CompClosure r = r

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : IsStableUnderPrecomp r
inst_2 : IsStableUnderPostcomp r
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ CompClosure r x_2 x_3 ↔ r x_2 x_3

Tactic:
simp only [compClosure_iff_self]

Premises used: CategoryTheory.HomRel.compClosure_iff_self
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
r : HomRel.{u_1, v_1} C_1
C : Type u_2
D : Type u_3
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
F : Functor.{v_2, v_3, u_2, u_3} C D
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z}, F.homRel g g' → F.homRel (f ≫ g) (f ≫ g')

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
r : HomRel.{u_1, v_1} C_1
C : Type u_2
D : Type u_3
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
F : Functor.{v_2, v_3, u_2, u_3} C D
⊢ ∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z), F.homRel f f' → F.homRel (f ≫ g) (f' ≫ g)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
r : HomRel.{u_1, v_1} C_1
C : Type u_2
D : Type u_3
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
F : Functor.{v_2, v_3, u_2, u_3} C D
X Y : C
⊢ ∀ {x y : X ⟶ Y}, F.homRel x y → F.homRel y x

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C_1 : Type u_1
inst : Category.{v_1, u_1} C_1
r : HomRel.{u_1, v_1} C_1
C : Type u_2
D : Type u_3
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} D
F : Functor.{v_2, v_3, u_2, u_3} C D
X Y : C
⊢ ∀ {x y z : X ⟶ Y}, F.homRel x y → F.homRel y z → F.homRel x z

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
a b c : Quotient r
f : a.as (r := r) ⟶ b.as (r := r)
g : b.as (r := r) ⟶ c.as (r := r)
⊢ comp r (Quot.mk (HomRel.CompClosure r) f) (Quot.mk (HomRel.CompClosure r) g) = Quot.mk (HomRel.CompClosure r) (f ≫ g)

Tactic:
rfl

Premises used: CategoryTheory.Quotient.comp, rfl
-- Module: Mathlib.CategoryTheory.Quotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
X Y : Quotient r
f : Hom r X Y
⊢ ∀ (a : X.as (r := r) ⟶ Y.as (r := r)),
    comp r (Quot.mk (HomRel.CompClosure r) (𝟙 (X.as (r := r)))) (Quot.mk (HomRel.CompClosure r) a) =
      Quot.mk (HomRel.CompClosure r) a

Tactic:
simp