[GOAL]
R : Type u
inst✝ : Ring R
⊢ ∀ (X : Type u),
    { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map (𝟙 X) =
      𝟙 ({ obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.obj X)
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : Ring R
X✝ : Type u
⊢ { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map (𝟙 X✝) =
    𝟙 ({ obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.obj X✝)
[PROOFSTEP]
exact Finsupp.lmapDomain_id _ _
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ∀ {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map (f ≫ g) =
      { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map f ≫
        { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : Ring R
X✝ Y✝ Z✝ : Type u
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map (f✝ ≫ g✝) =
    { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map f✝ ≫
      { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map g✝
[PROOFSTEP]
exact Finsupp.lmapDomain_comp _ _ _ _
[GOAL]
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
⊢ ((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom = (μ R X X').hom ≫ (free R).map (f ⊗ g)
[PROOFSTEP]
intros
  -- Porting note: broken ext
[GOAL]
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
⊢ ((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom = (μ R X X').hom ≫ (free R).map (f ⊗ g)
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
      (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom) =
    LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X')) ((μ R X X').hom ≫ (free R).map (f ⊗ g))
[PROOFSTEP]
apply Finsupp.lhom_ext'
[GOAL]
case H.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
⊢ ∀ (a : X),
    LinearMap.comp
        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
          (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom))
        (Finsupp.lsingle a) =
      LinearMap.comp
        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
          ((μ R X X').hom ≫ (free R).map (f ⊗ g)))
        (Finsupp.lsingle a)
[PROOFSTEP]
intro x
[GOAL]
case H.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
x : X
⊢ LinearMap.comp
      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
        (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom))
      (Finsupp.lsingle x) =
    LinearMap.comp
      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
        ((μ R X X').hom ≫ (free R).map (f ⊗ g)))
      (Finsupp.lsingle x)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
x : X
⊢ ↑(LinearMap.comp
          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
            (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom))
          (Finsupp.lsingle x))
      1 =
    ↑(LinearMap.comp
          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
            ((μ R X X').hom ≫ (free R).map (f ⊗ g)))
          (Finsupp.lsingle x))
      1
[PROOFSTEP]
apply Finsupp.lhom_ext'
[GOAL]
case H.h.h.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
x : X
⊢ ∀ (a : X'),
    LinearMap.comp
        (↑(LinearMap.comp
              (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
                (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom))
              (Finsupp.lsingle x))
          1)
        (Finsupp.lsingle a) =
      LinearMap.comp
        (↑(LinearMap.comp
              (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
                ((μ R X X').hom ≫ (free R).map (f ⊗ g)))
              (Finsupp.lsingle x))
          1)
        (Finsupp.lsingle a)
[PROOFSTEP]
intro x'
[GOAL]
case H.h.h.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
x : X
x' : X'
⊢ LinearMap.comp
      (↑(LinearMap.comp
            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
              (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom))
            (Finsupp.lsingle x))
        1)
      (Finsupp.lsingle x') =
    LinearMap.comp
      (↑(LinearMap.comp
            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
              ((μ R X X').hom ≫ (free R).map (f ⊗ g)))
            (Finsupp.lsingle x))
        1)
      (Finsupp.lsingle x')
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
x : X
x' : X'
⊢ ↑(LinearMap.comp
          (↑(LinearMap.comp
                (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
                  (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom))
                (Finsupp.lsingle x))
            1)
          (Finsupp.lsingle x'))
      1 =
    ↑(LinearMap.comp
          (↑(LinearMap.comp
                (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
                  ((μ R X X').hom ≫ (free R).map (f ⊗ g)))
                (Finsupp.lsingle x))
            1)
          (Finsupp.lsingle x'))
      1
[PROOFSTEP]
apply Finsupp.ext
[GOAL]
case H.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
x : X
x' : X'
⊢ ∀ (a : Y ⊗ Y'),
    ↑(↑(LinearMap.comp
                (↑(LinearMap.comp
                      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
                        (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom))
                      (Finsupp.lsingle x))
                  1)
                (Finsupp.lsingle x'))
            1)
        a =
      ↑(↑(LinearMap.comp
                (↑(LinearMap.comp
                      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
                        ((μ R X X').hom ≫ (free R).map (f ⊗ g)))
                      (Finsupp.lsingle x))
                  1)
                (Finsupp.lsingle x'))
            1)
        a
[PROOFSTEP]
intro
  ⟨y, y'⟩
    -- Porting note: used to be dsimp [μ]
[GOAL]
case H.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
x : X
x' : X'
y : Y
y' : Y'
⊢ ↑(↑(LinearMap.comp
              (↑(LinearMap.comp
                    (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
                      (((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom))
                    (Finsupp.lsingle x))
                1)
              (Finsupp.lsingle x'))
          1)
      (y, y') =
    ↑(↑(LinearMap.comp
              (↑(LinearMap.comp
                    (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj X'))
                      ((μ R X X').hom ≫ (free R).map (f ⊗ g)))
                    (Finsupp.lsingle x))
                1)
              (Finsupp.lsingle x'))
          1)
      (y, y')
[PROOFSTEP]
change
  (finsuppTensorFinsupp' R Y Y')
      (Finsupp.mapDomain f (Finsupp.single x 1) ⊗ₜ[R] Finsupp.mapDomain g (Finsupp.single x' 1)) _ =
    (Finsupp.mapDomain (f ⊗ g) (finsuppTensorFinsupp' R X X' (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single x' 1))) _
[GOAL]
case H.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y X' Y' : Type u
f : X ⟶ Y
g : X' ⟶ Y'
x : X
x' : X'
y : Y
y' : Y'
⊢ ↑(↑(finsuppTensorFinsupp' R Y Y')
          (Finsupp.mapDomain f (Finsupp.single x 1) ⊗ₜ[R] Finsupp.mapDomain g (Finsupp.single x' 1)))
      (y, y') =
    ↑(Finsupp.mapDomain (f ⊗ g) (↑(finsuppTensorFinsupp' R X X') (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single x' 1)))
      (y, y')
[PROOFSTEP]
simp_rw [Finsupp.mapDomain_single, finsuppTensorFinsupp'_single_tmul_single, mul_one, Finsupp.mapDomain_single,
  CategoryTheory.tensor_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
X : Type u
⊢ (λ_ ((free R).obj X)).hom =
    (ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom
[PROOFSTEP]
intros
  -- Porting note: broken ext
[GOAL]
R : Type u
inst✝ : CommRing R
X : Type u
⊢ (λ_ ((free R).obj X)).hom =
    (ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X : Type u
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X)) (λ_ ((free R).obj X)).hom =
    LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X))
      ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.h
R : Type u
inst✝ : CommRing R
X : Type u
⊢ ↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X)) (λ_ ((free R).obj X)).hom) 1 =
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X))
          ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom))
      1
[PROOFSTEP]
apply Finsupp.lhom_ext'
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
X : Type u
⊢ ∀ (a : X),
    LinearMap.comp (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X)) (λ_ ((free R).obj X)).hom) 1)
        (Finsupp.lsingle a) =
      LinearMap.comp
        (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X))
              ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom))
          1)
        (Finsupp.lsingle a)
[PROOFSTEP]
intro x
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x : X
⊢ LinearMap.comp (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X)) (λ_ ((free R).obj X)).hom) 1)
      (Finsupp.lsingle x) =
    LinearMap.comp
      (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X))
            ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom))
        1)
      (Finsupp.lsingle x)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x : X
⊢ ↑(LinearMap.comp (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X)) (λ_ ((free R).obj X)).hom) 1)
          (Finsupp.lsingle x))
      1 =
    ↑(LinearMap.comp
          (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X))
                ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom))
            1)
          (Finsupp.lsingle x))
      1
[PROOFSTEP]
apply Finsupp.ext
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x : X
⊢ ∀ (a : X),
    ↑(↑(LinearMap.comp
                (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X)) (λ_ ((free R).obj X)).hom) 1)
                (Finsupp.lsingle x))
            1)
        a =
      ↑(↑(LinearMap.comp
                (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X))
                      ((ε R ⊗ 𝟙 ((free R).obj X)) ≫
                        (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom))
                  1)
                (Finsupp.lsingle x))
            1)
        a
[PROOFSTEP]
intro x'
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x x' : X
⊢ ↑(↑(LinearMap.comp
              (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X)) (λ_ ((free R).obj X)).hom) 1)
              (Finsupp.lsingle x))
          1)
      x' =
    ↑(↑(LinearMap.comp
              (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X))
                    ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom))
                1)
              (Finsupp.lsingle x))
          1)
      x'
[PROOFSTEP]
let q : X →₀ R := ((λ_ (of R (X →₀ R))).hom) (1 ⊗ₜ[R] Finsupp.single x 1)
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x x' : X
q : X →₀ R := ↑(λ_ (of R (X →₀ R))).hom (1 ⊗ₜ[R] Finsupp.single x 1)
⊢ ↑(↑(LinearMap.comp
              (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X)) (λ_ ((free R).obj X)).hom) 1)
              (Finsupp.lsingle x))
          1)
      x' =
    ↑(↑(LinearMap.comp
              (↑(LinearMap.compr₂ (TensorProduct.mk R ↑tensorUnit' ↑((free R).obj X))
                    ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).toPrefunctor.obj (λ_ X).hom))
                1)
              (Finsupp.lsingle x))
          1)
      x'
[PROOFSTEP]
change
  q x' =
    Finsupp.mapDomain (λ_ X).hom
      (finsuppTensorFinsupp' R (𝟙_ (Type u)) X (Finsupp.single PUnit.unit 1 ⊗ₜ[R] Finsupp.single x 1)) x'
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x x' : X
q : X →₀ R := ↑(λ_ (of R (X →₀ R))).hom (1 ⊗ₜ[R] Finsupp.single x 1)
⊢ ↑q x' =
    ↑(Finsupp.mapDomain (λ_ X).hom
          (↑(finsuppTensorFinsupp' R (𝟙_ (Type u)) X) (Finsupp.single PUnit.unit 1 ⊗ₜ[R] Finsupp.single x 1)))
      x'
[PROOFSTEP]
simp_rw [finsuppTensorFinsupp'_single_tmul_single, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, mul_one,
  Finsupp.mapDomain_single, CategoryTheory.leftUnitor_hom_apply, one_smul]
[GOAL]
R : Type u
inst✝ : CommRing R
X : Type u
⊢ (ρ_ ((free R).obj X)).hom =
    (𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom
[PROOFSTEP]
intros
  -- Porting note: broken ext
[GOAL]
R : Type u
inst✝ : CommRing R
X : Type u
⊢ (ρ_ ((free R).obj X)).hom =
    (𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X : Type u
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit') (ρ_ ((free R).obj X)).hom =
    LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit')
      ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom)
[PROOFSTEP]
apply Finsupp.lhom_ext'
[GOAL]
case H.h
R : Type u
inst✝ : CommRing R
X : Type u
⊢ ∀ (a : X),
    LinearMap.comp (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit') (ρ_ ((free R).obj X)).hom)
        (Finsupp.lsingle a) =
      LinearMap.comp
        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit')
          ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom))
        (Finsupp.lsingle a)
[PROOFSTEP]
intro x
[GOAL]
case H.h
R : Type u
inst✝ : CommRing R
X : Type u
x : X
⊢ LinearMap.comp (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit') (ρ_ ((free R).obj X)).hom)
      (Finsupp.lsingle x) =
    LinearMap.comp
      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit')
        ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom))
      (Finsupp.lsingle x)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x : X
⊢ ↑(LinearMap.comp (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit') (ρ_ ((free R).obj X)).hom)
          (Finsupp.lsingle x))
      1 =
    ↑(LinearMap.comp
          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit')
            ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom))
          (Finsupp.lsingle x))
      1
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x : X
⊢ ↑(↑(LinearMap.comp (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit') (ρ_ ((free R).obj X)).hom)
              (Finsupp.lsingle x))
          1)
      1 =
    ↑(↑(LinearMap.comp
              (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit')
                ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom))
              (Finsupp.lsingle x))
          1)
      1
[PROOFSTEP]
apply Finsupp.ext
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x : X
⊢ ∀ (a : X),
    ↑(↑(↑(LinearMap.comp
                    (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit') (ρ_ ((free R).obj X)).hom)
                    (Finsupp.lsingle x))
                1)
            1)
        a =
      ↑(↑(↑(LinearMap.comp
                    (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit')
                      ((𝟙 ((free R).obj X) ⊗ ε R) ≫
                        (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom))
                    (Finsupp.lsingle x))
                1)
            1)
        a
[PROOFSTEP]
intro x'
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x x' : X
⊢ ↑(↑(↑(LinearMap.comp (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit') (ρ_ ((free R).obj X)).hom)
                  (Finsupp.lsingle x))
              1)
          1)
      x' =
    ↑(↑(↑(LinearMap.comp
                  (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit')
                    ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom))
                  (Finsupp.lsingle x))
              1)
          1)
      x'
[PROOFSTEP]
let q : X →₀ R := ((ρ_ (of R (X →₀ R))).hom) (Finsupp.single x 1 ⊗ₜ[R] 1)
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x x' : X
q : X →₀ R := ↑(ρ_ (of R (X →₀ R))).hom (Finsupp.single x 1 ⊗ₜ[R] 1)
⊢ ↑(↑(↑(LinearMap.comp (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit') (ρ_ ((free R).obj X)).hom)
                  (Finsupp.lsingle x))
              1)
          1)
      x' =
    ↑(↑(↑(LinearMap.comp
                  (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑tensorUnit')
                    ((𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).toPrefunctor.obj (ρ_ X).hom))
                  (Finsupp.lsingle x))
              1)
          1)
      x'
[PROOFSTEP]
change
  q x' =
    Finsupp.mapDomain (ρ_ X).hom
      (finsuppTensorFinsupp' R X (𝟙_ (Type u)) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single PUnit.unit 1)) x'
[GOAL]
case H.h.h.h.h
R : Type u
inst✝ : CommRing R
X : Type u
x x' : X
q : X →₀ R := ↑(ρ_ (of R (X →₀ R))).hom (Finsupp.single x 1 ⊗ₜ[R] 1)
⊢ ↑q x' =
    ↑(Finsupp.mapDomain (ρ_ X).hom
          (↑(finsuppTensorFinsupp' R X (𝟙_ (Type u))) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single PUnit.unit 1)))
      x'
[PROOFSTEP]
simp_rw [finsuppTensorFinsupp'_single_tmul_single, ModuleCat.MonoidalCategory.rightUnitor_hom_apply, mul_one,
  Finsupp.mapDomain_single, CategoryTheory.rightUnitor_hom_apply, one_smul]
[GOAL]
R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ ((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom =
    (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
      (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom
[PROOFSTEP]
intros
  -- Porting note: broken ext
[GOAL]
R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ ((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom =
    (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
      (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
      (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom) =
    LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
      ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
        (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H.H
R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
        (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
        ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
          (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom))
[PROOFSTEP]
apply Finsupp.lhom_ext'
[GOAL]
case H.H.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ ∀ (a : X),
    LinearMap.comp
        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
            (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
              (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
        (Finsupp.lsingle a) =
      LinearMap.comp
        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
            ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
              (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
        (Finsupp.lsingle a)
[PROOFSTEP]
intro x
[GOAL]
case H.H.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
⊢ LinearMap.comp
      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
          (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
      (Finsupp.lsingle x) =
    LinearMap.comp
      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
          ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
            (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
      (Finsupp.lsingle x)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.H.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
⊢ ↑(LinearMap.comp
          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
              (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
          (Finsupp.lsingle x))
      1 =
    ↑(LinearMap.comp
          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
              ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
          (Finsupp.lsingle x))
      1
[PROOFSTEP]
apply Finsupp.lhom_ext'
[GOAL]
case H.H.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
⊢ ∀ (a : Y),
    LinearMap.comp
        (↑(LinearMap.comp
              (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                  (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                    (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
              (Finsupp.lsingle x))
          1)
        (Finsupp.lsingle a) =
      LinearMap.comp
        (↑(LinearMap.comp
              (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                  ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                    (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
              (Finsupp.lsingle x))
          1)
        (Finsupp.lsingle a)
[PROOFSTEP]
intro y
[GOAL]
case H.H.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
y : Y
⊢ LinearMap.comp
      (↑(LinearMap.comp
            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
              (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                  (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
            (Finsupp.lsingle x))
        1)
      (Finsupp.lsingle y) =
    LinearMap.comp
      (↑(LinearMap.comp
            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
              (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                  (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
            (Finsupp.lsingle x))
        1)
      (Finsupp.lsingle y)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.H.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
y : Y
⊢ ↑(LinearMap.comp
          (↑(LinearMap.comp
                (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                  (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                    (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                      (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
                (Finsupp.lsingle x))
            1)
          (Finsupp.lsingle y))
      1 =
    ↑(LinearMap.comp
          (↑(LinearMap.comp
                (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                  (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                    ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                      (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
                (Finsupp.lsingle x))
            1)
          (Finsupp.lsingle y))
      1
[PROOFSTEP]
apply Finsupp.lhom_ext'
[GOAL]
case H.H.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
y : Y
⊢ ∀ (a : Z),
    LinearMap.comp
        (↑(LinearMap.comp
              (↑(LinearMap.comp
                    (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                        (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                          (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
                    (Finsupp.lsingle x))
                1)
              (Finsupp.lsingle y))
          1)
        (Finsupp.lsingle a) =
      LinearMap.comp
        (↑(LinearMap.comp
              (↑(LinearMap.comp
                    (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                        ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                          (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
                    (Finsupp.lsingle x))
                1)
              (Finsupp.lsingle y))
          1)
        (Finsupp.lsingle a)
[PROOFSTEP]
intro z
[GOAL]
case H.H.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
y : Y
z : Z
⊢ LinearMap.comp
      (↑(LinearMap.comp
            (↑(LinearMap.comp
                  (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                    (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                      (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                        (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
                  (Finsupp.lsingle x))
              1)
            (Finsupp.lsingle y))
        1)
      (Finsupp.lsingle z) =
    LinearMap.comp
      (↑(LinearMap.comp
            (↑(LinearMap.comp
                  (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                    (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                      ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                        (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
                  (Finsupp.lsingle x))
              1)
            (Finsupp.lsingle y))
        1)
      (Finsupp.lsingle z)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case H.H.h.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
y : Y
z : Z
⊢ ↑(LinearMap.comp
          (↑(LinearMap.comp
                (↑(LinearMap.comp
                      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                          (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                            (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
                      (Finsupp.lsingle x))
                  1)
                (Finsupp.lsingle y))
            1)
          (Finsupp.lsingle z))
      1 =
    ↑(LinearMap.comp
          (↑(LinearMap.comp
                (↑(LinearMap.comp
                      (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                        (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                          ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                            (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
                      (Finsupp.lsingle x))
                  1)
                (Finsupp.lsingle y))
            1)
          (Finsupp.lsingle z))
      1
[PROOFSTEP]
apply Finsupp.ext
[GOAL]
case H.H.h.h.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
y : Y
z : Z
⊢ ∀ (a : X ⊗ Y ⊗ Z),
    ↑(↑(LinearMap.comp
                (↑(LinearMap.comp
                      (↑(LinearMap.comp
                            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                              (LinearMap.compr₂
                                (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                                (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                                  (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
                            (Finsupp.lsingle x))
                        1)
                      (Finsupp.lsingle y))
                  1)
                (Finsupp.lsingle z))
            1)
        a =
      ↑(↑(LinearMap.comp
                (↑(LinearMap.comp
                      (↑(LinearMap.comp
                            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                              (LinearMap.compr₂
                                (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                                ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                                  (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
                            (Finsupp.lsingle x))
                        1)
                      (Finsupp.lsingle y))
                  1)
                (Finsupp.lsingle z))
            1)
        a
[PROOFSTEP]
intro a
[GOAL]
case H.H.h.h.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
y : Y
z : Z
a : X ⊗ Y ⊗ Z
⊢ ↑(↑(LinearMap.comp
              (↑(LinearMap.comp
                    (↑(LinearMap.comp
                          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                              (((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫
                                (μ R (X ⊗ Y) Z).hom ≫ map (free R).toPrefunctor.obj (α_ X Y Z).hom)))
                          (Finsupp.lsingle x))
                      1)
                    (Finsupp.lsingle y))
                1)
              (Finsupp.lsingle z))
          1)
      a =
    ↑(↑(LinearMap.comp
              (↑(LinearMap.comp
                    (↑(LinearMap.comp
                          (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X) ↑((free R).obj Y))
                            (LinearMap.compr₂ (TensorProduct.mk R ↑((free R).obj X ⊗ (free R).obj Y) ↑((free R).obj Z))
                              ((α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
                                (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom)))
                          (Finsupp.lsingle x))
                      1)
                    (Finsupp.lsingle y))
                1)
              (Finsupp.lsingle z))
          1)
      a
[PROOFSTEP]
change
  Finsupp.mapDomain (α_ X Y Z).hom
      (finsuppTensorFinsupp' R (X ⊗ Y) Z
        (finsuppTensorFinsupp' R X Y (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) ⊗ₜ[R] Finsupp.single z 1))
      a =
    finsuppTensorFinsupp' R X (Y ⊗ Z)
      (Finsupp.single x 1 ⊗ₜ[R] finsuppTensorFinsupp' R Y Z (Finsupp.single y 1 ⊗ₜ[R] Finsupp.single z 1)) a
[GOAL]
case H.H.h.h.h.h.h.h.h
R : Type u
inst✝ : CommRing R
X Y Z : Type u
x : X
y : Y
z : Z
a : X ⊗ Y ⊗ Z
⊢ ↑(Finsupp.mapDomain (α_ X Y Z).hom
          (↑(finsuppTensorFinsupp' R (X ⊗ Y) Z)
            (↑(finsuppTensorFinsupp' R X Y) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) ⊗ₜ[R] Finsupp.single z 1)))
      a =
    ↑(↑(finsuppTensorFinsupp' R X (Y ⊗ Z))
          (Finsupp.single x 1 ⊗ₜ[R] ↑(finsuppTensorFinsupp' R Y Z) (Finsupp.single y 1 ⊗ₜ[R] Finsupp.single z 1)))
      a
[PROOFSTEP]
simp_rw [finsuppTensorFinsupp'_single_tmul_single, Finsupp.mapDomain_single, mul_one,
  CategoryTheory.associator_hom_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ IsIso LaxMonoidal.ε
[PROOFSTEP]
refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ LaxMonoidal.ε ≫ Finsupp.lapply PUnit.unit = 𝟙 (𝟙_ (ModuleCat R))
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case refine'_1.h
R : Type u
inst✝ : CommRing R
⊢ ↑(LaxMonoidal.ε ≫ Finsupp.lapply PUnit.unit) 1 = ↑(𝟙 (𝟙_ (ModuleCat R))) 1
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1.h
R : Type u
inst✝ : CommRing R
⊢ ↑(ε R ≫ Finsupp.lapply PUnit.unit) 1 = ↑(𝟙 (𝟙_ (ModuleCat R))) 1
[PROOFSTEP]
erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply, Finsupp.single_eq_same, id_apply]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ Finsupp.lapply PUnit.unit ≫ LaxMonoidal.ε = 𝟙 ((free R).obj (𝟙_ (Type u)))
[PROOFSTEP]
apply Finsupp.lhom_ext'
[GOAL]
case refine'_2.h
R : Type u
inst✝ : CommRing R
⊢ ∀ (a : 𝟙_ (Type u)),
    LinearMap.comp (Finsupp.lapply PUnit.unit ≫ LaxMonoidal.ε) (Finsupp.lsingle a) =
      LinearMap.comp (𝟙 ((free R).obj (𝟙_ (Type u)))) (Finsupp.lsingle a)
[PROOFSTEP]
intro ⟨⟩
[GOAL]
case refine'_2.h
R : Type u
inst✝ : CommRing R
⊢ LinearMap.comp (Finsupp.lapply PUnit.unit ≫ LaxMonoidal.ε) (Finsupp.lsingle PUnit.unit) =
    LinearMap.comp (𝟙 ((free R).obj (𝟙_ (Type u)))) (Finsupp.lsingle PUnit.unit)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
case refine'_2.h.h
R : Type u
inst✝ : CommRing R
⊢ ↑(LinearMap.comp (Finsupp.lapply PUnit.unit ≫ LaxMonoidal.ε) (Finsupp.lsingle PUnit.unit)) 1 =
    ↑(LinearMap.comp (𝟙 ((free R).obj (𝟙_ (Type u)))) (Finsupp.lsingle PUnit.unit)) 1
[PROOFSTEP]
apply Finsupp.ext
[GOAL]
case refine'_2.h.h.h
R : Type u
inst✝ : CommRing R
⊢ ∀ (a : 𝟙_ (Type u)),
    ↑(↑(LinearMap.comp (Finsupp.lapply PUnit.unit ≫ LaxMonoidal.ε) (Finsupp.lsingle PUnit.unit)) 1) a =
      ↑(↑(LinearMap.comp (𝟙 ((free R).obj (𝟙_ (Type u)))) (Finsupp.lsingle PUnit.unit)) 1) a
[PROOFSTEP]
intro
  ⟨⟩
    -- Porting note: simp used to be able to close this goal
[GOAL]
case refine'_2.h.h.h
R : Type u
inst✝ : CommRing R
⊢ ↑(↑(LinearMap.comp (Finsupp.lapply PUnit.unit ≫ LaxMonoidal.ε) (Finsupp.lsingle PUnit.unit)) 1) PUnit.unit =
    ↑(↑(LinearMap.comp (𝟙 ((free R).obj (𝟙_ (Type u)))) (Finsupp.lsingle PUnit.unit)) 1) PUnit.unit
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.h.h.h
R : Type u
inst✝ : CommRing R
⊢ ↑(↑(Finsupp.lapply PUnit.unit ≫ ε R) (Finsupp.single PUnit.unit 1)) PUnit.unit =
    ↑(↑(𝟙 (of R (𝟙_ (Type u) →₀ R))) (Finsupp.single PUnit.unit 1)) PUnit.unit
[PROOFSTEP]
erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply, Finsupp.single_eq_same]
[GOAL]
R : Type u
inst✝ : CommRing R
src✝ : LaxMonoidalFunctor (Type u) (ModuleCat R) := LaxMonoidalFunctor.of (free R).toPrefunctor.obj
⊢ IsIso LaxMonoidal.ε
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
src✝ : LaxMonoidalFunctor (Type u) (ModuleCat R) := LaxMonoidalFunctor.of (free R).toPrefunctor.obj
X Y : Type u
⊢ IsIso (LaxMonoidalFunctor.μ (LaxMonoidalFunctor.mk src✝.toFunctor src✝.ε src✝.μ) X Y)
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝ : CommRing R
src✝ : LaxMonoidalFunctor (Type u) (ModuleCat R) := LaxMonoidalFunctor.of (free R).toPrefunctor.obj
X Y : Type u
⊢ IsIso (Free.μ R X Y).hom
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : Free R C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
dsimp
  -- This imitates the proof of associativity for `MonoidAlgebra`.
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : Free R C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ (sum (sum f fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)) fun f' s =>
      sum h fun g' t => single (f' ≫ g') (s * t)) =
    sum f fun f' s =>
      sum (sum g fun f' s => sum h fun g' t => single (f' ≫ g') (s * t)) fun g' t => single (f' ≫ g') (s * t)
[PROOFSTEP]
simp only [sum_sum_index, sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff,
  forall₃_true_iff, add_mul, mul_add, Category.assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
dsimp [CategoryTheory.categoryFree]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ (sum (f + f') fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)) =
    (sum f fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)) +
      sum f' fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)
[PROOFSTEP]
rw [Finsupp.sum_add_index']
[GOAL]
case h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y), (sum g fun g' t => single (a ≫ g') (0 * t)) = 0
[PROOFSTEP]
simp [add_mul]
[GOAL]
case h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R),
    (sum g fun g' t => single (a ≫ g') ((b₁ + b₂) * t)) =
      (sum g fun g' t => single (a ≫ g') (b₁ * t)) + sum g fun g' t => single (a ≫ g') (b₂ * t)
[PROOFSTEP]
simp [add_mul]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
dsimp [CategoryTheory.categoryFree]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (sum f fun f' s => sum (g + g') fun g' t => single (f' ≫ g') (s * t)) =
    (sum f fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)) +
      sum f fun f' s => sum g' fun g' t => single (f' ≫ g') (s * t)
[PROOFSTEP]
rw [← Finsupp.sum_add]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (sum f fun f' s => sum (g + g') fun g' t => single (f' ≫ g') (s * t)) =
    sum f fun a b => (sum g fun g' t => single (a ≫ g') (b * t)) + sum g' fun g' t => single (a ≫ g') (b * t)
[PROOFSTEP]
congr
[GOAL]
case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (fun f' s => sum (g + g') fun g' t => single (f' ≫ g') (s * t)) = fun a b =>
    (sum g fun g' t => single (a ≫ g') (b * t)) + sum g' fun g' t => single (a ≫ g') (b * t)
[PROOFSTEP]
ext r h
[GOAL]
case e_g.h.h.h
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ↑(sum (g + g') fun g' t => single (r ≫ g') (h * t)) a✝ =
    ↑((sum g fun g' t => single (r ≫ g') (h * t)) + sum g' fun g' t => single (r ≫ g') (h * t)) a✝
[PROOFSTEP]
rw [Finsupp.sum_add_index']
[GOAL]
case e_g.h.h.h.h_zero
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z), single (r ≫ a) (h * 0) = 0
[PROOFSTEP]
simp [mul_add]
[GOAL]
case e_g.h.h.h.h_add
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a✝ : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), single (r ≫ a) (h * (b₁ + b₂)) = single (r ≫ a) (h * b₁) + single (r ≫ a) (h * b₂)
[PROOFSTEP]
simp [mul_add]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g
[PROOFSTEP]
dsimp [CategoryTheory.categoryFree]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum (r • f) fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)) =
    r • sum f fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)
[PROOFSTEP]
rw [Finsupp.sum_smul_index]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum f fun i a => sum g fun g' t => single (i ≫ g') (r * a * t)) =
    r • sum f fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)
[PROOFSTEP]
simp [Finsupp.smul_sum, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (i : X ⟶ Y), (sum g fun g' t => single (i ≫ g') (0 * t)) = 0
[PROOFSTEP]
simp [Finsupp.smul_sum, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g
[PROOFSTEP]
dsimp [CategoryTheory.categoryFree]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (sum f fun f' s => sum (r • g) fun g' t => single (f' ≫ g') (s * t)) =
    r • sum f fun f' s => sum g fun g' t => single (f' ≫ g') (s * t)
[PROOFSTEP]
simp_rw [Finsupp.smul_sum]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (sum f fun f' s => sum (r • g) fun g' t => single (f' ≫ g') (s * t)) =
    sum f fun a b => sum g fun a_1 b_1 => r • single (a ≫ a_1) (b * b_1)
[PROOFSTEP]
congr
[GOAL]
case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (fun f' s => sum (r • g) fun g' t => single (f' ≫ g') (s * t)) = fun a b =>
    sum g fun a_1 b_1 => r • single (a ≫ a_1) (b * b_1)
[PROOFSTEP]
ext h s
[GOAL]
case e_g.h.h.h
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ↑(sum (r • g) fun g' t => single (h ≫ g') (s * t)) a✝ = ↑(sum g fun a b => r • single (h ≫ a) (s * b)) a✝
[PROOFSTEP]
rw [Finsupp.sum_smul_index]
[GOAL]
case e_g.h.h.h
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ↑(sum g fun i a => single (h ≫ i) (s * (r * a))) a✝ = ↑(sum g fun a b => r • single (h ≫ a) (s * b)) a✝
[PROOFSTEP]
simp [Finsupp.smul_sum, mul_left_comm]
[GOAL]
case e_g.h.h.h
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ∀ (i : Y ⟶ Z), single (h ≫ i) (s * 0) = 0
[PROOFSTEP]
simp [Finsupp.smul_sum, mul_left_comm]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ single f r ≫ single g s = single (f ≫ g) (r * s)
[PROOFSTEP]
dsimp [CategoryTheory.categoryFree]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ (sum (single f r) fun f' s_1 => sum (single g s) fun g' t => single (f' ≫ g') (s_1 * t)) = single (f ≫ g) (r * s)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun X => X, map := fun {X Y} f => single f 1 }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => single f 1 }.map f ≫
      { obj := fun X => X, map := fun {X Y} f => single f 1 }.map g
[PROOFSTEP]
dsimp only []
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ single (f ≫ g) 1 = single f 1 ≫ single g 1
[PROOFSTEP]
rw [single_comp_single, one_mul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
⊢ ∀ (X : Free R C),
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (𝟙 X) =
      𝟙 ({ obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.obj X)
[PROOFSTEP]
dsimp [CategoryTheory.categoryFree]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
⊢ ∀ (X : Free R C), (sum (single (𝟙 X) 1) fun f' r => r • F.map f') = 𝟙 (F.obj X)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
[PROOFSTEP]
apply Finsupp.induction_linear f
[GOAL]
case h0
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (0 ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map 0 ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
[PROOFSTEP]
dsimp
[GOAL]
case h0
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum (0 ≫ g) fun f' r => r • F.map f') = 0 ≫ sum g fun f' r => r • F.map f'
[PROOFSTEP]
rw [Limits.zero_comp, sum_zero_index, Limits.zero_comp]
[GOAL]
case hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (f g_1 : (X ⟶ Y) →₀ R),
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f ≫ g) =
        { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f ≫
          { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g →
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (g_1 ≫ g) =
          { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g_1 ≫
            { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g →
        { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map ((f + g_1) ≫ g) =
          { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f + g_1) ≫
            { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
[PROOFSTEP]
intro f₁ f₂ w₁ w₂
[GOAL]
case hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ :
  { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₁ ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f₁ ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
w₂ :
  { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₂ ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f₂ ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map ((f₁ + f₂) ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₁ + f₂) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
[PROOFSTEP]
rw [add_comp]
[GOAL]
case hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ :
  { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₁ ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f₁ ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
w₂ :
  { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₂ ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f₂ ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₁ ≫ g + f₂ ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₁ + f₂) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
[PROOFSTEP]
dsimp at *
[GOAL]
case hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
⊢ (sum (f₁ ≫ g + f₂ ≫ g) fun f' r => r • F.map f') =
    (sum (f₁ + f₂) fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
[PROOFSTEP]
rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
[GOAL]
case hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
⊢ ((sum (f₁ ≫ g) fun f' r => r • F.map f') + sum (f₂ ≫ g) fun f' r => r • F.map f') =
    ((sum f₁ fun f' r => r • F.map f') + sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
[PROOFSTEP]
simp only [w₁, w₂, add_comp]
[GOAL]
case hadd.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
⊢ ∀ (a : X ⟶ Y), 0 • F.map a = 0
[PROOFSTEP]
intros
[GOAL]
case hadd.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
a✝ : X ⟶ Y
⊢ 0 • F.map a✝ = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
case hadd.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
[PROOFSTEP]
intros
[GOAL]
case hadd.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
a✝ : X ⟶ Y
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • F.map a✝ = b₁✝ • F.map a✝ + b₂✝ • F.map a✝
[PROOFSTEP]
simp only [add_smul]
[GOAL]
case hadd.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0
[PROOFSTEP]
intros
[GOAL]
case hadd.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
a✝ : X ⟶ Z
⊢ 0 • F.map a✝ = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
case hadd.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
[PROOFSTEP]
intros
[GOAL]
case hadd.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r => r • F.map f') = (sum f₁ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r => r • F.map f') = (sum f₂ fun f' r => r • F.map f') ≫ sum g fun f' r => r • F.map f'
a✝ : X ⟶ Z
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • F.map a✝ = b₁✝ • F.map a✝ + b₂✝ • F.map a✝
[PROOFSTEP]
simp only [add_smul]
[GOAL]
case hsingle
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y) (b : R),
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single a b ≫ g) =
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single a b) ≫
        { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
[PROOFSTEP]
intro f' r
[GOAL]
case hsingle
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ g) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
[PROOFSTEP]
apply Finsupp.induction_linear g
[GOAL]
case hsingle.h0
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ 0) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map 0
[PROOFSTEP]
dsimp
[GOAL]
case hsingle.h0
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
⊢ (sum (single f' r ≫ 0) fun f' r => r • F.map f') = (sum (single f' r) fun f' r => r • F.map f') ≫ 0
[PROOFSTEP]
rw [Limits.comp_zero, sum_zero_index, Limits.comp_zero]
[GOAL]
case hsingle.hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
⊢ ∀ (f g : (Y ⟶ Z) →₀ R),
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ f) =
        { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
          { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f →
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ g) =
          { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
            { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g →
        { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ (f + g)) =
          { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
            { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f + g)
[PROOFSTEP]
intro f₁ f₂ w₁ w₂
[GOAL]
case hsingle.hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ f₁) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f₁
w₂ :
  { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ f₂) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f₂
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ (f₁ + f₂)) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₁ + f₂)
[PROOFSTEP]
rw [comp_add]
[GOAL]
case hsingle.hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ f₁) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f₁
w₂ :
  { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ f₂) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f₂
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map
      (single f' r ≫ f₁ + single f' r ≫ f₂) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f₁ + f₂)
[PROOFSTEP]
dsimp at *
[GOAL]
case hsingle.hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
⊢ (sum (single f' r ≫ f₁ + single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum (f₁ + f₂) fun f' r => r • F.map f'
[PROOFSTEP]
rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
[GOAL]
case hsingle.hadd
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
⊢ ((sum (single f' r ≫ f₁) fun f' r => r • F.map f') + sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ ((sum f₁ fun f' r => r • F.map f') + sum f₂ fun f' r => r • F.map f')
[PROOFSTEP]
simp only [w₁, w₂, comp_add]
[GOAL]
case hsingle.hadd.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
⊢ ∀ (a : Y ⟶ Z), 0 • F.map a = 0
[PROOFSTEP]
intros
[GOAL]
case hsingle.hadd.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
a✝ : Y ⟶ Z
⊢ 0 • F.map a✝ = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
case hsingle.hadd.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
[PROOFSTEP]
intros
[GOAL]
case hsingle.hadd.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
a✝ : Y ⟶ Z
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • F.map a✝ = b₁✝ • F.map a✝ + b₂✝ • F.map a✝
[PROOFSTEP]
simp only [add_smul]
[GOAL]
case hsingle.hadd.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0
[PROOFSTEP]
intros
[GOAL]
case hsingle.hadd.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
a✝ : X ⟶ Z
⊢ 0 • F.map a✝ = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
case hsingle.hadd.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
[PROOFSTEP]
intros
[GOAL]
case hsingle.hadd.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₁ fun f' r => r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r => r • F.map f') =
    (sum (single f' r) fun f' r => r • F.map f') ≫ sum f₂ fun f' r => r • F.map f'
a✝ : X ⟶ Z
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • F.map a✝ = b₁✝ • F.map a✝ + b₂✝ • F.map a✝
[PROOFSTEP]
simp only [add_smul]
[GOAL]
case hsingle.hsingle
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
⊢ ∀ (a : Y ⟶ Z) (b : R),
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ single a b) =
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
        { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single a b)
[PROOFSTEP]
intro g' s
[GOAL]
case hsingle.hsingle
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
g' : Y ⟶ Z
s : R
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r ≫ single g' s) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single g' s)
[PROOFSTEP]
rw [single_comp_single _ _ f' g' r s]
[GOAL]
case hsingle.hsingle
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
f' : X ⟶ Y
r : R
g' : Y ⟶ Z
s : R
⊢ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single (f' ≫ g') (r * s)) =
    { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single f' r) ≫
      { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single g' s)
[PROOFSTEP]
simp [mul_comm r s, mul_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : C
f : X ⟶ Y
r : R
⊢ (lift R F).map (single f r) = r • F.map f
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ (lift R F).map (f + g) = (lift R F).map f + (lift R F).map g
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ (sum (f + g) fun f' r => r • F.map f') = (sum f fun f' r => r • F.map f') + sum g fun f' r => r • F.map f'
[PROOFSTEP]
rw [Finsupp.sum_add_index']
[GOAL]
case h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y), 0 • F.map a = 0
[PROOFSTEP]
simp [add_smul]
[GOAL]
case h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
[PROOFSTEP]
simp [add_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (lift R F).map (r • f) = r • (lift R F).map f
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (sum (r • f) fun f' r => r • F.map f') = r • sum f fun f' r => r • F.map f'
[PROOFSTEP]
rw [Finsupp.sum_smul_index]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ (sum f fun i a => (r * a) • F.map i) = r • sum f fun f' r => r • F.map f'
[PROOFSTEP]
simp [Finsupp.smul_sum, mul_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ ∀ (i : X ⟶ Y), 0 • F.map i = 0
[PROOFSTEP]
simp [Finsupp.smul_sum, mul_smul]
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
⊢ ∀ {X Y : Free R C} (f : X ⟶ Y), F.map f ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map f
[PROOFSTEP]
intro X Y f
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
⊢ F.map f ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map f
[PROOFSTEP]
apply Finsupp.induction_linear f
[GOAL]
case h0
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
⊢ F.map 0 ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map 0
[PROOFSTEP]
rw [Functor.map_zero, Limits.zero_comp, Functor.map_zero, Limits.comp_zero]
[GOAL]
case hadd
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
⊢ ∀ (f g : (X ⟶ Y) →₀ R),
    F.map f ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map f →
      F.map g ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map g →
        F.map (f + g) ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map (f + g)
[PROOFSTEP]
intro f₁ f₂ w₁ w₂
[GOAL]
case hadd
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : F.map f₁ ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map f₁
w₂ : F.map f₂ ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map f₂
⊢ F.map (f₁ + f₂) ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map (f₁ + f₂)
[PROOFSTEP]
rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]
[GOAL]
case hsingle
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
⊢ ∀ (a : X ⟶ Y) (b : R),
    F.map (single a b) ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map (single a b)
[PROOFSTEP]
intro f' r
[GOAL]
case hsingle
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
f' : X ⟶ Y
r : R
⊢ F.map (single f' r) ≫ ((fun X => α.app X) Y).hom = ((fun X => α.app X) X).hom ≫ G.map (single f' r)
[PROOFSTEP]
rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp, comp_smul]
[GOAL]
case hsingle
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
f' : X ⟶ Y
r : R
⊢ r • F.map (single f' 1) ≫ NatTrans.app α.hom Y = r • NatTrans.app α.hom X ≫ G.map (single f' 1)
[PROOFSTEP]
change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
[GOAL]
case hsingle
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : Functor.Additive F
inst✝² : Functor.Linear R F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
f' : X ⟶ Y
r : R
⊢ r • (embedding R C ⋙ F).map f' ≫ NatTrans.app α.hom Y = r • NatTrans.app α.hom X ≫ (embedding R C ⋙ G).map f'
[PROOFSTEP]
rw [α.hom.naturality f']


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x : α
⊢ ∃ y, y ≠ x
[PROOFSTEP]
rcases exists_pair_ne α with ⟨y, y', h⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ y, y ≠ x
[PROOFSTEP]
by_cases hx : x = y
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
[PROOFSTEP]
rw [← hx] at h
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
[PROOFSTEP]
exact ⟨y', h.symm⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x
[PROOFSTEP]
exact ⟨y, Ne.symm hx⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
x : α
⊢ ∃ y, y ≠ x
[PROOFSTEP]
letI := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
x : α
this : DecidableEq α := Classical.decEq α
⊢ ∃ y, y ≠ x
[PROOFSTEP]
exact Decidable.exists_ne x
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
⊢ ∃ x y, x < y
[PROOFSTEP]
rcases exists_pair_ne α with ⟨x, y, hxy⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ x y, x < y
[PROOFSTEP]
cases lt_or_gt_of_ne hxy
[GOAL]
case intro.intro.inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : x < y
⊢ ∃ x y, x < y
[PROOFSTEP]
exact ⟨_, _, ‹_›⟩
[GOAL]
case intro.intro.inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : x > y
⊢ ∃ x y, x < y
[PROOFSTEP]
exact ⟨_, _, ‹_›⟩
[GOAL]
α : Type u_1
β : Type u_2
p : α → Prop
x : Subtype p
⊢ Nontrivial (Subtype p) ↔ ∃ y x_1, y ≠ ↑x
[PROOFSTEP]
simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne.def, Subtype.ext_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Inhabited α
h : ¬Nontrivial α
x : α
⊢ x = default
[PROOFSTEP]
by_contra H
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Inhabited α
h : ¬Nontrivial α
x : α
H : ¬x = default
⊢ False
[PROOFSTEP]
exact h ⟨_, _, H⟩
[GOAL]
α : Type u_1
β : Type u_2
⊢ Subsingleton α → ∀ (x y : α), x = y
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
h : Subsingleton α
⊢ ∀ (x y : α), x = y
[PROOFSTEP]
exact Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
⊢ ¬Nontrivial α ↔ Subsingleton α
[PROOFSTEP]
simp only [nontrivial_iff, subsingleton_iff, not_exists, Ne.def, not_not]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ Subsingleton α ∨ Nontrivial α
[PROOFSTEP]
rw [← not_nontrivial_iff_subsingleton, or_comm]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α
[PROOFSTEP]
exact Classical.em _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
⊢ Nontrivial (Option α)
[PROOFSTEP]
inhabit α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
inhabited_h : Inhabited α
⊢ Nontrivial (Option α)
[PROOFSTEP]
exact ⟨none, some default, fun.⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
⊢ Nontrivial α
[PROOFSTEP]
rcases exists_pair_ne β with ⟨x, y, h⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α
[PROOFSTEP]
rcases hf x with ⟨x', hx'⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α
[PROOFSTEP]
rcases hf y with ⟨y', hy'⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α
[PROOFSTEP]
have : x' ≠ y' := by
  refine fun H ↦ h ?_
  rw [← hx', ← hy', H]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ x' ≠ y'
[PROOFSTEP]
refine fun H ↦ h ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y
[PROOFSTEP]
rw [← hx', ← hy', H]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
this : x' ≠ y'
⊢ Nontrivial α
[PROOFSTEP]
exact ⟨⟨x', y', this⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
⊢ ∃ x, f x ≠ y
[PROOFSTEP]
rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
⊢ ∃ x, f x ≠ y
[PROOFSTEP]
by_cases h : f x₂ = y
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : f x₂ = y
⊢ ∃ x, f x ≠ y
[PROOFSTEP]
exact ⟨x₁, (hf.ne_iff' h).2 hx⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y
[PROOFSTEP]
exact ⟨x₂, h⟩
[GOAL]
α : Type u_1
β : Type u_2
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)
[PROOFSTEP]
letI := Classical.decEq (∀ i : I, f i)
[GOAL]
α : Type u_1
β : Type u_2
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)
[PROOFSTEP]
exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial