awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2
have hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
Tactic: rcases Prod.hom_ext_iff.1 hfg with ⟨hfg₁, hfg₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
⊢ IsIso f.1 ∧ IsIso f.2
have hfg₂ : (f ≫ g).2 = (𝟙 (P, S)).2
Tactic: rcases Prod.hom_ext_iff.1 hfg with ⟨hfg₁, hfg₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
hfg₂ : (f ≫ g).2 = (𝟙 (P, S)).2
⊢ IsIso f.1 ∧ IsIso f.2
have hgf₁ : (g ≫ f).1 = (𝟙 (Q, T)).1
Tactic: rcases Prod.hom_ext_iff.1 hgf with ⟨hgf₁, hgf₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
hfg₂ : (f ≫ g).2 = (𝟙 (P, S)).2
hgf₁ : (g ≫ f).1 = (𝟙 (Q, T)).1
⊢ IsIso f.1 ∧ IsIso f.2
have hgf₂ : (g ≫ f).2 = (𝟙 (Q, T)).2
Tactic: rcases Prod.hom_ext_iff.1 hgf with ⟨hgf₁, hgf₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g)
have rw : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f) ≫ (𝟙 W ×ₘ g))
Tactic: rw [← Functor.map_comp, prod_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
rw : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f) ≫ (𝟙 W ×ₘ g))
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g)
have rw₁ : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f).1 ≫ (𝟙 W ×ₘ g).1 ×ₘ (𝟙 W ×ₘ f).2 ≫ (𝟙 W ×ₘ g).2)
Tactic: rw [← Functor.map_comp, prod_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
rw : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f) ≫ (𝟙 W ×ₘ g))
rw₁ : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f).1 ≫ (𝟙 W ×ₘ g).1 ×ₘ (𝟙 W ×ₘ f).2 ≫ (𝟙 W ×ₘ g).2)
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g)
have rw₂ : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f).1 ×ₘ (𝟙 W ×ₘ f).2 ≫ (𝟙 W ×ₘ g).2)
Tactic: rw [← Functor.map_comp, prod_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W)
have rw : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W) ≫ (g ×ₘ 𝟙 W))
Tactic: rw [← Functor.map_comp, prod_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
rw : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W) ≫ (g ×ₘ 𝟙 W))
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W)
have rw₁ : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W).1 ≫ (g ×ₘ 𝟙 W).1 ×ₘ (f ×ₘ 𝟙 W).2 ≫ (g ×ₘ 𝟙 W).2)
Tactic: rw [← Functor.map_comp, prod_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
rw : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W) ≫ (g ×ₘ 𝟙 W))
rw₁ : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W).1 ≫ (g ×ₘ 𝟙 W).1 ×ₘ (f ×ₘ 𝟙 W).2 ≫ (g ×ₘ 𝟙 W).2)
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W)
have rw₂ : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W).1 ≫ (g ×ₘ 𝟙 W).1 ×ₘ (f ×ₘ 𝟙 W).2)
Tactic: rw [← Functor.map_comp, prod_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (𝟙 X ×ₘ g) ≫ F.map (f ×ₘ 𝟙 Y') = F.map (f ×ₘ g)
have rw : F.map ((𝟙 X ×ₘ g) ≫ (f ×ₘ 𝟙 Y')) = F.map (f ×ₘ g)
Tactic: rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
rw : F.map ((𝟙 X ×ₘ g) ≫ (f ×ₘ 𝟙 Y')) = F.map (f ×ₘ g)
⊢ F.map (𝟙 X ×ₘ g) ≫ F.map (f ×ₘ 𝟙 Y') = F.map (f ×ₘ g)
have rw₁ : F.map ((𝟙 X ×ₘ g).1 ≫ (f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2 ≫ (f ×ₘ 𝟙 Y').2) = F.map (f ×ₘ g)
Tactic: rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
rw : F.map ((𝟙 X ×ₘ g) ≫ (f ×ₘ 𝟙 Y')) = F.map (f ×ₘ g)
rw₁ : F.map ((𝟙 X ×ₘ g).1 ≫ (f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2 ≫ (f ×ₘ 𝟙 Y').2) = F.map (f ×ₘ g)
⊢ F.map (𝟙 X ×ₘ g) ≫ F.map (f ×ₘ 𝟙 Y') = F.map (f ×ₘ g)
have rw₂ : F.map ((f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2 ≫ (f ×ₘ 𝟙 Y').2) = F.map (f ×ₘ g)
Tactic: rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
rw : F.map ((𝟙 X ×ₘ g) ≫ (f ×ₘ 𝟙 Y')) = F.map (f ×ₘ g)
rw₁ : F.map ((𝟙 X ×ₘ g).1 ≫ (f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2 ≫ (f ×ₘ 𝟙 Y').2) = F.map (f ×ₘ g)
rw₂ : F.map ((f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2 ≫ (f ×ₘ 𝟙 Y').2) = F.map (f ×ₘ g)
⊢ F.map (𝟙 X ×ₘ g) ≫ F.map (f ×ₘ 𝟙 Y') = F.map (f ×ₘ g)
have rw₃ : F.map ((f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2) = F.map (f ×ₘ g)
Tactic: rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g)
have rw : F.map ((f ×ₘ 𝟙 Y) ≫ (𝟙 X' ×ₘ g)) = F.map (f ×ₘ g)
Tactic: rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
rw : F.map ((f ×ₘ 𝟙 Y) ≫ (𝟙 X' ×ₘ g)) = F.map (f ×ₘ g)
⊢ F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g)
have rw₁ : F.map ((f ×ₘ 𝟙 Y).1 ≫ (𝟙 X' ×ₘ g).1 ×ₘ (f ×ₘ 𝟙 Y).2 ≫ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
Tactic: rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
rw : F.map ((f ×ₘ 𝟙 Y) ≫ (𝟙 X' ×ₘ g)) = F.map (f ×ₘ g)
rw₁ : F.map ((f ×ₘ 𝟙 Y).1 ≫ (𝟙 X' ×ₘ g).1 ×ₘ (f ×ₘ 𝟙 Y).2 ≫ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
⊢ F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g)
have rw₂ : F.map ((f ×ₘ 𝟙 Y).1 ≫ (𝟙 X' ×ₘ g).1 ×ₘ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
Tactic: rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Bifunctor (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
rw : F.map ((f ×ₘ 𝟙 Y) ≫ (𝟙 X' ×ₘ g)) = F.map (f ×ₘ g)
rw₁ : F.map ((f ×ₘ 𝟙 Y).1 ≫ (𝟙 X' ×ₘ g).1 ×ₘ (f ×ₘ 𝟙 Y).2 ≫ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
rw₂ : F.map ((f ×ₘ 𝟙 Y).1 ≫ (𝟙 X' ×ₘ g).1 ×ₘ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
⊢ F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g)
have rw₃ : F.map ((f ×ₘ 𝟙 Y).1 ×ₘ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
Tactic: rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Profunctor.Basic (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X : C
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ P.map (𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g
have nth_rw : P.map (𝟙 X ≫ 𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g
Tactic: nth_rw 1 [← Category.id_comp (𝟙 X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Profunctor.Basic (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X X' X'' : C
Y : D
f : X ⟶ X'
f' : X' ⟶ X''
⊢ P.map (f ≫ f') (𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y)
have nth_rw : P.map (f ≫ f') (𝟙 Y ≫ 𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y)
Tactic: nth_rw 1 [← Category.id_comp (𝟙 Y)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Quotient.Linear (hypothesis)
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₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : HomRel.CompClosure r f₁ f₂
⊢ Eq (α := X ⟶ Y) (Quot.mk (HomRel.CompClosure r) (a • f₁)) (Quot.mk (HomRel.CompClosure r) (a • f₂))
have h₁₃ : r f₁ f₂
Tactic: simp only [HomRel.compClosure_eq_self] at h₁₂
Cleared hypotheses: h₁₂
-- 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₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
⊢ Eq (α := X ⟶ Y) (Quot.mk (HomRel.CompClosure r) (a • f₁)) (Quot.mk (HomRel.CompClosure r) (a • f₂))
have a₁ : HomRel.CompClosure r (a • f₁) (a • f₂)
Tactic: apply Quot.sound
-- 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₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
⊢ HomRel.CompClosure r (a • f₁) (a • f₂)
have a₁ : r (a • f₁) (a • f₂)
Tactic: rw [HomRel.compClosure_eq_self]
-- 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 • b • f
have obtain : ∀ (f : X ⟶ Y), (a * b) • (functor r).map f = a • 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 • b • (functor r).map f
have dsimp : (functor r).map ((a * b) • f) = (functor r).map (a • 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 • b • f)
have rw : (functor r).map (a • b • f) = (functor r).map (a • b • f)
Tactic: rw [mul_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 : (functor r).obj X ⟶ (functor r).obj Y
⊢ HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 f = f
have obtain : ∀ (f : X ⟶ Y), HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 ((functor r).map f) = (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)
f : X ⟶ Y
⊢ HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 ((functor r).map f) = (functor r).map f
have dsimp : (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 f) = (functor r).map 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)
f : X ⟶ Y
⊢ (functor r).map (HSMul.hSMul.{u_1, v_1, v_1} (α := R) 1 f) = (functor r).map f
have rw : (functor r).map f = (functor r).map f
Tactic: rw [one_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 : R
⊢ HSMul.hSMul (β := (functor r).obj X ⟶ (functor r).obj Y) a 0 = 0
have rw : HSMul.hSMul (β := (functor r).obj X ⟶ (functor r).obj Y) a ((functor r).map 0) = (functor r).map 0
Tactic: rw [← (functor r).map_zero X Y, smul_eq, smul_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)
a : R
rw : HSMul.hSMul (β := (functor r).obj X ⟶ (functor r).obj Y) a ((functor r).map 0) = (functor r).map 0
⊢ HSMul.hSMul (β := (functor r).obj X ⟶ (functor r).obj Y) a 0 = 0
have rw₁ : (functor r).map (HSMul.hSMul (β := X ⟶ Y) a 0) = (functor r).map 0
Tactic: rw [← (functor r).map_zero X Y, smul_eq, smul_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)
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
⊢ HSMul.hSMul (β := (functor r).obj X ⟶ (functor r).obj Y) a 0 = 0
have rw₂ : Eq (α := (functor r).obj X ⟶ (functor r).obj Y) ((functor r).map 0) ((functor r).map 0)
Tactic: rw [← (functor r).map_zero X Y, smul_eq, smul_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)
a : R
f g : (functor r).obj X ⟶ (functor r).obj Y
⊢ a • (f + g) = a • f + a • g
have obtain : ∀ (f : X ⟶ Y), a • ((functor r).map f + g) = a • (functor r).map f + a • 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
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
⊢ a • ((functor r).map f + g) = a • (functor r).map f + a • g
have obtain : ∀ (g : X ⟶ Y), a • ((functor r).map f + (functor r).map g) = a • (functor r).map f + a • (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
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
⊢ a • ((functor r).map f + (functor r).map g) = a • (functor r).map f + a • (functor r).map g
have dsimp : a • ((functor r).map f + (functor r).map g) = (functor r).map (a • f) + (functor r).map (a • g)
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 : R
f g : X ⟶ Y
⊢ a • ((functor r).map f + (functor r).map g) = (functor r).map (a • f) + (functor r).map (a • g)
have rw : a • (functor r).map (f + 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]
-- 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)
⊢ 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 + 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]
-- 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)
⊢ 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 + g)) = (functor r).map (a • f + a • g)
Tactic: rw [← (functor r).map_add, smul_eq, ← (functor r).map_add, smul_add]