awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • F.map (single f' 1) ≫ α.hom.app Y = r • α.hom.app X ≫ G.map (single f' 1)
have single : r • (embedding R C ⋙ F).map f' ≫ α.hom.app Y = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'
Tactic: change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • (embedding R C ⋙ F).map f' ≫ α.hom.app Y = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'
have single : r • α.hom.app X ≫ (embedding R C ⋙ G).map f' = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'
Tactic: rw [α.hom.naturality f']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
⊢ F.map f ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f
have zero : Eq (α := F.obj X ⟶ G.obj Y) (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)))
  (CategoryStruct.comp (Y := G.obj X) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X)) (G.map 0))
Tactic: induction f using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]
      | single f' r =>
        rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
          comp_smul]
        change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
        rw [α.hom.naturality f']
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
zero :
  Eq (α := F.obj X ⟶ G.obj Y)
    (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)))
    (CategoryStruct.comp (Y := G.obj X) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X)) (G.map 0))
⊢ F.map f ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f
have add : ∀ (f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R)
  (w₁ : F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
  (w₂ : F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂),
  F.map (f₁ + f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
Tactic: induction f using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]
      | single f' r =>
        rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
          comp_smul]
        change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
        rw [α.hom.naturality f']
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
zero :
  Eq (α := F.obj X ⟶ G.obj Y)
    (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)))
    (CategoryStruct.comp (Y := G.obj X) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X)) (G.map 0))
add :
  ∀ (f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R)
    (w₁ : F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
    (w₂ :
      F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂),
    F.map (f₁ + f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
      Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
⊢ F.map f ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f
have single : ∀ (f' : X ⟶ Y) (r : R),
  F.map (single f' r) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (single f' r)
Tactic: induction f using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]
      | single f' r =>
        rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
          comp_smul]
        change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
        rw [α.hom.naturality f']
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g
have _private : ∀ (hom' : (↑M : Type v) →ₗ[R] (↑N : Type v)) (h : { hom' := hom' : M.Hom N }.hom = g.hom),
  { hom' := hom' : M.Hom N } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
g : M.Hom N
hom' : (↑M : Type v) →ₗ[R] (↑N : Type v)
h : { hom' := hom' : M.Hom N }.hom = g.hom
⊢ { hom' := hom' : M.Hom N } = g
have _private : ∀ (hom'_1 : (↑M : Type v) →ₗ[R] (↑N : Type v)) (h : { hom' := hom' : M.Hom N }.hom = { hom' := hom'_1 }.hom),
  { hom' := hom' : M.Hom N } = { hom' := hom'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : ModuleCat.{u_1, u} R
f : M ⟶ X
⊢ f = default
have hf : ∀ (x : (↑M : Type u_1)),
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : ModuleCat.{u_1, u} R
f : M ⟶ X
x : (↑M : Type u_1)
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have hf : Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) 0 : (↑X : Type u_1))
  ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) 0 : (↑X : Type u_1))
Tactic: rw [Subsingleton.elim x (0 : M)]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : ModuleCat.{u_1, u} R
f : X ⟶ M
⊢ f = default
have hf : ∀ (x : (↑X : Type u_1)),
  Eq (α := (↑M : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑M : Type u_1)) x : (↑M : Type u_1))
    ((Hom.hom default : (a : (↑X : Type u_1)) → (↑M : Type u_1)) x : (↑M : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟(↑e : X₁ →ₗ[R] X₂) ≫ ↟(↑e.symm : X₂ →ₗ[R] X₁) = 𝟙 (of R X₁)
have hf : ∀ (x : (↑(of R X₁) : Type v)),
  Eq (α := (↑(of R X₁) : Type v))
    ((Hom.hom (↟(↑e : X₁ →ₗ[R] X₂) ≫ ↟(↑e.symm : X₂ →ₗ[R] X₁)) : (a : (↑(of R X₁) : Type v)) → (↑(of R X₁) : Type v))
        x :
      (↑(of R X₁) : Type v))
    ((Hom.hom (𝟙 (of R X₁)) : (a : (↑(of R X₁) : Type v)) → (↑(of R X₁) : Type v)) x : (↑(of R X₁) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟(↑e.symm : X₂ →ₗ[R] X₁) ≫ ↟(↑e : X₁ →ₗ[R] X₂) = 𝟙 (of R X₂)
have hf : ∀ (x : (↑(of R X₂) : Type v)),
  Eq (α := (↑(of R X₂) : Type v))
    ((Hom.hom (↟(↑e.symm : X₂ →ₗ[R] X₁) ≫ ↟(↑e : X₁ →ₗ[R] X₂)) : (a : (↑(of R X₂) : Type v)) → (↑(of R X₂) : Type v))
        x :
      (↑(of R X₂) : Type v))
    ((Hom.hom (𝟙 (of R X₂)) : (a : (↑(of R X₂) : Type v)) → (↑(of R X₂) : Type v)) x : (↑(of R X₂) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
h : IsZero M
⊢ Subsingleton.{v + 1} (↑M : Type v)
have refine : ∀ (x : (↑M : Type v)), x = 0
Tactic: refine subsingleton_of_forall_eq 0 (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
h : IsZero M
x : (↑M : Type v)
⊢ x = 0
have rw : Eq (α := (↑M : Type v)) ((Hom.hom (𝟙 M) : (a : (↑M : Type v)) → (↑M : Type v)) x : (↑M : Type v)) (0 : (↑M : Type v))
Tactic: rw [← LinearMap.id_apply (R := R) x, ← ModuleCat.hom_id]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M N : ModuleCat.{v, u} S
x : S₀
x_1 : S
x_2 : (↑M : Type v)
⊢ (x • x_1) • x_2 = x • x_1 • x_2
have rw : HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) x : S) (x_1 • x_2) = x • x_1 • x_2
Tactic: rw [Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M N : ModuleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
have rw : HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M N : ModuleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
rw :
  HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
have rw₁ : HMul.hMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M N : ModuleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
rw :
  HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₁ :
  HMul.hMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
have rw₂ : HMul.hMul (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) s • n =
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M N : ModuleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
rw :
  HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₁ :
  HMul.hMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₂ :
  HMul.hMul (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) s • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
have rw₃ : HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n) =
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Ring S
inst_3 : Algebra S₀ S
M_1 N_1 x M N : ModuleCat.{v, u} S
s₀ : S₀
f : x ⟶ M
g : M ⟶ N
⊢ (s₀ • f) ≫ g = s₀ • f ≫ g
have hf : ∀ (x_1 : (↑x : Type v)),
  Eq (α := (↑N : Type v)) ((Hom.hom ((s₀ • f) ≫ g) : (a : (↑x : Type v)) → (↑N : Type v)) x_1 : (↑N : Type v))
    ((Hom.hom (s₀ • f ≫ g) : (a : (↑x : Type v)) → (↑N : Type v)) x_1 : (↑N : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
r : R
⊢ HSMul.hSMul (β := (↑M : Type v)) r 0 = 0
have rw : Eq.{v + 1} (α := (↑M : Type v)) 0 0
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
r : R
x y : (↑M : Type v)
⊢ r • (x + y) = r • x + r • y
have rw : r • x + r • y = r • x + r • y
Tactic: rw [smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N : ModuleCat.{v, u} R
A : AddCommGrpCat
φ : RingHom.{u, u_1} R (End A)
x x_1 : R
x_2 : (↑(mkOfSMul' φ) : Type u_1)
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2
have simp : (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CC :=
        AddCommGrpCat.carrier)
        (HAdd.hAdd (α := End A) (β := End A) ((φ : (a : R) → End A) x : End A) ((φ : (a : R) → End A) x_1 : End A)) :
      (a : (↑A : Type u_1)) → (↑A : Type u_1))
    x_2 =
  HAdd.hAdd (α := (↑(mkOfSMul' φ) : Type u_1)) (β := (↑(mkOfSMul' φ) : Type u_1))
    ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) AddCommGrpCat.carrier _ _ A A
            ((φ : (a : R) → End A) x) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        x_2 :
      (↑A : Type u_1))
    ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) AddCommGrpCat.carrier _ _ A A
            ((φ : (a : R) → End A) x_1) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        x_2 :
      (↑A : Type u_1))
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (goal)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N A B : ModuleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      f)
⊢ IsIso (X :=
    Functor.obj
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      A)
    (CategoryTheory.Functor.map
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      f)
have change : IsIso (X :=
  Functor.obj
    (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      AddCommGrpCat.carrier))
    (Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      A))
  (CategoryTheory.Functor.map
    (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      AddCommGrpCat.carrier))
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      f))
Tactic: change IsIso ((forget _).map ((forget₂ _ AddCommGrpCat).map f))
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Basic (hypothesis)
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N A B : ModuleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      f)
⊢ IsIso f
have this : IsIso (X :=
  Functor.obj
    (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
      carrier))
    A)
  (CategoryTheory.Functor.map
    (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
      carrier))
    f)
