[GOAL]
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
a₁✝ a₂✝ : X✝ ⟶ Y✝
h :
  (CategoryTheory.Functor.mk { obj := fun R_1 => ↑R_1, map := fun {X Y} f => f.toFun }).map a₁✝ =
    (CategoryTheory.Functor.mk { obj := fun R_1 => ↑R_1, map := fun {X Y} f => f.toFun }).map a₂✝
x : ↑X✝
⊢ ↑a₁✝ x = ↑a₂✝ x
[PROOFSTEP]
dsimp at h 
[GOAL]
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : ↑a₁✝ = ↑a₂✝
x : ↑X✝
⊢ ↑a₁✝ x = ↑a₂✝ x
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ ↑f x = ↑default x
[PROOFSTEP]
rw [Subsingleton.elim x (0 : M)]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ ↑f 0 = ↑default 0
[PROOFSTEP]
dsimp
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ ↑f 0 = ↑0 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : X ⟶ M
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : X ⟶ M
x : ↑X
⊢ ↑f x = ↑default x
[PROOFSTEP]
apply Subsingleton.elim
[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 e) = 𝟙 (ModuleCat.of R X₁)
[PROOFSTEP]
ext
[GOAL]
case h
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₂
x✝ : ↑(ModuleCat.of R X₁)
⊢ ↑(↑e ≫ ↑(symm e)) x✝ = ↑(𝟙 (ModuleCat.of R X₁)) x✝
[PROOFSTEP]
apply e.left_inv
[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₂
⊢ ↑(symm e) ≫ ↑e = 𝟙 (ModuleCat.of R X₂)
[PROOFSTEP]
ext
[GOAL]
case h
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₂
x✝ : ↑(ModuleCat.of R X₂)
⊢ ↑(↑(symm e) ≫ ↑e) x✝ = ↑(𝟙 (ModuleCat.of R X₂)) x✝
[PROOFSTEP]
apply e.right_inv
[GOAL]
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
X Y : ModuleCat R
i : X ≅ Y
⊢ ∀ (x y : ↑X), ↑i.hom (x + y) = ↑i.hom x + ↑i.hom y
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
X Y : ModuleCat R
i : X ≅ Y
⊢ ∀ (r : R) (x : ↑X),
    AddHom.toFun { toFun := ↑i.hom, map_add' := (_ : ∀ (a a_1 : ↑X), ↑i.hom (a + a_1) = ↑i.hom a + ↑i.hom a_1) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := ↑i.hom, map_add' := (_ : ∀ (a a_1 : ↑X), ↑i.hom (a + a_1) = ↑i.hom a + ↑i.hom a_1) } x
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
X Y : ModuleCat R
i : X ≅ Y
x : ↑X
⊢ ↑i.inv
      (AddHom.toFun
        { toAddHom := { toFun := ↑i.hom, map_add' := (_ : ∀ (a a_1 : ↑X), ↑i.hom (a + a_1) = ↑i.hom a + ↑i.hom a_1) },
            map_smul' := (_ : ∀ (a : R) (a_1 : ↑X), ↑i.hom (a • a_1) = a • ↑i.hom a_1) }.toAddHom
        x) =
    x
[PROOFSTEP]
change (i.hom ≫ i.inv) x = x
[GOAL]
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
X Y : ModuleCat R
i : X ≅ Y
x : ↑X
⊢ ↑(i.hom ≫ i.inv) x = x
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
X Y : ModuleCat R
i : X ≅ Y
x : ↑Y
⊢ AddHom.toFun
      { toAddHom := { toFun := ↑i.hom, map_add' := (_ : ∀ (a a_1 : ↑X), ↑i.hom (a + a_1) = ↑i.hom a + ↑i.hom a_1) },
          map_smul' := (_ : ∀ (a : R) (a_1 : ↑X), ↑i.hom (a • a_1) = a • ↑i.hom a_1) }.toAddHom
      (↑i.inv x) =
    x
[PROOFSTEP]
change (i.inv ≫ i.hom) x = x
[GOAL]
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
X Y : ModuleCat R
i : X ≅ Y
x : ↑Y
⊢ ↑(i.inv ≫ i.hom) x = x
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
inst✝ : Ring R✝
X₁ X₂ : Type v
P Q R : ModuleCat R✝
f f' : P ⟶ Q
g : Q ⟶ R
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
ext
[GOAL]
case h
R✝ : Type u
inst✝ : Ring R✝
X₁ X₂ : Type v
P Q R : ModuleCat R✝
f f' : P ⟶ Q
g : Q ⟶ R
x✝ : ↑P
⊢ ↑((f + f') ≫ g) x✝ = ↑(f ≫ g + f' ≫ g) x✝
[PROOFSTEP]
dsimp
[GOAL]
case h
R✝ : Type u
inst✝ : Ring R✝
X₁ X₂ : Type v
P Q R : ModuleCat R✝
f f' : P ⟶ Q
g : Q ⟶ R
x✝ : ↑P
⊢ ↑g (↑(f + f') x✝) = ↑(f ≫ g + f' ≫ g) x✝
[PROOFSTEP]
erw [map_add]
[GOAL]
case h
R✝ : Type u
inst✝ : Ring R✝
X₁ X₂ : Type v
P Q R : ModuleCat R✝
f f' : P ⟶ Q
g : Q ⟶ R
x✝ : ↑P
⊢ ↑g (↑f x✝) + ↑g (↑f' x✝) = ↑(f ≫ g + f' ≫ g) x✝
[PROOFSTEP]
rfl
[GOAL]
R✝ : Type u
inst✝ : Ring R✝
X₁ X₂ : Type v
P Q R : ModuleCat R✝
f : P ⟶ Q
g g' : Q ⟶ R
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
ext
[GOAL]
case h
R✝ : Type u
inst✝ : Ring R✝
X₁ X₂ : Type v
P Q R : ModuleCat R✝
f : P ⟶ Q
g g' : Q ⟶ R
x✝ : ↑P
⊢ ↑(f ≫ (g + g')) x✝ = ↑(f ≫ g + f ≫ g') x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
X₁ X₂ : Type v
S : Type u
inst✝ : CommRing S
⊢ ∀ (X Y Z : ModuleCat S) (r : S) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝¹ : Ring R
X₁ X₂ : Type v
S : Type u
inst✝ : CommRing S
X✝ Y✝ Z✝ : ModuleCat S
r✝ : S
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (r✝ • f✝) ≫ g✝ = r✝ • f✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
X₁ X₂ : Type v
S : Type u
inst✝ : CommRing S
X✝ Y✝ Z✝ : ModuleCat S
r✝ : S
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ ↑((r✝ • f✝) ≫ g✝) x✝ = ↑(r✝ • f✝ ≫ g✝) x✝
[PROOFSTEP]
dsimp
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
X₁ X₂ : Type v
S : Type u
inst✝ : CommRing S
X✝ Y✝ Z✝ : ModuleCat S
r✝ : S
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ ↑g✝ (↑(r✝ • f✝) x✝) = ↑(r✝ • f✝ ≫ g✝) x✝
[PROOFSTEP]
rw [LinearMap.smul_apply, LinearMap.smul_apply, map_smul]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
X₁ X₂ : Type v
S : Type u
inst✝ : CommRing S
X✝ Y✝ Z✝ : ModuleCat S
r✝ : S
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ r✝ • ↑g✝ (↑f✝ x✝) = r✝ • ↑(f✝ ≫ g✝) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
X₁ X₂ : Type v
S : Type u
inst✝ : CommRing S
⊢ ∀ (X Y Z : ModuleCat S) (f : X ⟶ Y) (r : S) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝¹ : Ring R
X₁ X₂ : Type v
S : Type u
inst✝ : CommRing S
X✝ Y✝ Z✝ : ModuleCat S
f✝ : X✝ ⟶ Y✝
r✝ : S
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ≫ (r✝ • g✝) = r✝ • f✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
X₁ X₂ : Type v
S : Type u
inst✝ : CommRing S
X✝ Y✝ Z✝ : ModuleCat S
f✝ : X✝ ⟶ Y✝
r✝ : S
g✝ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ ↑(f✝ ≫ (r✝ • g✝)) x✝ = ↑(r✝ • f✝ ≫ g✝) x✝
[PROOFSTEP]
rfl
