[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) (x + y) =
    (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) x +
      (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) y
[PROOFSTEP]
apply (mono_iff_injective F'.m).1
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ Mono F'.m
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
        (x + y)) =
    ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) x +
        (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) y)
[PROOFSTEP]
infer_instance
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
        (x + y)) =
    ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) x +
        (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) y)
[PROOFSTEP]
rw [LinearMap.map_add]
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑F'.m
      ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
        (x + y)) =
    ↑F'.m
        ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) x) +
      ↑F'.m
        ((fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))) y)
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑(x + y)) (_ : ↑(x + y) ∈ LinearMap.range f)) =
    ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)) +
      ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x => ↑f x = ↑y) (_ : ↑y ∈ LinearMap.range f))
[PROOFSTEP]
simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↑(image f)
⊢ ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ AddHom.toFun
      {
        toFun := fun x =>
          ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
        map_add' :=
          (_ :
            ∀ (x y : ↑(image f)),
              (fun x => ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                  (x + y) =
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    x +
                  (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    y) }
      (c • x) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
          map_add' :=
            (_ :
              ∀ (x y : ↑(image f)),
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    (x + y) =
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      x +
                    (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      y) }
        x
[PROOFSTEP]
apply (mono_iff_injective F'.m).1
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ Mono F'.m
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑F'.m
      (AddHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
          map_add' :=
            (_ :
              ∀ (x y : ↑(image f)),
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    (x + y) =
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      x +
                    (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      y) }
        (c • x)) =
    ↑F'.m
      (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
            map_add' :=
              (_ :
                ∀ (x y : ↑(image f)),
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      (x + y) =
                    (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        x +
                      (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        y) }
          x)
[PROOFSTEP]
infer_instance
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑F'.m
      (AddHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
          map_add' :=
            (_ :
              ∀ (x y : ↑(image f)),
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    (x + y) =
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      x +
                    (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      y) }
        (c • x)) =
    ↑F'.m
      (↑(RingHom.id R) c •
        AddHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
            map_add' :=
              (_ :
                ∀ (x y : ↑(image f)),
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      (x + y) =
                    (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        x +
                      (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        y) }
          x)
[PROOFSTEP]
rw [LinearMap.map_smul]
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑F'.m
      (AddHom.toFun
        {
          toFun := fun x =>
            ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
          map_add' :=
            (_ :
              ∀ (x y : ↑(image f)),
                (fun x =>
                      ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                    (x + y) =
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      x +
                    (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      y) }
        (c • x)) =
    ↑(RingHom.id R) c •
      ↑F'.m
        (AddHom.toFun
          {
            toFun := fun x =>
              ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)),
            map_add' :=
              (_ :
                ∀ (x y : ↑(image f)),
                  (fun x =>
                        ↑F'.e ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                      (x + y) =
                    (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        x +
                      (fun x =>
                          ↑F'.e
                            ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)))
                        y) }
          x)
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _ • (F'.e ≫ F'.m) _
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑(c • x)) (_ : ↑(c • x) ∈ LinearMap.range f)) =
    ↑(RingHom.id R) c •
      ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f))
[PROOFSTEP]
simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
[GOAL]
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↑(image f)
⊢ ↑(c • x) = ↑(RingHom.id R) c • ↑x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑(lift F' ≫ F'.m) x = ↑(ι f) x
[PROOFSTEP]
change (F'.e ≫ F'.m) _ = _
[GOAL]
case h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => ↑f x_1 = ↑x) (_ : ↑x ∈ LinearMap.range f)) = ↑(ι f) x
[PROOFSTEP]
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
[GOAL]
case h
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = ↑(ι f) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
G✝ H✝ : ModuleCat R
f✝ : G✝ ⟶ H✝
G H : ModuleCat R
f : G ⟶ H
⊢ (imageIsoRange f).hom ≫ ofHom (Submodule.subtype (LinearMap.range f)) = Limits.image.ι f
[PROOFSTEP]
erw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]


[GOAL]
R : Type u
inst✝ : CommRing R
X✝ Y✝ : AlgebraCat 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]
intros x
[GOAL]
R : Type u
inst✝ : CommRing R
X✝ Y✝ : AlgebraCat 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✝ : CommRing R
X✝ Y✝ : AlgebraCat R
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : ↑a₁✝ = ↑a₂✝
x : ↑X✝
⊢ ↑a₁✝ x = ↑a₂✝ x
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
⊢ ∀ (X : Type u),
    { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.obj
          X)
[PROOFSTEP]
intro X
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X : Type u
⊢ { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.obj
        X)
[PROOFSTEP]
apply FreeAlgebra.hom_ext
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X : Type u
⊢ ↑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
          (𝟙 X)) ∘
      FreeAlgebra.ι R =
    ↑(𝟙
          ({ obj := fun S => mk (FreeAlgebra R S),
                map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.obj
            X)) ∘
      FreeAlgebra.ι R
[PROOFSTEP]
simp only [FreeAlgebra.ι_comp_lift]
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X : Type u
⊢ FreeAlgebra.ι R ∘ 𝟙 X = ↑(𝟙 (mk (FreeAlgebra R X))) ∘ FreeAlgebra.ι R
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
⊢ ∀ {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
        (f ≫ g) =
      { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
          f ≫
        { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
          g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
      (f✝ ≫ g✝) =
    { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map f✝ ≫
      { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map g✝
[PROOFSTEP]
apply FreeAlgebra.hom_ext
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ ↑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
          (f✝ ≫ g✝)) ∘
      FreeAlgebra.ι R =
    ↑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
            f✝ ≫
          { obj := fun S => mk (FreeAlgebra R S),
                map := fun {X Y} f => ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map
            g✝) ∘
      FreeAlgebra.ι R
[PROOFSTEP]
simp only [FreeAlgebra.ι_comp_lift]
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ FreeAlgebra.ι R ∘ (f✝ ≫ g✝) =
    ↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝) ≫ ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ FreeAlgebra.ι R
[PROOFSTEP]
ext1
  -- Porting node: this ↓ `erw` used to be handled by the `simp` below it
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X✝
⊢ (FreeAlgebra.ι R ∘ (f✝ ≫ g✝)) x✝ =
    (↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝) ≫ ↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ FreeAlgebra.ι R)
      x✝
[PROOFSTEP]
erw [CategoryTheory.coe_comp]
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X✝
⊢ (FreeAlgebra.ι R ∘ (f✝ ≫ g✝)) x✝ =
    ((↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ ↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝))) ∘
        FreeAlgebra.ι R)
      x✝
[PROOFSTEP]
simp only [CategoryTheory.coe_comp, Function.comp_apply, types_comp_apply]
  -- Porting node: this ↓ `erw` and `rfl` used to be handled by the `simp` above
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X✝
⊢ FreeAlgebra.ι R (g✝ (f✝ x✝)) =
    ↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝))
      (↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝)) (FreeAlgebra.ι R x✝))
