awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
obtain : ∀ (f : X ⟶ Y), (a * b) • (functor r).map f = a • b • (functor r).map f
⊢ (a * b) • f = a • b • f

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
dsimp : (functor r).map ((a * b) • f) = (functor r).map (a • b • f)
⊢ (a * b) • (functor r).map f = a • b • (functor r).map f

Tactic:
dsimp [smul]
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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 rw₁ : (functor r).map (a • b • f) = (functor r).map (a • b • f)
⊢ (functor r).map ((a * b) • f) = (functor r).map (a • b • f)

Tactic:
rw [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
obtain : ∀ (f : X ⟶ Y), HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 ((functor r).map f) = (functor r).map f
⊢ HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 f = f

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
dsimp : (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 f) = (functor r).map f
⊢ HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 ((functor r).map f) = (functor r).map f

Tactic:
dsimp [smul]
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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 rw₁ : (functor r).map f = (functor r).map f
⊢ (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 f) = (functor r).map f

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
rw : HSMul.hSMul (β := (functor r).obj X ⟶ (functor r).obj Y) a ((functor r).map 0) = (functor r).map 0
rw₁ : (functor r).map (HSMul.hSMul (β := X ⟶ Y) a 0) = (functor r).map 0
rw₂ rw₃ : Eq (α := (functor r).obj X ⟶ (functor r).obj Y) ((functor r).map 0) ((functor r).map 0)
⊢ HSMul.hSMul (β := (functor r).obj X ⟶ (functor r).obj Y) a 0 = 0

Tactic:
rw [← (functor r).map_zero X Y, smul_eq, smul_zero]

Premises used: CategoryTheory.Quotient.Linear.smul_eq, CategoryTheory.Quotient.functor, CategoryTheory.Functor.map_zero, smul_zero
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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 : (functor r).obj X ⟶ (functor r).obj Y
obtain : ∀ (f : X ⟶ Y), a • ((functor r).map f + g) = a • (functor r).map f + a • g
⊢ a • (f + g) = a • f + a • g

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
g : (functor r).obj X ⟶ (functor r).obj Y
f : X ⟶ Y
obtain : ∀ (g : X ⟶ Y), a • ((functor r).map f + (functor r).map g) = a • (functor r).map f + a • (functor r).map g
⊢ a • ((functor r).map f + g) = a • (functor r).map f + a • g

Tactic:
obtain ⟨g, rfl⟩ := (functor r).map_surjective g

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
dsimp : a • ((functor r).map f + (functor r).map g) = (functor r).map (a • f) + (functor r).map (a • g)
⊢ a • ((functor r).map f + (functor r).map g) = a • (functor r).map f + a • (functor r).map g

Tactic:
dsimp [smul]
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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)
rw₃ rw₄ : (functor r).map (a • f + a • 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)

Tactic:
rw [← (functor r).map_add, smul_eq, ← (functor r).map_add, smul_add]

Premises used: CategoryTheory.Quotient.Linear.smul_eq, CategoryTheory.Quotient.functor, CategoryTheory.Functor.map_add, smul_add
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
obtain : ∀ (f : X ⟶ Y), (a + b) • (functor r).map f = a • (functor r).map f + b • (functor r).map f
⊢ (a + b) • f = a • f + b • f

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
dsimp : (functor r).map ((a + b) • f) = (functor r).map (a • f) + (functor r).map (b • f)
⊢ (a + b) • (functor r).map f = a • (functor r).map f + b • (functor r).map f

Tactic:
dsimp [smul]
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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)
rw₁ rw₂ : (functor r).map (a • f) + (functor r).map (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)

Tactic:
rw [add_smul, Functor.map_add]

Premises used: CategoryTheory.Functor.map_add, add_smul
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
obtain : ∀ (f : X ⟶ Y), HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 ((functor r).map f) = 0
⊢ HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 f = 0

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
dsimp : (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 f) = 0
⊢ HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 ((functor r).map f) = 0

Tactic:
dsimp [smul]
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
rw₁ rw₂ : Eq.{v_1 + 1} (α := (functor r).obj X ⟶ (functor r).obj Y) 0 0
⊢ (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 0 f) = 0

Tactic:
rw [zero_smul, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, zero_smul
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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)
obtain : ∀ (f : X ⟶ Y), (a • (functor r).map f) ≫ g = a • (functor r).map f ≫ g
⊢ (a • f) ≫ g = a • f ≫ g

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
obtain : ∀ (g : Y ⟶ Z), (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
⊢ (a • (functor r).map f) ≫ g = a • (functor r).map f ≫ g

Tactic:
obtain ⟨g, rfl⟩ := (functor r).map_surjective g

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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)
rw₄ 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

Tactic:
rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]

Premises used: CategoryTheory.Quotient.Linear.smul_eq, CategoryTheory.Functor.map_comp, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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)
obtain : ∀ (f : X ⟶ Y), (functor r).map f ≫ (a • g) = a • (functor r).map f ≫ g
⊢ f ≫ (a • g) = a • f ≫ g

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
obtain : ∀ (g : Y ⟶ Z), (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g
⊢ (functor r).map f ≫ (a • g) = a • (functor r).map f ≫ g

Tactic:
obtain ⟨g, rfl⟩ := (functor r).map_surjective g

Premises used: CategoryTheory.Quotient.functor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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)
rw₄ rw₅ : (functor r).map (a • f ≫ 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

Tactic:
rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.comp_smul]

Premises used: CategoryTheory.Quotient.Linear.smul_eq, CategoryTheory.Linear.comp_smul, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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
⊢ Linear.{u_1, v_1, u_2} R (Quotient r)

Tactic:
exact
    { smul_comp := by
        rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ a f g
        obtain ⟨f, rfl⟩ := (functor r).map_surjective f
        obtain ⟨g, rfl⟩ := (functor r).map_surjective g
        rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]
      comp_smul := by
        rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ f a g
        obtain ⟨f, rfl⟩ := (functor r).map_surjective f
        obtain ⟨g, rfl⟩ := (functor r).map_surjective g
        rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.comp_smul] }
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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 : Linear.{u_1, v_1, u_2} R (Quotient r) := linear R r hr
⊢ Functor.Linear R (functor r)

Tactic:

Premises used: CategoryTheory.Functor.Linear.mk
-- Module: Mathlib.CategoryTheory.Quotient.Linear
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 : Linear.{u_1, v_1, u_2} R (Quotient r) := linear R r hr
⊢ Functor.Linear R (functor r)

Tactic:
exact { }
-- 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₁₂ : HomRel.CompClosure r g₁ g₂
⊢ r g₁ g₂

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_1 g : X ⟶ Y
f g₁ g₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r g₁ g₂
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_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:
hr _ _ _ _ (Congruence.equivalence.refl f) h₁₂

Premises used: Equivalence.refl, CategoryTheory.Congruence.equivalence