awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
f g : X ⟶ Y
rw : a • (functor r).map (f + g) = (functor r).map (a • f) + (functor r).map (a • g)
rw₁ : (functor r).map (a • (f + g)) = (functor r).map (a • f) + (functor r).map (a • g)
rw₂ : (functor r).map (a • (f + g)) = (functor r).map (a • f + a • g)
⊢ a • ((functor r).map f + (functor r).map g) = (functor r).map (a • f) + (functor r).map (a • g)
have rw₃ : (functor r).map (a • f + a • g) = (functor r).map (a • f + a • g)
Tactic: rw [← (functor r).map_add, smul_eq, ← (functor r).map_add, smul_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a b : R
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ (a + b) • f = a • f + b • f
have obtain : ∀ (f : X ⟶ Y), (a + b) • (functor r).map f = a • (functor r).map f + b • (functor r).map f
Tactic: obtain ⟨f, rfl⟩ := (functor r).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a b : R
f : X ⟶ Y
⊢ (a + b) • (functor r).map f = a • (functor r).map f + b • (functor r).map f
have dsimp : (functor r).map ((a + b) • f) = (functor r).map (a • f) + (functor r).map (b • f)
Tactic: dsimp [smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a b : R
f : X ⟶ Y
⊢ (functor r).map ((a + b) • f) = (functor r).map (a • f) + (functor r).map (b • f)
have rw : (functor r).map (a • f + b • f) = (functor r).map (a • f) + (functor r).map (b • f)
Tactic: rw [add_smul, Functor.map_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a b : R
f : X ⟶ Y
rw : (functor r).map (a • f + b • f) = (functor r).map (a • f) + (functor r).map (b • f)
⊢ (functor r).map ((a + b) • f) = (functor r).map (a • f) + (functor r).map (b • f)
have rw₁ : (functor r).map (a • f) + (functor r).map (b • f) = (functor r).map (a • f) + (functor r).map (b • f)
Tactic: rw [add_smul, Functor.map_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 f = 0
have obtain : ∀ (f : X ⟶ Y), HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 ((functor r).map f) = 0
Tactic: obtain ⟨f, rfl⟩ := (functor r).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
f : X ⟶ Y
⊢ HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 ((functor r).map f) = 0
have dsimp : (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 f) = 0
Tactic: dsimp [smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
f : X ⟶ Y
⊢ (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 f) = 0
have rw : Eq (α := (functor r).obj X ⟶ (functor r).obj Y) ((functor r).map 0) 0
Tactic: rw [zero_smul, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
X Y : C
smul : SMul.{u_1, v_1} R ((functor r).obj X ⟶ (functor r).obj Y) :=
  Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
f : X ⟶ Y
rw : Eq (α := (functor r).obj X ⟶ (functor r).obj Y) ((functor r).map 0) 0
⊢ (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 f) = 0
have rw₁ : Eq.{v_1 + 1} (α := (functor r).obj X ⟶ (functor r).obj Y) 0 0
Tactic: rw [zero_smul, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)
g : Quiver.Hom (V := Quotient r) (mk (r := r) Y) (mk (r := r) Z)
⊢ (a • f) ≫ g = a • f ≫ g
have obtain : ∀ (f : X ⟶ Y), (a • (functor r).map f) ≫ g = a • (functor r).map f ≫ g
Tactic: obtain ⟨f, rfl⟩ := (functor r).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
g : Quiver.Hom (V := Quotient r) (mk (r := r) Y) (mk (r := r) Z)
f : X ⟶ Y
⊢ (a • (functor r).map f) ≫ g = a • (functor r).map f ≫ g
have obtain : ∀ (g : Y ⟶ Z), (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
Tactic: obtain ⟨g, rfl⟩ := (functor r).map_surjective g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
have rw : (functor r).map (a • f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
rw : (functor r).map (a • f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
⊢ (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
have rw₁ : (functor r).map ((a • f) ≫ g) = a • (functor r).map f ≫ (functor r).map g
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
rw : (functor r).map (a • f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
rw₁ : (functor r).map ((a • f) ≫ g) = a • (functor r).map f ≫ (functor r).map g
⊢ (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
have rw₂ : (functor r).map ((a • f) ≫ g) = a • (functor r).map (f ≫ g)
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
rw : (functor r).map (a • f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
rw₁ : (functor r).map ((a • f) ≫ g) = a • (functor r).map f ≫ (functor r).map g
rw₂ : (functor r).map ((a • f) ≫ g) = a • (functor r).map (f ≫ g)
⊢ (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
have rw₃ : (functor r).map ((a • f) ≫ g) = (functor r).map (a • f ≫ g)
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
rw : (functor r).map (a • f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
rw₁ : (functor r).map ((a • f) ≫ g) = a • (functor r).map f ≫ (functor r).map g
rw₂ : (functor r).map ((a • f) ≫ g) = a • (functor r).map (f ≫ g)
rw₃ : (functor r).map ((a • f) ≫ g) = (functor r).map (a • f ≫ g)
⊢ (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
have rw₄ : (functor r).map (a • f ≫ g) = (functor r).map (a • f ≫ g)
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
f : Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)
a : R
g : Quiver.Hom (V := Quotient r) (mk (r := r) Y) (mk (r := r) Z)
⊢ f ≫ (a • g) = a • f ≫ g
have obtain : ∀ (f : X ⟶ Y), (functor r).map f ≫ (a • g) = a • (functor r).map f ≫ g
Tactic: obtain ⟨f, rfl⟩ := (functor r).map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
g : Quiver.Hom (V := Quotient r) (mk (r := r) Y) (mk (r := r) Z)
f : X ⟶ Y
⊢ (functor r).map f ≫ (a • g) = a • (functor r).map f ≫ g
have obtain : ∀ (g : Y ⟶ Z), (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g
Tactic: obtain ⟨g, rfl⟩ := (functor r).map_surjective g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g
have rw : (functor r).map f ≫ (functor r).map (a • g) = a • (functor r).map f ≫ (functor r).map g
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.comp_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
rw : (functor r).map f ≫ (functor r).map (a • g) = a • (functor r).map f ≫ (functor r).map g
⊢ (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g
have rw₁ : (functor r).map (f ≫ (a • g)) = a • (functor r).map f ≫ (functor r).map g
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.comp_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
rw : (functor r).map f ≫ (functor r).map (a • g) = a • (functor r).map f ≫ (functor r).map g
rw₁ : (functor r).map (f ≫ (a • g)) = a • (functor r).map f ≫ (functor r).map g
⊢ (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g
have rw₂ : (functor r).map (f ≫ (a • g)) = a • (functor r).map (f ≫ g)
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.comp_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
rw : (functor r).map f ≫ (functor r).map (a • g) = a • (functor r).map f ≫ (functor r).map g
rw₁ : (functor r).map (f ≫ (a • g)) = a • (functor r).map f ≫ (functor r).map g
rw₂ : (functor r).map (f ≫ (a • g)) = a • (functor r).map (f ≫ g)
⊢ (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g
have rw₃ : (functor r).map (f ≫ (a • g)) = (functor r).map (a • f ≫ g)
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.comp_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst_5 : Preadditive.{v_1, u_2} (Quotient r)
inst_6 : (functor r).Additive
this : (X Y : Quotient r) → Module.{u_1, v_1} R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
rw : (functor r).map f ≫ (functor r).map (a • g) = a • (functor r).map f ≫ (functor r).map g
rw₁ : (functor r).map (f ≫ (a • g)) = a • (functor r).map f ≫ (functor r).map g
rw₂ : (functor r).map (f ≫ (a • g)) = a • (functor r).map (f ≫ g)
rw₃ : (functor r).map (f ≫ (a • g)) = (functor r).map (a • f ≫ g)
⊢ (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g
have rw₄ : (functor r).map (a • f ≫ g) = (functor r).map (a • f ≫ g)
Tactic: rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.comp_smul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (hypothesis)
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₁₂ : HomRel.CompClosure r g₁ 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₂)
have h₁₃ : r g₁ g₂
Tactic: simp only [HomRel.compClosure_iff_self] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (goal)
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₂
⊢ 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₂)
have erw : r (f + g₁) (f + g₂)
Tactic: erw [functor_map_eq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (hypothesis)
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₂
⊢ 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)
have h₁₃ : r f₁ f₂
Tactic: simp only [HomRel.compClosure_iff_self] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Preadditive (goal)
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₂
⊢ 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)
have erw : r (f₁ + g) (f₂ + g)
Tactic: erw [functor_map_eq_iff]