[PROOFSTEP]
erw [FreeAlgebra.lift_ι_apply, FreeAlgebra.lift_ι_apply]
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X✝
⊢ FreeAlgebra.ι R (g✝ (f✝ x✝)) = (FreeAlgebra.ι R ∘ g✝) (f✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
⊢ ∀ {X' X : Type u} {Y : AlgebraCat R} (f : X' ⟶ X) (g : X ⟶ (forget (AlgebraCat R)).obj Y),
    ↑((fun X A => (FreeAlgebra.lift R).symm) X' Y).symm (f ≫ g) =
      (free R).map f ≫ ↑((fun X A => (FreeAlgebra.lift R).symm) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
⊢ ↑((fun X A => (FreeAlgebra.lift R).symm) X'✝ Y✝).symm (f✝ ≫ g✝) =
    (free R).map f✝ ≫ ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y✝).symm g✝
[PROOFSTEP]
apply FreeAlgebra.hom_ext
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
⊢ ↑(↑((fun X A => (FreeAlgebra.lift R).symm) X'✝ Y✝).symm (f✝ ≫ g✝)) ∘ FreeAlgebra.ι R =
    ↑((free R).map f✝ ≫ ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y✝).symm g✝) ∘ FreeAlgebra.ι R
[PROOFSTEP]
simp only [FreeAlgebra.ι_comp_lift]
[GOAL]
case w
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
⊢ ↑(↑(FreeAlgebra.lift R).symm.symm (f✝ ≫ g✝)) ∘ FreeAlgebra.ι R =
    ↑((free R).map f✝ ≫ ↑(FreeAlgebra.lift R).symm.symm g✝) ∘ FreeAlgebra.ι R
[PROOFSTEP]
ext1
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
x✝ : X'✝
⊢ (↑(↑(FreeAlgebra.lift R).symm.symm (f✝ ≫ g✝)) ∘ FreeAlgebra.ι R) x✝ =
    (↑((free R).map f✝ ≫ ↑(FreeAlgebra.lift R).symm.symm g✝) ∘ FreeAlgebra.ι R) x✝
[PROOFSTEP]
simp only [free_map, Equiv.symm_symm, FreeAlgebra.lift_ι_apply, CategoryTheory.coe_comp, Function.comp_apply,
  types_comp_apply]
  -- Porting node: this ↓ `erw` and `rfl` used to be handled by the `simp` above
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
x✝ : X'✝
⊢ ↑(↑(FreeAlgebra.lift R) (f✝ ≫ g✝)) (FreeAlgebra.ι R x✝) =
    ↑(↑(FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝) ≫ ↑(FreeAlgebra.lift R) g✝) (FreeAlgebra.ι R x✝)
[PROOFSTEP]
erw [FreeAlgebra.lift_ι_apply, CategoryTheory.comp_apply, FreeAlgebra.lift_ι_apply, Function.comp_apply,
  FreeAlgebra.lift_ι_apply]
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X'✝ X✝ : Type u
Y✝ : AlgebraCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget (AlgebraCat R)).obj Y✝
x✝ : X'✝
⊢ (f✝ ≫ g✝) x✝ = g✝ (f✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
⊢ ∀ {X : Type u} {Y Y' : AlgebraCat R} (f : (free R).obj X ⟶ Y) (g : Y ⟶ Y'),
    ↑((fun X A => (FreeAlgebra.lift R).symm) X Y') (f ≫ g) =
      ↑((fun X A => (FreeAlgebra.lift R).symm) X Y) f ≫ (forget (AlgebraCat R)).map g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ : Type u
Y✝ Y'✝ : AlgebraCat R
f✝ : (free R).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y'✝) (f✝ ≫ g✝) =
    ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y✝) f✝ ≫ (forget (AlgebraCat R)).map g✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ : Type u
Y✝ Y'✝ : AlgebraCat R
f✝ : (free R).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
a✝ : X✝
⊢ ↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y'✝) (f✝ ≫ g✝) a✝ =
    (↑((fun X A => (FreeAlgebra.lift R).symm) X✝ Y✝) f✝ ≫ (forget (AlgebraCat R)).map g✝) a✝
[PROOFSTEP]
simp only [CategoryTheory.coe_comp, Function.comp_apply, FreeAlgebra.lift_symm_apply, types_comp_apply]
  -- Porting note: proof used to be done after this ↑ `simp`; added ↓ two lines
[GOAL]
case h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ : Type u
Y✝ Y'✝ : AlgebraCat R
f✝ : (free R).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
a✝ : X✝
⊢ ↑(FreeAlgebra.lift R).symm (f✝ ≫ g✝) a✝ = (forget (AlgebraCat R)).map g✝ (↑(FreeAlgebra.lift R).symm f✝ a✝)
[PROOFSTEP]
erw [FreeAlgebra.lift_symm_apply, FreeAlgebra.lift_symm_apply]
[GOAL]
case h
R : Type u
inst✝ : CommRing R
M N U : ModuleCat R
X✝ : Type u
Y✝ Y'✝ : AlgebraCat R
f✝ : (free R).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
a✝ : X✝
⊢ (↑(f✝ ≫ g✝) ∘ FreeAlgebra.ι R) a✝ = (forget (AlgebraCat R)).map g✝ ((↑f✝ ∘ FreeAlgebra.ι R) a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
g₁ : Ring X₁
g₂ : Ring X₂
m₁ : Algebra R X₁
m₂ : Algebra R X₂
e : X₁ ≃ₐ[R] X₂
⊢ ↑e ≫ ↑(symm e) = 𝟙 (AlgebraCat.of R X₁)
[PROOFSTEP]
ext x
[GOAL]
case w
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
g₁ : Ring X₁
g₂ : Ring X₂
m₁ : Algebra R X₁
m₂ : Algebra R X₂
e : X₁ ≃ₐ[R] X₂
x : (forget (AlgebraCat R)).obj (AlgebraCat.of R X₁)
⊢ ↑(↑e ≫ ↑(symm e)) x = ↑(𝟙 (AlgebraCat.of R X₁)) x
[PROOFSTEP]
exact e.left_inv x
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
g₁ : Ring X₁
g₂ : Ring X₂
m₁ : Algebra R X₁
m₂ : Algebra R X₂
e : X₁ ≃ₐ[R] X₂
⊢ ↑(symm e) ≫ ↑e = 𝟙 (AlgebraCat.of R X₂)
[PROOFSTEP]
ext x
[GOAL]
case w
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
g₁ : Ring X₁
g₂ : Ring X₂
m₁ : Algebra R X₁
m₂ : Algebra R X₂
e : X₁ ≃ₐ[R] X₂
x : (forget (AlgebraCat R)).obj (AlgebraCat.of R X₂)
⊢ ↑(↑(symm e) ≫ ↑e) x = ↑(𝟙 (AlgebraCat.of R X₂)) x
[PROOFSTEP]
exact e.right_inv x
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑X
⊢ ↑i.inv (↑i.hom x) = x
[PROOFSTEP]
change (i.hom ≫ i.inv) x = x
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑X
⊢ ↑(i.hom ≫ i.inv) x = x
[PROOFSTEP]
simp only [hom_inv_id]
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑X
⊢ ↑(𝟙 X) x = x
[PROOFSTEP]
rw [id_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑Y
⊢ ↑i.hom (↑i.inv x) = x
[PROOFSTEP]
change (i.inv ≫ i.hom) x = x
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑Y
⊢ ↑(i.inv ≫ i.hom) x = x
[PROOFSTEP]
simp only [inv_hom_id]
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
i : X ≅ Y
x : ↑Y
⊢ ↑(𝟙 Y) x = x
[PROOFSTEP]
rw [id_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgebraCat R)).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget (AlgebraCat.{u} R)).map f)
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgebraCat R)).map f)
i : (forget (AlgebraCat R)).obj X ≅ (forget (AlgebraCat R)).obj Y := asIso ((forget (AlgebraCat R)).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃ₐ[R] Y := { f, i.toEquiv with }
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type u
X Y : AlgebraCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgebraCat R)).map f)
i : (forget (AlgebraCat R)).obj X ≅ (forget (AlgebraCat R)).obj Y := asIso ((forget (AlgebraCat R)).map f)
e : ↑X ≃ₐ[R] ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := f.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑↑f) (x * y) = OneHom.toFun (↑↑↑f) x * OneHom.toFun (↑↑↑f) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑↑f) (x + y) = OneHom.toFun (↑↑↑f) x + OneHom.toFun (↑↑↑f) y),
    commutes' := (_ : ∀ (r : R), OneHom.toFun (↑↑↑f) (↑(algebraMap R ↑X) r) = ↑(algebraMap R ↑Y) r) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toAlgebraIso).1⟩


[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))
[PROOFSTEP]
rw [huv, disjoint_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range (↑f ∘ v)))
[PROOFSTEP]
refine' Disjoint.mono_right (span_mono (range_comp_subset_range _ _)) _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range ↑f))
[PROOFSTEP]
rw [← LinearMap.range_coe, (span_eq (LinearMap.range f)), (exact_iff _ _).mp he]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (LinearMap.ker g)
[PROOFSTEP]
exact range_ker_disjoint hw
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw✝ : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
w : ι' → ↑P
hw : LinearIndependent R w
hse : ShortExact f g
⊢ LinearIndependent R (Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w))
[PROOFSTEP]
refine' linearIndependent_leftExact hv _ hse.mono hse.exact _
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw✝ : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
w : ι' → ↑P
hw : LinearIndependent R w
hse : ShortExact f g
⊢ LinearIndependent R (↑g ∘ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inr)
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw✝ : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
w : ι' → ↑P
hw : LinearIndependent R w
hse : ShortExact f g
⊢ LinearIndependent R (↑g ∘ Function.invFun ↑g ∘ w)
[PROOFSTEP]
rwa [← Function.comp.assoc,
  Function.RightInverse.comp_eq_id (Function.rightInverse_invFun ((epi_iff_surjective _).mp hse.epi)),
  Function.comp.left_id]
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw✝ : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
w : ι' → ↑P
hw : LinearIndependent R w
hse : ShortExact f g
⊢ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inl = ↑f ∘ v
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
⊢ ⊤ ≤ span R (range u)
[PROOFSTEP]
intro m _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
⊢ m ∈ span R (range u)
[PROOFSTEP]
have hgm : g m ∈ span R (range (g ∘ u ∘ Sum.inr)) := hw mem_top
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
hgm : ↑g m ∈ span R (range (↑g ∘ u ∘ Sum.inr))
⊢ m ∈ span R (range u)
[PROOFSTEP]
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hgm
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
hgm : ∃ c, (Finsupp.sum c fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
⊢ m ∈ span R (range u)
[PROOFSTEP]
obtain ⟨cm, hm⟩ := hgm
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
⊢ m ∈ span R (range u)
[PROOFSTEP]
let m' : M := Finsupp.sum cm fun j a ↦ a • (u (Sum.inr j))
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ m ∈ span R (range u)
[PROOFSTEP]
have hsub : m - m' ∈ LinearMap.range f
[GOAL]
case hsub
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ m - m' ∈ LinearMap.range f
[PROOFSTEP]
rw [(exact_iff _ _).mp he]
[GOAL]
case hsub
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ m - m' ∈ LinearMap.ker g
[PROOFSTEP]
simp only [LinearMap.mem_ker, map_sub, sub_eq_zero]
[GOAL]
case hsub
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ ↑g m = ↑g (Finsupp.sum cm fun j a => a • u (Sum.inr j))
[PROOFSTEP]
rw [← hm, map_finsupp_sum]
[GOAL]
case hsub
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = Finsupp.sum cm fun a b => ↑g (b • u (Sum.inr a))
[PROOFSTEP]
simp only [Function.comp_apply, SMulHomClass.map_smul]
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
hsub : m - m' ∈ LinearMap.range f
⊢ m ∈ span R (range u)
[PROOFSTEP]
obtain ⟨n, hnm⟩ := hsub
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
hnm : ↑f n = m - m'
⊢ m ∈ span R (range u)
[PROOFSTEP]
have hn : n ∈ span R (range v) := hv mem_top
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
hnm : ↑f n = m - m'
hn : n ∈ span R (range v)
⊢ m ∈ span R (range u)
[PROOFSTEP]
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
hnm : ↑f n = m - m'
hn : ∃ c, (Finsupp.sum c fun i a => a • v i) = n
⊢ m ∈ span R (range u)
[PROOFSTEP]
obtain ⟨cn, hn⟩ := hn
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
hnm : ↑f n = m - m'
cn : ι →₀ R
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ m ∈ span R (range u)
[PROOFSTEP]
rw [← hn, map_finsupp_sum] at hnm
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ m ∈ span R (range u)
[PROOFSTEP]
rw [← sub_add_cancel m m', ← hnm, ]
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ (Finsupp.sum cn fun a b => ↑f (b • v a)) + m' ∈ span R (range u)
[PROOFSTEP]
simp only [SMulHomClass.map_smul]
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ ((Finsupp.sum cn fun a b => b • ↑f (v a)) + Finsupp.sum cm fun j a => a • u (Sum.inr j)) ∈ span R (range u)
[PROOFSTEP]
have hn' : (Finsupp.sum cn fun a b ↦ b • f (v a)) = (Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) := by congr; ext a b;
  change b • (f ∘ v) a = _; rw [← huv]; rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
[PROOFSTEP]
congr
[GOAL]
case e_g
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ (fun a b => b • ↑f (v a)) = fun a b => b • u (Sum.inl a)
[PROOFSTEP]
ext a b
[GOAL]
case e_g.h.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
a : ι
b : R
⊢ b • ↑f (v a) = b • u (Sum.inl a)
[PROOFSTEP]
change b • (f ∘ v) a = _
[GOAL]
case e_g.h.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
a : ι
b : R
⊢ b • (↑f ∘ v) a = b • u (Sum.inl a)
[PROOFSTEP]
rw [← huv]
[GOAL]
case e_g.h.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
a : ι
b : R
⊢ b • (u ∘ Sum.inl) a = b • u (Sum.inl a)
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ ((Finsupp.sum cn fun a b => b • ↑f (v a)) + Finsupp.sum cm fun j a => a • u (Sum.inr j)) ∈ span R (range u)
[PROOFSTEP]
rw [hn']
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ ((Finsupp.sum cn fun a b => b • u (Sum.inl a)) + Finsupp.sum cm fun j a => a • u (Sum.inr j)) ∈ span R (range u)
[PROOFSTEP]
apply add_mem
[GOAL]
case intro.intro.intro.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ (Finsupp.sum cn fun a b => b • u (Sum.inl a)) ∈ span R (range u)
[PROOFSTEP]
rw [Finsupp.mem_span_range_iff_exists_finsupp]
[GOAL]
case intro.intro.intro.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ ∃ c, (Finsupp.sum c fun i a => a • u i) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
[PROOFSTEP]
use cn.mapDomain (Sum.inl)
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ (Finsupp.sum (Finsupp.mapDomain Sum.inl cn) fun i a => a • u i) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
[PROOFSTEP]
rw [Finsupp.sum_mapDomain_index_inj Sum.inl_injective]
[GOAL]
case intro.intro.intro.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ (Finsupp.sum cm fun j a => a • u (Sum.inr j)) ∈ span R (range u)
[PROOFSTEP]
rw [Finsupp.mem_span_range_iff_exists_finsupp]
[GOAL]
case intro.intro.intro.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ ∃ c, (Finsupp.sum c fun i a => a • u i) = Finsupp.sum cm fun j a => a • u (Sum.inr j)
[PROOFSTEP]
use cm.mapDomain (Sum.inr)
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ (Finsupp.sum (Finsupp.mapDomain Sum.inr cm) fun i a => a • u i) = Finsupp.sum cm fun j a => a • u (Sum.inr j)
[PROOFSTEP]
rw [Finsupp.sum_mapDomain_index_inj Sum.inr_injective]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ ⊤ ≤ span R (range (Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w)))
[PROOFSTEP]
refine' span_exact he _ hv _
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inl = ↑f ∘ v
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ ⊤ ≤ span R (range (↑g ∘ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inr))
[PROOFSTEP]
convert hw
[GOAL]
case h.e'_4.h.e'_6.h.e'_3
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ ↑g ∘ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inr = w
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
[GOAL]
case h.e'_4.h.e'_6.h.e'_3
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ ↑g ∘ Function.invFun ↑g ∘ w = w
[PROOFSTEP]
rw [ModuleCat.epi_iff_surjective] at hE
[GOAL]
case h.e'_4.h.e'_6.h.e'_3
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Function.Surjective ↑g
he : Exact f g
⊢ ↑g ∘ Function.invFun ↑g ∘ w = w
[PROOFSTEP]
rw [← Function.comp.assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE), Function.comp.left_id]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝³ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝² : Module.Free R ↑N
inst✝¹ : Module.Free R ↑P
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑M = Module.rank R ↑N + Module.rank R ↑P
[PROOFSTEP]
haveI := free_shortExact h
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝³ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝² : Module.Free R ↑N
inst✝¹ : Module.Free R ↑P
inst✝ : StrongRankCondition R
this : Module.Free R ↑M
⊢ Module.rank R ↑M = Module.rank R ↑N + Module.rank R ↑P
[PROOFSTEP]
rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R N,
  Module.Free.rank_eq_card_chooseBasisIndex R P, Cardinal.add_def, Cardinal.eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝³ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝² : Module.Free R ↑N
inst✝¹ : Module.Free R ↑P
inst✝ : StrongRankCondition R
this : Module.Free R ↑M
⊢ Nonempty (Module.Free.ChooseBasisIndex R ↑M ≃ Module.Free.ChooseBasisIndex R ↑N ⊕ Module.Free.ChooseBasisIndex R ↑P)
[PROOFSTEP]
exact
  ⟨Basis.indexEquiv (Module.Free.chooseBasis R M)
      (Basis.ofShortExact h (Module.Free.chooseBasis R N) (Module.Free.chooseBasis R P))⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝⁵ : Ring R
N P : ModuleCat R
v : ι → ↑N
n p : ℕ
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝⁴ : Module.Free R ↑N
inst✝³ : Module.Finite R ↑N
inst✝² : Module.Free R ↑P
inst✝¹ : Module.Finite R ↑P
hN : FiniteDimensional.finrank R ↑N = n
hP : FiniteDimensional.finrank R ↑P = p
inst✝ : StrongRankCondition R
⊢ FiniteDimensional.finrank R ↑M = n + p
[PROOFSTEP]
apply FiniteDimensional.finrank_eq_of_rank_eq
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝⁵ : Ring R
N P : ModuleCat R
v : ι → ↑N
n p : ℕ
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝⁴ : Module.Free R ↑N
inst✝³ : Module.Finite R ↑N
inst✝² : Module.Free R ↑P
inst✝¹ : Module.Finite R ↑P
hN : FiniteDimensional.finrank R ↑N = n
hP : FiniteDimensional.finrank R ↑P = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑M = ↑(n + p)
[PROOFSTEP]
rw [free_shortExact_rank_add h, ← hN, ← hP]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝⁵ : Ring R
N P : ModuleCat R
v : ι → ↑N
n p : ℕ
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝⁴ : Module.Free R ↑N
inst✝³ : Module.Finite R ↑N
inst✝² : Module.Free R ↑P
inst✝¹ : Module.Finite R ↑P
hN : FiniteDimensional.finrank R ↑N = n
hP : FiniteDimensional.finrank R ↑P = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑N + Module.rank R ↑P = ↑(FiniteDimensional.finrank R ↑N + FiniteDimensional.finrank R ↑P)
[PROOFSTEP]
simp only [Nat.cast_add, FiniteDimensional.finrank_eq_rank]


[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P : PresheafOfModules R
X : Cᵒᵖ
⊢ map P (𝟙 X) = id'
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P : PresheafOfModules R
X : Cᵒᵖ
x✝ : ↑(obj P X)
⊢ ↑(map P (𝟙 X)) x✝ = ↑id' x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P : PresheafOfModules R
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ map P (f ≫ g) = comp (map P g) (map P f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P : PresheafOfModules R
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
x✝ : ↑(obj P X)
⊢ ↑(map P (f ≫ g)) x✝ = ↑(comp (map P g) (map P f)) x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R✝ : Cᵒᵖ ⥤ RingCat
P Q R : PresheafOfModules R✝
f : Hom P Q
g : Hom Q R
x✝² : Cᵒᵖ
x✝¹ : ↑(R✝.obj x✝²)
x✝ : ↑(P.presheaf.obj x✝²)
⊢ ↑(NatTrans.app (f.hom ≫ g.hom) x✝²) (x✝¹ • x✝) = x✝¹ • ↑(NatTrans.app (f.hom ≫ g.hom) x✝²) x✝
[PROOFSTEP]
simp [Hom.map_smul]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
f g : P ⟶ Q
w : ∀ (X : Cᵒᵖ), app f X = app g X
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
g : P ⟶ Q
hom✝ : P.presheaf ⟶ Q.presheaf
map_smul✝ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(NatTrans.app hom✝ X) (r • x) = r • ↑(NatTrans.app hom✝ X) x
w : ∀ (X : Cᵒᵖ), app { hom := hom✝, map_smul := map_smul✝ } X = app g X
⊢ { hom := hom✝, map_smul := map_smul✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
hom✝¹ : P.presheaf ⟶ Q.presheaf
map_smul✝¹ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)),
    ↑(NatTrans.app hom✝¹ X) (r • x) = r • ↑(NatTrans.app hom✝¹ X) x
hom✝ : P.presheaf ⟶ Q.presheaf
map_smul✝ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(NatTrans.app hom✝ X) (r • x) = r • ↑(NatTrans.app hom✝ X) x
w : ∀ (X : Cᵒᵖ), app { hom := hom✝¹, map_smul := map_smul✝¹ } X = app { hom := hom✝, map_smul := map_smul✝ } X
⊢ { hom := hom✝¹, map_smul := map_smul✝¹ } = { hom := hom✝, map_smul := map_smul✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_hom
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
hom✝¹ : P.presheaf ⟶ Q.presheaf
map_smul✝¹ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)),
    ↑(NatTrans.app hom✝¹ X) (r • x) = r • ↑(NatTrans.app hom✝¹ X) x
hom✝ : P.presheaf ⟶ Q.presheaf
map_smul✝ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(NatTrans.app hom✝ X) (r • x) = r • ↑(NatTrans.app hom✝ X) x
w : ∀ (X : Cᵒᵖ), app { hom := hom✝¹, map_smul := map_smul✝¹ } X = app { hom := hom✝, map_smul := map_smul✝ } X
⊢ hom✝¹ = hom✝
[PROOFSTEP]
ext X x
[GOAL]
case mk.mk.e_hom.w.h.w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
P Q : PresheafOfModules R
hom✝¹ : P.presheaf ⟶ Q.presheaf
map_smul✝¹ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)),
    ↑(NatTrans.app hom✝¹ X) (r • x) = r • ↑(NatTrans.app hom✝¹ X) x
hom✝ : P.presheaf ⟶ Q.presheaf
map_smul✝ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(NatTrans.app hom✝ X) (r • x) = r • ↑(NatTrans.app hom✝ X) x
w : ∀ (X : Cᵒᵖ), app { hom := hom✝¹, map_smul := map_smul✝¹ } X = app { hom := hom✝, map_smul := map_smul✝ } X
X : Cᵒᵖ
x : ↑(P.presheaf.obj X)
⊢ ↑(NatTrans.app hom✝¹ X) x = ↑(NatTrans.app hom✝ X) x
[PROOFSTEP]
exact LinearMap.congr_fun (w X) x


[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
i j : ι
x : A i
y : M j
⊢ ↑(↑(smulAddMonoidHom A M) (↑(of A i) x)) (↑(of M j) y) = ↑(of M (i + j)) (GSmul.smul x y)
[PROOFSTEP]
simp [smulAddMonoidHom]
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ 1 • x = x
[PROOFSTEP]
suffices smulAddMonoidHom A M 1 = AddMonoidHom.id (⨁ i, M i) from FunLike.congr_fun this x
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ ↑(smulAddMonoidHom A M) 1 = AddMonoidHom.id (⨁ (i : ι), M i)
[PROOFSTEP]
apply DirectSum.addHom_ext
[GOAL]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ ∀ (i : ι) (y : M i),
    ↑(↑(smulAddMonoidHom A M) 1) (↑(of (fun i => M i) i) y) =
      ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) y)