Tactic: have : IsIso ((forget _).map f) := by
      change IsIso ((forget _).map ((forget₂ _ AddCommGrpCat).map f))
      infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Biproducts (goal)
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R ((↑M : Type v) × (↑N : Type v)),
        π :=
          {
            app := fun (j : Discrete WalkingPair) ↦
              Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                    x ⟶
                  Functor.obj (pair M N) x)
                j fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj
                      (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                      { as := x : Discrete WalkingPair } ⟶
                    Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                  j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))) (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
            naturality := ⋯ :
            NatTrans (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
              (pair M N) } :
        Cone (pair M N) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R ((↑M : Type v) × (↑N : Type v)),
                π :=
                  {
                    app := fun (j : Discrete WalkingPair) ↦
                      Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                        Functor.obj
                            (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                            x ⟶
                          Functor.obj (pair M N) x)
                        j fun (j : WalkingPair) ↦
                        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                          Functor.obj
                              (Functor.obj (Functor.const (Discrete WalkingPair))
                                (of R ((↑M : Type v) × (↑N : Type v))))
                              { as := x : Discrete WalkingPair } ⟶
                            Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                          j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v)))
                          (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
                    naturality := ⋯ :
                    NatTrans (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                      (pair M N) } :
                Cone (pair M N) }.π.app
          j =
      s.π.app j
⊢ m = ↟(LinearMap.prod (Hom.hom (s.π.app { as := WalkingPair.left })) (Hom.hom (s.π.app { as := WalkingPair.right })))
have simp_rw : m =
  ↟(LinearMap.prod (Hom.hom (m ≫ ↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))))
      (Hom.hom (m ≫ ↟(LinearMap.snd R (↑M : Type v) (↑N : Type v)))))
Tactic: simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]