[PROOFSTEP]
intro i xi
[GOAL]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(↑(smulAddMonoidHom A M) 1) (↑(of (fun i => M i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
[PROOFSTEP]
rw [show (1 : DirectSum ι fun i => A i) = (of A 0) GOne.one by rfl]
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ 1 = ↑(of A 0) GOne.one
[PROOFSTEP]
rfl
[GOAL]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(↑(smulAddMonoidHom A M) (↑(of A 0) GOne.one)) (↑(of (fun i => M i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
[PROOFSTEP]
rw [smulAddMonoidHom_apply_of_of]
[GOAL]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(of M (0 + i)) (GSmul.smul GOne.one xi) = ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
[PROOFSTEP]
exact
  DirectSum.of_eq_of_gradedMonoid_eq
    (one_smul (GradedMonoid A) <| GradedMonoid.mk i xi)
      -- Porting note: renamed to mul_smul' since DirectSum.Gmodule.mul_smul already exists
      -- Almost identical to the proof of `direct_sum.mul_assoc`
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
⊢ (a * b) • c = a • b • c
[PROOFSTEP]
suffices
  (
          -- `fun a b c ↦ (a * b) • c` as a bundled homsmulAddMonoidHom A M).compHom.comp
      (DirectSum.mulHom A) =
    (AddMonoidHom.compHom AddMonoidHom.flipHom <| (smulAddMonoidHom A M).flip.compHom.comp <| smulAddMonoidHom A M).flip
  from
  -- `fun a b c ↦ a • (b • c)` as a bundled homFunLike.congr_fun (FunLike.congr_fun (FunLike.congr_fun this a) b) c
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
⊢ comp (↑compHom (smulAddMonoidHom A M)) (mulHom A) =
    AddMonoidHom.flip
      (↑(↑compHom flipHom) (comp (↑compHom (AddMonoidHom.flip (smulAddMonoidHom A M))) (smulAddMonoidHom A M)))
[PROOFSTEP]
ext ai ax bi bx ci cx : 6
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : M ci
⊢ ↑(comp
          (↑(comp (↑(comp (comp (↑compHom (smulAddMonoidHom A M)) (mulHom A)) (of (fun i => A i) ai)) ax)
                (of (fun i => A i) bi))
            bx)
          (of (fun i => M i) ci))
      cx =
    ↑(comp
          (↑(comp
                (↑(comp
                      (AddMonoidHom.flip
                        (↑(↑compHom flipHom)
                          (comp (↑compHom (AddMonoidHom.flip (smulAddMonoidHom A M))) (smulAddMonoidHom A M))))
                      (of (fun i => A i) ai))
                  ax)
                (of (fun i => A i) bi))
            bx)
          (of (fun i => M i) ci))
      cx
[PROOFSTEP]
dsimp only [coe_comp, Function.comp_apply, compHom_apply_apply, flip_apply, flipHom_apply]
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : M ci
⊢ ↑(↑(smulAddMonoidHom A M) (↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx)))
      (↑(of (fun i => M i) ci) cx) =
    ↑(↑(smulAddMonoidHom A M) (↑(of (fun i => A i) ai) ax))
      (↑(↑(smulAddMonoidHom A M) (↑(of (fun i => A i) bi) bx)) (↑(of (fun i => M i) ci) cx))
[PROOFSTEP]
rw [smulAddMonoidHom_apply_of_of, smulAddMonoidHom_apply_of_of, DirectSum.mulHom_of_of, smulAddMonoidHom_apply_of_of]
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ι), A i
c : ⨁ (i : ι), M i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : M ci
⊢ ↑(of M (ai + bi + ci)) (GSmul.smul (GMul.mul ax bx) cx) = ↑(of M (ai + (bi + ci))) (GSmul.smul ax (GSmul.smul bx cx))
[PROOFSTEP]
exact
  DirectSum.of_eq_of_gradedMonoid_eq (mul_smul (GradedMonoid.mk ai ax) (GradedMonoid.mk bi bx) (GradedMonoid.mk ci cx))
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
r s : ⨁ (i : ι), A i
x : ⨁ (i : ι), M i
⊢ (r + s) • x = r • x + s • x
[PROOFSTEP]
simp only [smul_def, map_add, AddMonoidHom.add_apply]
[GOAL]
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ 0 • x = 0
[PROOFSTEP]
simp only [smul_def, map_zero, AddMonoidHom.zero_apply]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
⊢ Module A (⨁ (i : ι), { x // x ∈ 𝓜 i })
[PROOFSTEP]
letI := isModule 𝓐 𝓜
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
this : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
⊢ Module A (⨁ (i : ι), { x // x ∈ 𝓜 i })
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
⊢ M ≃ₗ[A] ⨁ (i : ι), { x // x ∈ 𝓜 i }
[PROOFSTEP]
letI h := isModule 𝓐 𝓜
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
⊢ M ≃ₗ[A] ⨁ (i : ι), { x // x ∈ 𝓜 i }
[PROOFSTEP]
refine
  ⟨⟨(DirectSum.decomposeAddEquiv 𝓜).toAddHom, ?_⟩, (DirectSum.decomposeAddEquiv 𝓜).symm.toFun,
    (DirectSum.decomposeAddEquiv 𝓜).left_inv, (DirectSum.decomposeAddEquiv 𝓜).right_inv⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
⊢ ∀ (r : A) (x : M),
    AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (r • x) =
      ↑(RingHom.id A) r • AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) x
[PROOFSTEP]
intro x y
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
⊢ AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (x • y) =
    ↑(RingHom.id A) x • AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) y
[PROOFSTEP]
classical
rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul, AddEquiv.coe_toAddHom,
  map_sum, Finset.sum_smul]
refine Finset.sum_congr rfl (fun i _hi => ?_)
rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum, Finset.smul_sum]
refine Finset.sum_congr rfl (fun j _hj => ?_)
rw [show
    (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
      DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i)) (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j))
    from DirectSum.Gmodule.smul_def _ _ _ _]
simp only [decomposeAddEquiv_apply, Equiv.invFun_as_coe, Equiv.symm_symm, decompose_coe,
  Gmodule.smulAddMonoidHom_apply_of_of]
convert DirectSum.decompose_coe 𝓜 _
rfl
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
⊢ AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (x • y) =
    ↑(RingHom.id A) x • AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) y
[PROOFSTEP]
rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul, AddEquiv.coe_toAddHom,
  map_sum, Finset.sum_smul]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
⊢ ∑ x_1 in DFinsupp.support (↑(decompose 𝓐) x), ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) x_1) • y) =
    ∑ i in DFinsupp.support (↑(decompose 𝓐) x), ↑(RingHom.id A) ↑(↑(↑(decompose 𝓐) x) i) • ↑(decomposeAddEquiv 𝓜) y
[PROOFSTEP]
refine Finset.sum_congr rfl (fun i _hi => ?_)
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
⊢ ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • y) =
    ↑(RingHom.id A) ↑(↑(↑(decompose 𝓐) x) i) • ↑(decomposeAddEquiv 𝓜) y
[PROOFSTEP]
rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum, Finset.smul_sum]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
⊢ ∑ x_1 in DFinsupp.support (↑(decompose 𝓜) y),
      ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) x_1)) =
    ∑ x_1 in DFinsupp.support (↑(decompose 𝓜) y),
      ↑(↑(↑(decompose 𝓐) x) i) • ↑(decomposeAddEquiv 𝓜) ↑(↑(↑(decompose 𝓜) y) x_1)
[PROOFSTEP]
refine Finset.sum_congr rfl (fun j _hj => ?_)
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
j : ι
_hj : j ∈ DFinsupp.support (↑(decompose 𝓜) y)
⊢ ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) j)) =
    ↑(↑(↑(decompose 𝓐) x) i) • ↑(decomposeAddEquiv 𝓜) ↑(↑(↑(decompose 𝓜) y) j)
[PROOFSTEP]
rw [show
    (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
      DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i)) (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j))
    from DirectSum.Gmodule.smul_def _ _ _ _]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
j : ι
_hj : j ∈ DFinsupp.support (↑(decompose 𝓜) y)
⊢ ↑(decomposeAddEquiv 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) j)) =
    ↑(↑(Gmodule.smulAddMonoidHom (fun i => { x // x ∈ 𝓐 i }) fun i => { x // x ∈ 𝓜 i })
          (↑(decompose 𝓐) ↑(↑(↑(decompose 𝓐) x) i)))
      (↑(decomposeAddEquiv 𝓜) ↑(↑(↑(decompose 𝓜) y) j))
[PROOFSTEP]
simp only [decomposeAddEquiv_apply, Equiv.invFun_as_coe, Equiv.symm_symm, decompose_coe,
  Gmodule.smulAddMonoidHom_apply_of_of]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
j : ι
_hj : j ∈ DFinsupp.support (↑(decompose 𝓜) y)
⊢ ↑(decompose 𝓜) (↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) j)) =
    ↑(of (fun i => { x // x ∈ 𝓜 i }) (i + j)) (GradedMonoid.GSmul.smul (↑(↑(decompose 𝓐) x) i) (↑(↑(decompose 𝓜) y) j))
[PROOFSTEP]
convert DirectSum.decompose_coe 𝓜 _
[GOAL]
case h.e'_2.h.e'_6
ι : Type u_1
R : Type u_2
A : Type u_3
M : Type u_4
σ : Type u_5
σ' : Type u_6
inst✝¹⁴ : AddMonoid ι
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ι → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ι → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedMonoid 𝓐
inst✝³ : SetLike.GradedSmul 𝓐 𝓜
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ι), { x // x ∈ 𝓜 i }) := isModule 𝓐 𝓜
x : A
y : M
i : ι
_hi : i ∈ DFinsupp.support (↑(decompose 𝓐) x)
j : ι
_hj : j ∈ DFinsupp.support (↑(decompose 𝓜) y)
⊢ ↑(↑(↑(decompose 𝓐) x) i) • ↑(↑(↑(decompose 𝓜) y) j) =
    ↑(GradedMonoid.GSmul.smul (↑(↑(decompose 𝓐) x) i) (↑(↑(decompose 𝓜) y) j))
[PROOFSTEP]
rfl


[GOAL]
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
⊢ Module.Projective R P ↔ Projective (of R P)
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
⊢ Projective (of R P)
[PROOFSTEP]
letI : Module.Projective R (ModuleCat.of R P) := h
[GOAL]
case refine'_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
this : Module.Projective R ↑(of R P) := h
⊢ Projective (of R P)
[PROOFSTEP]
exact ⟨fun E X epi => Module.projective_lifting_property _ _ ((ModuleCat.epi_iff_surjective _).mp epi)⟩
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
⊢ Module.Projective R P
[PROOFSTEP]
refine' Module.Projective.of_lifting_property.{u, v} _
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
⊢ ∀ {M : Type (max v u)} {N : Type (max u v)} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M]
    [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ↑f → ∃ h, comp f h = g
[PROOFSTEP]
intro E X mE mX sE sX f g s
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ↑f
⊢ ∃ h, comp f h = g
[PROOFSTEP]
haveI : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ↑f
this : Epi (↟f)
⊢ ∃ h, comp f h = g
[PROOFSTEP]
letI : Projective (ModuleCat.of R P) := h
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ↑f
this✝ : Epi (↟f)
this : Projective (of R P) := h
⊢ ∃ h, comp f h = g
[PROOFSTEP]
exact ⟨Projective.factorThru (↟g) (↟f), Projective.factorThru_comp (↟g) (↟f)⟩
[GOAL]
R : Type u
inst✝ : Ring R
M✝ M : ModuleCat R
m : ↑M
⊢ ↑(↑(Basis.constr Finsupp.basisSingleOne ℕ) _root_.id) (Finsupp.single m 1) = m
[PROOFSTEP]
dsimp [Basis.constr]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ M : ModuleCat R
m : ↑M
⊢ ↑(comp (Finsupp.total (↑M) (↑M) R _root_.id) (comp (Finsupp.lmapDomain R R _root_.id) LinearMap.id))
      (Finsupp.single m 1) =
    m
[PROOFSTEP]
simp only [Finsupp.lmapDomain_id, comp_id]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ M : ModuleCat R
m : ↑M
⊢ ↑(Finsupp.total (↑M) (↑M) R _root_.id) (Finsupp.single m 1) = m
[PROOFSTEP]
rw [Finsupp.total_single, one_smul]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ M : ModuleCat R
m : ↑M
⊢ _root_.id m = m
[PROOFSTEP]
rfl


[GOAL]
⊢ ∀ {X' X : Type u} {Y : AddCommGroupCat} (f : X' ⟶ X) (g : X ⟶ (forget AddCommGroupCat).obj Y),
    ↑((fun X G => FreeAbelianGroup.lift.symm) X' Y).symm (f ≫ g) =
      free.map f ≫ ↑((fun X G => FreeAbelianGroup.lift.symm) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
X'✝ X✝ : Type u
Y✝ : AddCommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGroupCat).obj Y✝
⊢ ↑((fun X G => FreeAbelianGroup.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝) =
    free.map f✝ ≫ ↑((fun X G => FreeAbelianGroup.lift.symm) X✝ Y✝).symm g✝
[PROOFSTEP]
ext
[GOAL]
case w
X'✝ X✝ : Type u
Y✝ : AddCommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(↑((fun X G => FreeAbelianGroup.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝)) x✝ =
    ↑(free.map f✝ ≫ ↑((fun X G => FreeAbelianGroup.lift.symm) X✝ Y✝).symm g✝) x✝
[PROOFSTEP]
simp only [Equiv.symm_symm]
[GOAL]
case w
X'✝ X✝ : Type u
Y✝ : AddCommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget AddCommGroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(↑FreeAbelianGroup.lift (f✝ ≫ g✝)) x✝ = ↑(free.map f✝ ≫ ↑FreeAbelianGroup.lift g✝) x✝
[PROOFSTEP]
apply FreeAbelianGroup.lift_comp
[GOAL]
⊢ ∀ (X : Type u),
    { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (𝟙 X) =
      𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X)
[PROOFSTEP]
intros
[GOAL]
X✝ : Type u
⊢ { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (𝟙 X✝) =
    𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
[PROOFSTEP]
ext1
[GOAL]
case w
X✝ : Type u
x✝ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
⊢ ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (𝟙 X✝)) x✝ =
    ↑(𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)) x✝
[PROOFSTEP]
rw [← FreeGroup.map.unique]
[GOAL]
case w.hg
X✝ : Type u
x✝ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
⊢ ∀ (x : X✝),
    ↑(𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)) (FreeGroup.of x) =
      FreeGroup.of (𝟙 X✝ x)
[PROOFSTEP]
intros
[GOAL]
case w.hg
X✝ : Type u
x✝¹ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
x✝ : X✝
⊢ ↑(𝟙 ({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)) (FreeGroup.of x✝) =
    FreeGroup.of (𝟙 X✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (f ≫ g) =
      { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f ≫
        { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g
[PROOFSTEP]
intros
[GOAL]
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (f✝ ≫ g✝) =
    { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f✝ ≫
      { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g✝
[PROOFSTEP]
ext1
[GOAL]
case w
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
⊢ ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map (f✝ ≫ g✝)) x✝ =
    ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f✝ ≫
          { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g✝)
      x✝
[PROOFSTEP]
rw [← FreeGroup.map.unique]
[GOAL]
case w.hg
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
⊢ ∀ (x : X✝),
    ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f✝ ≫
            { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g✝)
        (FreeGroup.of x) =
      FreeGroup.of ((f✝ ≫ g✝) x)
[PROOFSTEP]
intros
[GOAL]
case w.hg
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝¹ : ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.obj X✝)
x✝ : X✝
⊢ ↑({ obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map f✝ ≫
          { obj := fun α => of (FreeGroup α), map := fun {X Y} => FreeGroup.map }.map g✝)
      (FreeGroup.of x✝) =
    FreeGroup.of ((f✝ ≫ g✝) x✝)
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {X' X : Type u} {Y : GroupCat} (f : X' ⟶ X) (g : X ⟶ (forget GroupCat).obj Y),
    ↑((fun X G => FreeGroup.lift.symm) X' Y).symm (f ≫ g) = free.map f ≫ ↑((fun X G => FreeGroup.lift.symm) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
⊢ ↑((fun X G => FreeGroup.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝) =
    free.map f✝ ≫ ↑((fun X G => FreeGroup.lift.symm) X✝ Y✝).symm g✝
[PROOFSTEP]
ext1
[GOAL]
case w
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(↑((fun X G => FreeGroup.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝)) x✝ =
    ↑(free.map f✝ ≫ ↑((fun X G => FreeGroup.lift.symm) X✝ Y✝).symm g✝) x✝
[PROOFSTEP]
simp only [Equiv.symm_symm]
[GOAL]
case w
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(↑FreeGroup.lift (f✝ ≫ g✝)) x✝ = ↑(free.map f✝ ≫ ↑FreeGroup.lift g✝) x✝
[PROOFSTEP]
apply Eq.symm
[GOAL]
case w.h
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ↑(free.map f✝ ≫ ↑FreeGroup.lift g✝) x✝ = ↑(↑FreeGroup.lift (f✝ ≫ g✝)) x✝
[PROOFSTEP]
apply FreeGroup.lift.unique
[GOAL]
case w.h.hg
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝ : ↑(free.obj X'✝)
⊢ ∀ (x : X'✝), ↑(free.map f✝ ≫ ↑FreeGroup.lift g✝) (FreeGroup.of x) = (f✝ ≫ g✝) x
[PROOFSTEP]
intros
[GOAL]
case w.h.hg
X'✝ X✝ : Type u
Y✝ : GroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GroupCat).obj Y✝
x✝¹ : ↑(free.obj X'✝)
x✝ : X'✝
⊢ ↑(free.map f✝ ≫ ↑FreeGroup.lift g✝) (FreeGroup.of x✝) = (f✝ ≫ g✝) x✝
[PROOFSTEP]
apply FreeGroup.lift.of
[GOAL]
G : GroupCat
⊢ CommGroup (Abelianization ↑G)
[PROOFSTEP]
infer_instance
[GOAL]
X✝ Y✝ : GroupCat
f : X✝ ⟶ Y✝
⊢ (fun x => ↑Abelianization.of (↑f x)) 1 = 1
[PROOFSTEP]
simp
[GOAL]
X✝ Y✝ : GroupCat
f : X✝ ⟶ Y✝
⊢ ∀ (x y : ↑X✝),
    OneHom.toFun { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) }
        (x * y) =
      OneHom.toFun { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) } x *
        OneHom.toFun { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) } y
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (X : GroupCat),
    { obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
        (𝟙 X) =
      𝟙
        ({ obj := fun G => Bundled.mk (Abelianization ↑G),
              map := fun {X Y} f =>
                ↑Abelianization.lift
                  {
                    toOneHom :=
                      { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a a_1 : ↑X),
                          ↑Abelianization.of (↑f (a * a_1)) =
                            ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.obj
          X)
[PROOFSTEP]
intros
[GOAL]
X✝ : GroupCat
⊢ { obj := fun G => Bundled.mk (Abelianization ↑G),
          map := fun {X Y} f =>
            ↑Abelianization.lift
              {
                toOneHom :=
                  { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a a_1 : ↑X),
                      ↑Abelianization.of (↑f (a * a_1)) =
                        ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
      (𝟙 X✝) =
    𝟙
      ({ obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.obj
        X✝)
[PROOFSTEP]
simp only [MonoidHom.mk_coe, coe_id]
[GOAL]
X✝ : GroupCat
⊢ ↑Abelianization.lift
      {
        toOneHom :=
          { toFun := fun x => ↑Abelianization.of (↑(𝟙 X✝) x), map_one' := (_ : ↑Abelianization.of (↑(𝟙 X✝) 1) = 1) },
        map_mul' :=
          (_ :
            ∀ (a a_1 : ↑X✝),
              ↑Abelianization.of (↑(𝟙 X✝) (a * a_1)) =
                ↑Abelianization.of (↑(𝟙 X✝) a) * ↑Abelianization.of (↑(𝟙 X✝) a_1)) } =
    𝟙 (Bundled.mk (Abelianization ↑X✝))
[PROOFSTEP]
apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr
[GOAL]
X✝ : GroupCat
⊢ {
      toOneHom :=
        { toFun := fun x => ↑Abelianization.of (↑(𝟙 X✝) x), map_one' := (_ : ↑Abelianization.of (↑(𝟙 X✝) 1) = 1) },
      map_mul' :=
        (_ :
          ∀ (a a_1 : ↑X✝),
            ↑Abelianization.of (↑(𝟙 X✝) (a * a_1)) =
              ↑Abelianization.of (↑(𝟙 X✝) a) * ↑Abelianization.of (↑(𝟙 X✝) a_1)) } =
    ↑Abelianization.lift.symm (𝟙 (Bundled.mk (Abelianization ↑X✝)))
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {X Y Z : GroupCat} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
        (f ≫ g) =
      { obj := fun G => Bundled.mk (Abelianization ↑G),
              map := fun {X Y} f =>
                ↑Abelianization.lift
                  {
                    toOneHom :=
                      { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a a_1 : ↑X),
                          ↑Abelianization.of (↑f (a * a_1)) =
                            ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
          f ≫
        { obj := fun G => Bundled.mk (Abelianization ↑G),
              map := fun {X Y} f =>
                ↑Abelianization.lift
                  {
                    toOneHom :=
                      { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a a_1 : ↑X),
                          ↑Abelianization.of (↑f (a * a_1)) =
                            ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
          g
[PROOFSTEP]
intros
[GOAL]
X✝ Y✝ Z✝ : GroupCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun G => Bundled.mk (Abelianization ↑G),
          map := fun {X Y} f =>
            ↑Abelianization.lift
              {
                toOneHom :=
                  { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a a_1 : ↑X),
                      ↑Abelianization.of (↑f (a * a_1)) =
                        ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
      (f✝ ≫ g✝) =
    { obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
        f✝ ≫
      { obj := fun G => Bundled.mk (Abelianization ↑G),
            map := fun {X Y} f =>
              ↑Abelianization.lift
                {
                  toOneHom :=
                    { toFun := fun x => ↑Abelianization.of (↑f x), map_one' := (_ : ↑Abelianization.of (↑f 1) = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a a_1 : ↑X),
                        ↑Abelianization.of (↑f (a * a_1)) =
                          ↑Abelianization.of (↑f a) * ↑Abelianization.of (↑f a_1)) } }.map
        g✝
[PROOFSTEP]
simp only [coe_comp]
[GOAL]
X✝ Y✝ Z✝ : GroupCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ ↑Abelianization.lift
      {
        toOneHom :=
          { toFun := fun x => ↑Abelianization.of (↑(f✝ ≫ g✝) x),
            map_one' := (_ : ↑Abelianization.of (↑(f✝ ≫ g✝) 1) = 1) },
        map_mul' :=
          (_ :
            ∀ (a a_1 : ↑X✝),
              ↑Abelianization.of (↑(f✝ ≫ g✝) (a * a_1)) =
                ↑Abelianization.of (↑(f✝ ≫ g✝) a) * ↑Abelianization.of (↑(f✝ ≫ g✝) a_1)) } =
    ↑Abelianization.lift
        {
          toOneHom :=
            { toFun := fun x => ↑Abelianization.of (↑f✝ x), map_one' := (_ : ↑Abelianization.of (↑f✝ 1) = 1) },
          map_mul' :=
            (_ :
              ∀ (a a_1 : ↑X✝),
                ↑Abelianization.of (↑f✝ (a * a_1)) = ↑Abelianization.of (↑f✝ a) * ↑Abelianization.of (↑f✝ a_1)) } ≫
      ↑Abelianization.lift
        {
          toOneHom :=
            { toFun := fun x => ↑Abelianization.of (↑g✝ x), map_one' := (_ : ↑Abelianization.of (↑g✝ 1) = 1) },
          map_mul' :=
            (_ :
              ∀ (a a_1 : ↑Y✝),
                ↑Abelianization.of (↑g✝ (a * a_1)) = ↑Abelianization.of (↑g✝ a) * ↑Abelianization.of (↑g✝ a_1)) }
[PROOFSTEP]
apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr
[GOAL]
X✝ Y✝ Z✝ : GroupCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ {
      toOneHom :=
        { toFun := fun x => ↑Abelianization.of (↑(f✝ ≫ g✝) x),
          map_one' := (_ : ↑Abelianization.of (↑(f✝ ≫ g✝) 1) = 1) },
      map_mul' :=
        (_ :
          ∀ (a a_1 : ↑X✝),
            ↑Abelianization.of (↑(f✝ ≫ g✝) (a * a_1)) =
              ↑Abelianization.of (↑(f✝ ≫ g✝) a) * ↑Abelianization.of (↑(f✝ ≫ g✝) a_1)) } =
    ↑Abelianization.lift.symm
      (↑Abelianization.lift
          {
            toOneHom :=
              { toFun := fun x => ↑Abelianization.of (↑f✝ x), map_one' := (_ : ↑Abelianization.of (↑f✝ 1) = 1) },
            map_mul' :=
              (_ :
                ∀ (a a_1 : ↑X✝),
                  ↑Abelianization.of (↑f✝ (a * a_1)) = ↑Abelianization.of (↑f✝ a) * ↑Abelianization.of (↑f✝ a_1)) } ≫
        ↑Abelianization.lift
          {
            toOneHom :=
              { toFun := fun x => ↑Abelianization.of (↑g✝ x), map_one' := (_ : ↑Abelianization.of (↑g✝ 1) = 1) },
            map_mul' :=
              (_ :
                ∀ (a a_1 : ↑Y✝),
                  ↑Abelianization.of (↑g✝ (a * a_1)) = ↑Abelianization.of (↑g✝ a) * ↑Abelianization.of (↑g✝ a_1)) })
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {X' X : GroupCat} {Y : CommGroupCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ CommGroupCat GroupCat).obj Y),
    ↑((fun G A => Abelianization.lift.symm) X' Y).symm (f ≫ g) =
      abelianize.map f ≫ ↑((fun G A => Abelianization.lift.symm) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
⊢ ↑((fun G A => Abelianization.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝) =
    abelianize.map f✝ ≫ ↑((fun G A => Abelianization.lift.symm) X✝ Y✝).symm g✝
[PROOFSTEP]
ext1
[GOAL]
case w
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ↑(↑((fun G A => Abelianization.lift.symm) X'✝ Y✝).symm (f✝ ≫ g✝)) x✝ =
    ↑(abelianize.map f✝ ≫ ↑((fun G A => Abelianization.lift.symm) X✝ Y✝).symm g✝) x✝
[PROOFSTEP]
simp only [Equiv.symm_symm]
[GOAL]
case w
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ↑(↑Abelianization.lift (f✝ ≫ g✝)) x✝ = ↑(abelianize.map f✝ ≫ ↑Abelianization.lift g✝) x✝
[PROOFSTEP]
apply Eq.symm
[GOAL]
case w.h
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ↑(abelianize.map f✝ ≫ ↑Abelianization.lift g✝) x✝ = ↑(↑Abelianization.lift (f✝ ≫ g✝)) x✝
[PROOFSTEP]
apply Abelianization.lift.unique
[GOAL]
case w.h.hφ
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ∀ (x : ↑X'✝), ↑(abelianize.map f✝ ≫ ↑Abelianization.lift g✝) (↑Abelianization.of x) = ↑(f✝ ≫ g✝) x
[PROOFSTEP]
intros
[GOAL]
case w.h.hφ
X'✝ X✝ : GroupCat
Y✝ : CommGroupCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGroupCat GroupCat).obj Y✝
x✝¹ : ↑(abelianize.obj X'✝)
x✝ : ↑X'✝
⊢ ↑(abelianize.map f✝ ≫ ↑Abelianization.lift g✝) (↑Abelianization.of x✝) = ↑(f✝ ≫ g✝) x✝
[PROOFSTEP]
apply Abelianization.lift.of
[GOAL]
⊢ ∀ ⦃X Y : MonCat⦄ (f : X ⟶ Y),
    (MonCat.units ⋙ forget₂ GroupCat MonCat).map f ≫ (fun X => Units.coeHom ↑X) Y =
      (fun X => Units.coeHom ↑X) X ≫ (𝟭 MonCat).map f
[PROOFSTEP]
intros
[GOAL]
X✝ Y✝ : MonCat
f✝ : X✝ ⟶ Y✝
⊢ (MonCat.units ⋙ forget₂ GroupCat MonCat).map f✝ ≫ (fun X => Units.coeHom ↑X) Y✝ =
    (fun X => Units.coeHom ↑X) X✝ ≫ (𝟭 MonCat).map f✝
[PROOFSTEP]
exact MonoidHom.ext fun x => rfl
[GOAL]
⊢ ∀ ⦃X Y : CommMonCat⦄ (f : X ⟶ Y),
    (CommMonCat.units ⋙ forget₂ CommGroupCat CommMonCat).map f ≫ (fun X => Units.coeHom ↑X) Y =
      (fun X => Units.coeHom ↑X) X ≫ (𝟭 CommMonCat).map f
[PROOFSTEP]
intros
[GOAL]
X✝ Y✝ : CommMonCat
f✝ : X✝ ⟶ Y✝
⊢ (CommMonCat.units ⋙ forget₂ CommGroupCat CommMonCat).map f✝ ≫ (fun X => Units.coeHom ↑X) Y✝ =
    (fun X => Units.coeHom ↑X) X✝ ≫ (𝟭 CommMonCat).map f✝
[PROOFSTEP]
exact MonoidHom.ext fun x => rfl