[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Mono f
⊢ (LinearEquiv.toModuleIso'
          (LinearEquiv.trans (LinearEquiv.symm (Submodule.quotEquivOfEqBot (LinearMap.ker f) (_ : LinearMap.ker f = ⊥)))
            (LinearEquiv.trans (LinearMap.quotKerEquivRange f)
              (LinearEquiv.ofEq (LinearMap.range f) (LinearMap.ker (Submodule.mkQ (LinearMap.range f)))
                (_ : LinearMap.range f = LinearMap.ker (Submodule.mkQ (LinearMap.range f))))))).hom ≫
      Fork.ι (kernelCone (Submodule.mkQ (LinearMap.range f))) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Mono f
x✝ : ↑M
⊢ ↑((LinearEquiv.toModuleIso'
              (LinearEquiv.trans
                (LinearEquiv.symm (Submodule.quotEquivOfEqBot (LinearMap.ker f) (_ : LinearMap.ker f = ⊥)))
                (LinearEquiv.trans (LinearMap.quotKerEquivRange f)
                  (LinearEquiv.ofEq (LinearMap.range f) (LinearMap.ker (Submodule.mkQ (LinearMap.range f)))
                    (_ : LinearMap.range f = LinearMap.ker (Submodule.mkQ (LinearMap.range f))))))).hom ≫
          Fork.ι (kernelCone (Submodule.mkQ (LinearMap.range f))))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Epi f
⊢ Cofork.π (cokernelCocone (Submodule.subtype (LinearMap.ker f))) ≫
      (LinearEquiv.toModuleIso'
          (LinearEquiv.trans
            (LinearEquiv.trans
              (Submodule.quotEquivOfEq (LinearMap.range (Submodule.subtype (LinearMap.ker f))) (LinearMap.ker f)
                (_ : LinearMap.range (Submodule.subtype (LinearMap.ker f)) = LinearMap.ker f))
              (LinearMap.quotKerEquivRange f))
            (LinearEquiv.ofTop (LinearMap.range f) (_ : LinearMap.range f = ⊤)))).hom =
    f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Epi f
x✝ : ↑((parallelPair (Submodule.subtype (LinearMap.ker f)) 0).obj WalkingParallelPair.one)
⊢ ↑(Cofork.π (cokernelCocone (Submodule.subtype (LinearMap.ker f))) ≫
          (LinearEquiv.toModuleIso'
              (LinearEquiv.trans
                (LinearEquiv.trans
                  (Submodule.quotEquivOfEq (LinearMap.range (Submodule.subtype (LinearMap.ker f))) (LinearMap.ker f)
                    (_ : LinearMap.range (Submodule.subtype (LinearMap.ker f)) = LinearMap.ker f))
                  (LinearMap.quotKerEquivRange f))
                (LinearEquiv.ofTop (LinearMap.range f) (_ : LinearMap.range f = ⊤)))).hom)
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
O : ModuleCat R
g : N ⟶ O
⊢ Exact f g ↔ range f = ker g
[PROOFSTEP]
rw [abelian.exact_iff' f g (kernelIsLimit _) (cokernelIsColimit _)]
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
O : ModuleCat R
g : N ⟶ O
⊢ f ≫ g = 0 ∧ Fork.ι (kernelCone g) ≫ Cofork.π (cokernelCocone f) = 0 ↔ range f = ker g
[PROOFSTEP]
exact
  ⟨fun h => le_antisymm (range_le_ker_iff.2 h.1) (ker_le_range_iff.2 h.2), fun h =>
    ⟨range_le_ker_iff.1 <| le_of_eq h, ker_le_range_iff.1 <| le_of_eq h.symm⟩⟩


[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ natDegree 0 ≤ 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : Multiset S[X]
⊢ ∀ (a : List S[X]),
    natDegree (Multiset.sum (Quotient.mk (List.isSetoid S[X]) a)) ≤
      foldr max (_ : ∀ (a b c : ℕ), max a (max b c) = max b (max a c)) 0
        (Multiset.map natDegree (Quotient.mk (List.isSetoid S[X]) a))
[PROOFSTEP]
simpa using natDegree_list_sum_le
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
⊢ natDegree (∑ i in s, f i) ≤ Finset.fold max 0 (natDegree ∘ f) s
[PROOFSTEP]
simpa using natDegree_multiset_sum_le (s.val.map f)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ degree (List.sum l) ≤ List.maximum (List.map natDegree l)
[PROOFSTEP]
by_cases h : l.sum = 0
[GOAL]
case pos
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : List.sum l = 0
⊢ degree (List.sum l) ≤ List.maximum (List.map natDegree l)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬List.sum l = 0
⊢ degree (List.sum l) ≤ List.maximum (List.map natDegree l)
[PROOFSTEP]
rw [degree_eq_natDegree h]
[GOAL]
case neg
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬List.sum l = 0
⊢ ↑(natDegree (List.sum l)) ≤ List.maximum (List.map natDegree l)
[PROOFSTEP]
suffices (l.map natDegree).maximum = ((l.map natDegree).foldr max 0 : ℕ)
  by
  rw [this]
  simpa [this, Nat.cast_withBot] using natDegree_list_sum_le l
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬List.sum l = 0
this : List.maximum (List.map natDegree l) = ↑(List.foldr max 0 (List.map natDegree l))
⊢ ↑(natDegree (List.sum l)) ≤ List.maximum (List.map natDegree l)
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬List.sum l = 0
this : List.maximum (List.map natDegree l) = ↑(List.foldr max 0 (List.map natDegree l))
⊢ ↑(natDegree (List.sum l)) ≤ ↑(List.foldr max 0 (List.map natDegree l))
[PROOFSTEP]
simpa [this, Nat.cast_withBot] using natDegree_list_sum_le l
[GOAL]
case neg
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬List.sum l = 0
⊢ List.maximum (List.map natDegree l) = ↑(List.foldr max 0 (List.map natDegree l))
[PROOFSTEP]
rw [← List.foldr_max_of_ne_nil]
[GOAL]
case neg
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬List.sum l = 0
⊢ ↑(List.foldr max ⊥ (List.map natDegree l)) = ↑(List.foldr max 0 (List.map natDegree l))
[PROOFSTEP]
congr
[GOAL]
case neg
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬List.sum l = 0
⊢ List.map natDegree l ≠ []
[PROOFSTEP]
contrapose! h
[GOAL]
case neg
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : List.map natDegree l = []
⊢ List.sum l = 0
[PROOFSTEP]
rw [List.map_eq_nil] at h
[GOAL]
case neg
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : l = []
⊢ List.sum l = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ natDegree (List.prod l) ≤ List.sum (List.map natDegree l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
⊢ natDegree (List.prod []) ≤ List.sum (List.map natDegree [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH : natDegree (List.prod tl) ≤ List.sum (List.map natDegree tl)
⊢ natDegree (List.prod (hd :: tl)) ≤ List.sum (List.map natDegree (hd :: tl))
[PROOFSTEP]
simpa using natDegree_mul_le.trans (add_le_add_left IH _)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ degree (List.prod l) ≤ List.sum (List.map degree l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
⊢ degree (List.prod []) ≤ List.sum (List.map degree [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH : degree (List.prod tl) ≤ List.sum (List.map degree tl)
⊢ degree (List.prod (hd :: tl)) ≤ List.sum (List.map degree (hd :: tl))
[PROOFSTEP]
simpa using (degree_mul_le _ _).trans (add_le_add_left IH _)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
⊢ coeff (List.prod l) (List.length l * n) = List.prod (List.map (fun p => coeff p n) l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hl : ∀ (p : S[X]), p ∈ [] → natDegree p ≤ n
⊢ coeff (List.prod []) (List.length [] * n) = List.prod (List.map (fun p => coeff p n) [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
⊢ coeff (List.prod (hd :: tl)) (List.length (hd :: tl) * n) = List.prod (List.map (fun p => coeff p n) (hd :: tl))
[PROOFSTEP]
have hl' : ∀ p ∈ tl, natDegree p ≤ n := fun p hp => hl p (List.mem_cons_of_mem _ hp)
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (List.prod (hd :: tl)) (List.length (hd :: tl) * n) = List.prod (List.map (fun p => coeff p n) (hd :: tl))
[PROOFSTEP]
simp only [List.prod_cons, List.map, List.length]
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (hd * List.prod tl) ((List.length tl + 1) * n) = coeff hd n * List.prod (List.map (fun p => coeff p n) tl)
[PROOFSTEP]
rw [add_mul, one_mul, add_comm, ← IH hl', mul_comm tl.length]
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
[PROOFSTEP]
have h : natDegree tl.prod ≤ n * tl.length :=
  by
  refine' (natDegree_list_prod_le _).trans _
  rw [← tl.length_map natDegree, mul_comm]
  refine' List.sum_le_card_nsmul _ _ _
  simpa using hl'
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ natDegree (List.prod tl) ≤ n * List.length tl
[PROOFSTEP]
refine' (natDegree_list_prod_le _).trans _
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ List.sum (List.map natDegree tl) ≤ n * List.length tl
[PROOFSTEP]
rw [← tl.length_map natDegree, mul_comm]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ List.sum (List.map natDegree tl) ≤ List.length (List.map natDegree tl) * n
[PROOFSTEP]
refine' List.sum_le_card_nsmul _ _ _
[GOAL]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ ∀ (x : ℕ), x ∈ List.map natDegree tl → x ≤ n
[PROOFSTEP]
simpa using hl'
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
[PROOFSTEP]
have hdn : natDegree hd ≤ n := hl _ (List.mem_cons_self _ _)
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
[PROOFSTEP]
rcases hdn.eq_or_lt with (rfl | hdn')
[GOAL]
case cons.inl
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)
[PROOFSTEP]
cases' h.eq_or_lt with h' h'
[GOAL]
case cons.inl.inl
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) = natDegree hd * List.length tl
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)
[PROOFSTEP]
rw [← h', coeff_mul_degree_add_degree, leadingCoeff, leadingCoeff]
[GOAL]
case cons.inl.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) < natDegree hd * List.length tl
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt, coeff_eq_zero_of_natDegree_lt h', mul_zero]
[GOAL]
case cons.inl.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) < natDegree hd * List.length tl
⊢ natDegree (hd * List.prod tl) < natDegree hd + natDegree hd * List.length tl
[PROOFSTEP]
exact natDegree_mul_le.trans_lt (add_lt_add_left h' _)
[GOAL]
case cons.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
hdn' : natDegree hd < n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hdn', coeff_eq_zero_of_natDegree_lt, zero_mul]
[GOAL]
case cons.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
hdn' : natDegree hd < n
⊢ natDegree (hd * List.prod tl) < n + n * List.length tl
[PROOFSTEP]
exact natDegree_mul_le.trans_lt (add_lt_add_of_lt_of_le hdn' h)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ ∀ (a : List R[X]),
    natDegree (prod (Quotient.mk (List.isSetoid R[X]) a)) ≤
      Multiset.sum (Multiset.map natDegree (Quotient.mk (List.isSetoid R[X]) a))
[PROOFSTEP]
simpa using natDegree_list_prod_le
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ natDegree (∏ i in s, f i) ≤ ∑ i in s, natDegree (f i)
[PROOFSTEP]
simpa using natDegree_multiset_prod_le (s.1.map f)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ ∀ (a : List R[X]),
    degree (prod (Quotient.mk (List.isSetoid R[X]) a)) ≤
      Multiset.sum (Multiset.map degree (Quotient.mk (List.isSetoid R[X]) a))
[PROOFSTEP]
simpa using degree_list_prod_le
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ degree (∏ i in s, f i) ≤ ∑ i in s, degree (f i)
[PROOFSTEP]
simpa only [Multiset.map_map] using degree_multiset_prod_le (s.1.map f)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : prod (Multiset.map leadingCoeff t) ≠ 0
⊢ leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
[PROOFSTEP]
induction' t using Multiset.induction_on with a t ih
[GOAL]
case empty
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t) ≠ 0
h : prod (Multiset.map leadingCoeff 0) ≠ 0
⊢ leadingCoeff (prod 0) = prod (Multiset.map leadingCoeff 0)
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : prod (Multiset.map leadingCoeff (a ::ₘ t)) ≠ 0
⊢ leadingCoeff (prod (a ::ₘ t)) = prod (Multiset.map leadingCoeff (a ::ₘ t))
[PROOFSTEP]
simp only [Multiset.map_cons, Multiset.prod_cons] at h ⊢
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
⊢ leadingCoeff (a * prod t) = leadingCoeff a * prod (Multiset.map leadingCoeff t)
[PROOFSTEP]
rw [Polynomial.leadingCoeff_mul']
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
⊢ leadingCoeff a * leadingCoeff (prod t) = leadingCoeff a * prod (Multiset.map leadingCoeff t)
[PROOFSTEP]
rw [ih]
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
⊢ prod (Multiset.map leadingCoeff t) ≠ 0
[PROOFSTEP]
simp [*]
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
⊢ ¬prod (Multiset.map leadingCoeff t) = 0
[PROOFSTEP]
apply right_ne_zero_of_mul h
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
⊢ leadingCoeff a * leadingCoeff (prod t) ≠ 0
[PROOFSTEP]
rw [ih]
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
⊢ leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
⊢ prod (Multiset.map leadingCoeff t) ≠ 0
[PROOFSTEP]
simp [*]
[GOAL]
case cons
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
h✝ : prod (Multiset.map leadingCoeff t✝) ≠ 0
a : R[X]
t : Multiset R[X]
ih : prod (Multiset.map leadingCoeff t) ≠ 0 → leadingCoeff (prod t) = prod (Multiset.map leadingCoeff t)
h : leadingCoeff a * prod (Multiset.map leadingCoeff t) ≠ 0
⊢ prod (Multiset.map leadingCoeff t) ≠ 0
[PROOFSTEP]
apply right_ne_zero_of_mul h
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∏ i in s, leadingCoeff (f i) ≠ 0
⊢ leadingCoeff (∏ i in s, f i) = ∏ i in s, leadingCoeff (f i)
[PROOFSTEP]
simpa using leadingCoeff_multiset_prod' (s.1.map f) (by simpa using h)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∏ i in s, leadingCoeff (f i) ≠ 0
⊢ prod (Multiset.map leadingCoeff (Multiset.map f s.val)) ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
⊢ natDegree (prod t) = Multiset.sum (Multiset.map (fun f => natDegree f) t)
[PROOFSTEP]
revert h
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0 →
    natDegree (prod t) = Multiset.sum (Multiset.map (fun f => natDegree f) t)
[PROOFSTEP]
refine' Multiset.induction_on t _ fun a t ih ht => _
[GOAL]
case refine'_1
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ prod (Multiset.map (fun f => leadingCoeff f) 0) ≠ 0 →
    natDegree (prod 0) = Multiset.sum (Multiset.map (fun f => natDegree f) 0)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0 →
    natDegree (prod t) = Multiset.sum (Multiset.map (fun f => natDegree f) t)
ht : prod (Multiset.map (fun f => leadingCoeff f) (a ::ₘ t)) ≠ 0
⊢ natDegree (prod (a ::ₘ t)) = Multiset.sum (Multiset.map (fun f => natDegree f) (a ::ₘ t))
[PROOFSTEP]
rw [Multiset.map_cons, Multiset.prod_cons] at ht ⊢
[GOAL]
case refine'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0 →
    natDegree (prod t) = Multiset.sum (Multiset.map (fun f => natDegree f) t)
ht : leadingCoeff a * prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
⊢ natDegree (a * prod t) = Multiset.sum (natDegree a ::ₘ Multiset.map (fun f => natDegree f) t)
[PROOFSTEP]
rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]
[GOAL]
case refine'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0 →
    natDegree (prod t) = Multiset.sum (Multiset.map (fun f => natDegree f) t)
ht : leadingCoeff a * prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
[PROOFSTEP]
apply right_ne_zero_of_mul ht
[GOAL]
case refine'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0 →
    natDegree (prod t) = Multiset.sum (Multiset.map (fun f => natDegree f) t)
ht : leadingCoeff a * prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
⊢ leadingCoeff a * leadingCoeff (prod t) ≠ 0
[PROOFSTEP]
rwa [Polynomial.leadingCoeff_multiset_prod']
[GOAL]
case refine'_2.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih :
  prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0 →
    natDegree (prod t) = Multiset.sum (Multiset.map (fun f => natDegree f) t)
ht : leadingCoeff a * prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
⊢ prod (Multiset.map leadingCoeff t) ≠ 0
[PROOFSTEP]
apply right_ne_zero_of_mul ht
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∏ i in s, leadingCoeff (f i) ≠ 0
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
[PROOFSTEP]
simpa using natDegree_multiset_prod' (s.1.map f) (by simpa using h)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∏ i in s, leadingCoeff (f i) ≠ 0
⊢ prod (Multiset.map (fun f => leadingCoeff f) (Multiset.map f s.val)) ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
⊢ natDegree (prod t) = Multiset.sum (Multiset.map natDegree t)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ natDegree (prod t) = Multiset.sum (Multiset.map natDegree t)
[PROOFSTEP]
apply natDegree_multiset_prod'
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
[PROOFSTEP]
suffices (t.map fun f => leadingCoeff f).prod = 1 by
  rw [this]
  simp
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
this : prod (Multiset.map (fun f => leadingCoeff f) t) = 1
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
this : prod (Multiset.map (fun f => leadingCoeff f) t) = 1
⊢ 1 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) = 1
[PROOFSTEP]
convert prod_replicate (Multiset.card t) (1 : R)
[GOAL]
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ Multiset.map (fun f => leadingCoeff f) t = replicate (↑Multiset.card t) 1
[PROOFSTEP]
simp only [eq_replicate, Multiset.card_map, eq_self_iff_true, true_and_iff]
[GOAL]
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ ∀ (b : R), b ∈ Multiset.map (fun f => leadingCoeff f) t → b = 1
[PROOFSTEP]
rintro i hi
[GOAL]
case h.e'_2.h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R
hi : i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ i = 1
[PROOFSTEP]
obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp hi
[GOAL]
case h.e'_2.h.e'_3.intro.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : leadingCoeff i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ leadingCoeff i = 1
[PROOFSTEP]
apply h
[GOAL]
case h.e'_2.h.e'_3.intro.intro.a
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
i : R[X]
hi✝ : i ∈ t
hi : leadingCoeff i ∈ Multiset.map (fun f => leadingCoeff f) t
⊢ i ∈ t
[PROOFSTEP]
assumption
[GOAL]
case h.e'_3
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (f : R[X]), f ∈ t → Monic f
✝ : Nontrivial R
⊢ 1 = 1 ^ ↑Multiset.card t
[PROOFSTEP]
simp
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → Monic (f i)
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
[PROOFSTEP]
simpa using natDegree_multiset_prod_of_monic (s.1.map f) (by simpa using h)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → Monic (f i)
⊢ ∀ (f_1 : R[X]), f_1 ∈ Multiset.map f s.val → Monic f_1
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
n : ℕ
hl : ∀ (p : R[X]), p ∈ t → natDegree p ≤ n
⊢ coeff (prod t) (↑Multiset.card t * n) = prod (Multiset.map (fun p => coeff p n) t)
[PROOFSTEP]
induction t using Quotient.inductionOn
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
n : ℕ
a✝ : List R[X]
hl : ∀ (p : R[X]), p ∈ Quotient.mk (List.isSetoid R[X]) a✝ → natDegree p ≤ n
⊢ coeff (prod (Quotient.mk (List.isSetoid R[X]) a✝)) (↑Multiset.card (Quotient.mk (List.isSetoid R[X]) a✝) * n) =
    prod (Multiset.map (fun p => coeff p n) (Quotient.mk (List.isSetoid R[X]) a✝))
[PROOFSTEP]
simpa using coeff_list_prod_of_natDegree_le _ _ hl
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
h : ∀ (p : ι), p ∈ s → natDegree (f p) ≤ n
⊢ coeff (∏ i in s, f i) (Finset.card s * n) = ∏ i in s, coeff (f i) n
[PROOFSTEP]
cases' s with l hl
[GOAL]
case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ coeff (∏ i in { val := l, nodup := hl }, f i) (Finset.card { val := l, nodup := hl } * n) =
    ∏ i in { val := l, nodup := hl }, coeff (f i) n
[PROOFSTEP]
convert coeff_multiset_prod_of_natDegree_le (l.map f) n ?_
[GOAL]
case h.e'_2.h.e'_4.h.e'_5
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ Finset.card { val := l, nodup := hl } = ↑Multiset.card (Multiset.map f l)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ ∏ i in { val := l, nodup := hl }, coeff (f i) n = prod (Multiset.map (fun p => coeff p n) (Multiset.map f l))
[PROOFSTEP]
simp
[GOAL]
case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ ∀ (p : R[X]), p ∈ Multiset.map f l → natDegree p ≤ n
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ coeff (prod t) 0 = prod (Multiset.map (fun f => coeff f 0) t)
[PROOFSTEP]
refine' Multiset.induction_on t _ fun a t ht => _
[GOAL]
case refine'_1
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ coeff (prod 0) 0 = prod (Multiset.map (fun f => coeff f 0) 0)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ht : coeff (prod t) 0 = prod (Multiset.map (fun f => coeff f 0) t)
⊢ coeff (prod (a ::ₘ t)) 0 = prod (Multiset.map (fun f => coeff f 0) (a ::ₘ t))
[PROOFSTEP]
rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ coeff (∏ i in s, f i) 0 = ∏ i in s, coeff (f i) 0
[PROOFSTEP]
simpa using coeff_zero_multiset_prod (s.1.map f)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ nextCoeff (prod (Multiset.map (fun x => X - ↑C x) t)) = -Multiset.sum t
[PROOFSTEP]
rw [nextCoeff_multiset_prod]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ Multiset.sum (Multiset.map (fun i => nextCoeff (X - ↑C i)) t) = -Multiset.sum t
[PROOFSTEP]
simp only [nextCoeff_X_sub_C]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ Multiset.sum (Multiset.map (fun x => -x) t) = -Multiset.sum t
[PROOFSTEP]
exact t.sum_hom (-AddMonoidHom.id R)
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ ∀ (i : R), i ∈ t → Monic (X - ↑C i)
[PROOFSTEP]
intros
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
i✝ : R
a✝ : i✝ ∈ t
⊢ Monic (X - ↑C i✝)
[PROOFSTEP]
apply monic_X_sub_C
[GOAL]
R : Type u
ι : Type w
s✝ : Finset ι
inst✝ : CommRing R
s : Finset ι
f : ι → R
⊢ nextCoeff (∏ i in s, (X - ↑C (f i))) = -∑ i in s, f i
[PROOFSTEP]
simpa using multiset_prod_X_sub_C_nextCoeff (s.1.map f)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = -Multiset.sum t
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = -Multiset.sum t
[PROOFSTEP]
convert multiset_prod_X_sub_C_nextCoeff (by assumption)
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ Multiset ?m.927417
[PROOFSTEP]
assumption
[GOAL]
case h.e'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    nextCoeff (prod (Multiset.map (fun x => X - ↑C x) t))
[PROOFSTEP]
rw [nextCoeff]
[GOAL]
case h.e'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    if natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0 then 0
    else coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) - 1)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
[PROOFSTEP]
rw [natDegree_multiset_prod_of_monic] at h
[GOAL]
case pos
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : Multiset.sum (Multiset.map natDegree (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
[PROOFSTEP]
simp only [Multiset.mem_map] at *
[GOAL]
case pos.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), f ∈ Multiset.map (fun x => X - ↑C x) t → Monic f
[PROOFSTEP]
simp only [Multiset.mem_map] at *
[GOAL]
case pos
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : Multiset.sum (Multiset.map (fun x => natDegree x) (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
case pos.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), (∃ a, a ∈ t ∧ X - ↑C a = f) → Monic f
[PROOFSTEP]
swap
[GOAL]
case pos.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), (∃ a, a ∈ t ∧ X - ↑C a = f) → Monic f
[PROOFSTEP]
rintro _ ⟨_, _, rfl⟩
[GOAL]
case pos.h.intro.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
w✝ : R
left✝ : w✝ ∈ t
⊢ Monic (X - ↑C w✝)
[PROOFSTEP]
apply monic_X_sub_C
[GOAL]
case pos
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : Multiset.sum (Multiset.map (fun x => natDegree x) (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
[PROOFSTEP]
simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map] at h
[GOAL]
case pos
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ∀ (x : ℕ), (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) → x = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
[PROOFSTEP]
contrapose! h
[GOAL]
case pos
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) ≠ 0
⊢ ∃ x, (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) ∧ x ≠ 0
[PROOFSTEP]
obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht
[GOAL]
case pos.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) ≠ 0
x : R
hx : x ∈ t
⊢ ∃ x, (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) ∧ x ≠ 0
[PROOFSTEP]
exact ⟨_, ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩, one_ne_zero⟩
[GOAL]
case neg
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ¬natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) - 1)
[PROOFSTEP]
congr
[GOAL]
case neg.e_a.e_a
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ¬natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ↑Multiset.card t = natDegree (prod (Multiset.map (fun x => X - ↑C x) t))
[PROOFSTEP]
rw [natDegree_multiset_prod_of_monic]
[GOAL]
case neg.e_a.e_a
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ¬natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ↑Multiset.card t = Multiset.sum (Multiset.map natDegree (Multiset.map (fun x => X - ↑C x) t))
[PROOFSTEP]
simp [natDegree_X_sub_C, monic_X_sub_C]
[GOAL]
case neg.e_a.e_a.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ¬natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), f ∈ Multiset.map (fun x => X - ↑C x) t → Monic f
[PROOFSTEP]
simp [natDegree_X_sub_C, monic_X_sub_C]
[GOAL]
R : Type u
ι : Type w
s✝ : Finset ι
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < Finset.card s
⊢ coeff (∏ i in s, (X - ↑C (f i))) (Finset.card s - 1) = -∑ i in s, f i
[PROOFSTEP]
simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)
[GOAL]
R : Type u
ι : Type w
s✝ : Finset ι
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < Finset.card s
⊢ 0 < ↑Multiset.card (Multiset.map f s.val)
[PROOFSTEP]
simpa using hs
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
[PROOFSTEP]
apply natDegree_prod'
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ ∏ i in s, leadingCoeff (f i) ≠ 0
[PROOFSTEP]
rw [prod_ne_zero_iff]
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ ∀ (a : ι), a ∈ s → leadingCoeff (f a) ≠ 0
[PROOFSTEP]
intro x hx
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
x : ι
hx : x ∈ s
⊢ leadingCoeff (f x) ≠ 0
[PROOFSTEP]
simp [h x hx]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ¬0 ∈ t
⊢ natDegree (prod t) = Multiset.sum (Multiset.map natDegree t)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ¬0 ∈ t
✝ : Nontrivial R
⊢ natDegree (prod t) = Multiset.sum (Multiset.map natDegree t)
[PROOFSTEP]
rw [natDegree_multiset_prod']
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ¬0 ∈ t
✝ : Nontrivial R
⊢ prod (Multiset.map (fun f => leadingCoeff f) t) ≠ 0
[PROOFSTEP]
simp_rw [Ne.def, Multiset.prod_eq_zero_iff, Multiset.mem_map, leadingCoeff_eq_zero]
[GOAL]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ¬0 ∈ t
✝ : Nontrivial R
⊢ ¬∃ a, a ∈ t ∧ a = 0
[PROOFSTEP]
rintro ⟨_, h, rfl⟩
[GOAL]
case h.intro.intro
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h✝ : ¬0 ∈ t
✝ : Nontrivial R
h : 0 ∈ t
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
⊢ leadingCoeff (prod t) = prod (Multiset.map (fun f => leadingCoeff f) t)
[PROOFSTEP]
rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
⊢ prod (Multiset.map (↑leadingCoeffHom) t) = prod (Multiset.map (fun f => leadingCoeff f) t)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
⊢ leadingCoeff (∏ i in s, f i) = ∏ i in s, leadingCoeff (f i)
[PROOFSTEP]
simpa using leadingCoeff_multiset_prod (s.1.map f)


[GOAL]
R : Type u
inst✝ : Ring R
r : R
M N : ModuleCat R
f : M ⟶ N
⊢ (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map f ≫
      (fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) N =
    (fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) M ≫
      (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map f
[PROOFSTEP]
ext
[GOAL]
case w
R : Type u
inst✝ : Ring R
r : R
M N : ModuleCat R
f : M ⟶ N
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj M)
⊢ ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map f ≫
          (fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) N)
      x✝ =
    ↑((fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) M ≫
          (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map f)
      x✝
[PROOFSTEP]
exact (f.map_smul _ _).symm
[GOAL]
R : Type u
inst✝ : Ring R
⊢ Function.LeftInverse (fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) fun r =>
    NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)
[PROOFSTEP]
intro r
[GOAL]
R : Type u
inst✝ : Ring R
r : R
⊢ (fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1)
      ((fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)) r) =
    r
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : Ring R
⊢ Function.RightInverse (fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) fun r =>
    NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r)
[PROOFSTEP]
intro φ
[GOAL]
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))
⊢ (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
    φ
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case app
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))
⊢ ((fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
        ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ)).app =
    φ.app
[PROOFSTEP]
ext M (x : M)
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))
M : ModuleCat R
x : ↑M
⊢ ↑(NatTrans.app
          ((fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
            ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ))
          M)
      x =
    ↑(NatTrans.app φ M) x
[PROOFSTEP]
have w :=
  congr_fun ((forget _).congr_map (φ.naturality (ModuleCat.asHomRight (LinearMap.toSpanSingleton R M x)))) (1 : R)
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))
M : ModuleCat R
x : ↑M
w :
  (forget AddCommGroupCat).map
      ((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map
          (ModuleCat.asHomRight (LinearMap.toSpanSingleton R (↑M) x)) ≫
        NatTrans.app φ M)
      1 =
    (forget AddCommGroupCat).map
      (NatTrans.app φ (ModuleCat.of R R) ≫
        (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.map
          (ModuleCat.asHomRight (LinearMap.toSpanSingleton R (↑M) x)))
      1
⊢ ↑(NatTrans.app
          ((fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
            ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ))
          M)
      x =
    ↑(NatTrans.app φ M) x
[PROOFSTEP]
exact w.symm.trans (congr_arg (φ.app M) (one_smul R x))
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        (x * y) =
      Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          x *
        Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          y
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : Ring R
x✝ y✝ : R
⊢ Equiv.toFun
      { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
        invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
        right_inv :=
          (_ :
            ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
              (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                  ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                φ) }
      (x✝ * y✝) =
    Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        x✝ *
      Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        y✝
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case app
R : Type u
inst✝ : Ring R
x✝ y✝ : R
⊢ (Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        (x✝ * y✝)).app =
    (Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          x✝ *
        Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          y✝).app
[PROOFSTEP]
ext
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ ↑(NatTrans.app
          (Equiv.toFun
            { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
              invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
              right_inv :=
                (_ :
                  ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                    (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                        ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                      φ) }
            (x✝² * y✝))
          x✝¹)
      x✝ =
    ↑(NatTrans.app
          (Equiv.toFun
              { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
                invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
                right_inv :=
                  (_ :
                    ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                      (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                          ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                        φ) }
              x✝² *
            Equiv.toFun
              { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
                invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
                right_inv :=
                  (_ :
                    ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                      (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                          ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                        φ) }
              y✝)
          x✝¹)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ (x✝² * y✝) • x✝ =
    ↑(NatTrans.app
          ((NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) x✝²)) *
            NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) y✝))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [AddCommGroupCat.ofHom_apply, DistribMulAction.toAddMonoidHom_apply, mul_smul]
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ x✝² • y✝ • x✝ =
    ↑(NatTrans.app
          ((NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) x✝²)) *
            NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) y✝))
          x✝¹)
      x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ∀ (x y : R),
    Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        (x + y) =
      Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          x +
        Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          y
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : Ring R
x✝ y✝ : R
⊢ Equiv.toFun
      { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
        invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
        right_inv :=
          (_ :
            ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
              (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                  ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                φ) }
      (x✝ + y✝) =
    Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        x✝ +
      Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        y✝
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case app
R : Type u
inst✝ : Ring R
x✝ y✝ : R
⊢ (Equiv.toFun
        { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
          invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
          right_inv :=
            (_ :
              ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                    ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                  φ) }
        (x✝ + y✝)).app =
    (Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          x✝ +
        Equiv.toFun
          { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
            invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
            right_inv :=
              (_ :
                ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                  (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                      ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                    φ) }
          y✝).app
[PROOFSTEP]
ext
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ ↑(NatTrans.app
          (Equiv.toFun
            { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
              invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
              right_inv :=
                (_ :
                  ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                    (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                        ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                      φ) }
            (x✝² + y✝))
          x✝¹)
      x✝ =
    ↑(NatTrans.app
          (Equiv.toFun
              { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
                invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
                right_inv :=
                  (_ :
                    ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                      (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                          ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                        φ) }
              x✝² +
            Equiv.toFun
              { toFun := fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r),
                invFun := fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1, left_inv := (_ : ∀ (r : R), r * 1 = r),
                right_inv :=
                  (_ :
                    ∀ (φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat))),
                      (fun r => NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) r))
                          ((fun φ => ↑(NatTrans.app φ (ModuleCat.of R R)) 1) φ) =
                        φ) }
              y✝)
          x✝¹)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ (x✝² + y✝) • x✝ =
    ↑(NatTrans.app
          ((NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) x✝²)) +
            NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) y✝))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [AddCommGroupCat.ofHom_apply, DistribMulAction.toAddMonoidHom_apply, add_smul]
[GOAL]
case app.h.w
R : Type u
inst✝ : Ring R
x✝² y✝ : R
x✝¹ : ModuleCat R
x✝ : ↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGroupCat)).obj.obj x✝¹)
⊢ x✝² • x✝ + y✝ • x✝ =
    ↑(NatTrans.app
          ((NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) x✝²)) +
            NatTrans.mk fun M => AddCommGroupCat.ofHom (DistribMulAction.toAddMonoidHom (↑M) y✝))
          x✝¹)
      x✝
[PROOFSTEP]
rfl


[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
⊢ ↟(Submodule.subtype (LinearMap.ker f)) ≫ f = 0
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
x : ↑(of R { x // x ∈ LinearMap.ker f })
⊢ ↑(↟(Submodule.subtype (LinearMap.ker f)) ≫ f) x = ↑0 x
[PROOFSTEP]
cases x
[GOAL]
case h.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
val✝ : ↑M
property✝ : val✝ ∈ LinearMap.ker f
⊢ ↑(↟(Submodule.subtype (LinearMap.ker f)) ≫ f) { val := val✝, property := property✝ } =
    ↑0 { val := val✝, property := property✝ }
[PROOFSTEP]
assumption
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Fork f 0
c : ↑s.pt
⊢ ↑f (↑(Fork.ι s) c) = 0
[PROOFSTEP]
rw [← @Function.comp_apply _ _ _ f (Fork.ι s) c, ← coe_comp, Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N]
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Fork f 0
c : ↑s.pt
⊢ ↑0 c = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = Fork.ι s
x : ↑s.pt
⊢ ↑(↑m x) =
    ↑(↑((fun s =>
              LinearMap.codRestrict (LinearMap.ker f) (Fork.ι s) (_ : ∀ (c : ↑s.pt), ↑(Fork.ι s) c ∈ LinearMap.ker f))
            s)
        x)
[PROOFSTEP]
simp [← h]
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = Fork.ι s
x : ↑s.pt
⊢ ↑m x =
    ↑(LinearMap.codRestrict (LinearMap.ker f) (m ≫ Fork.ι (kernelCone f))
          (_ : ∀ (c : ↑s.pt), ↑(m ≫ Fork.ι (kernelCone f)) c ∈ LinearMap.ker f))
      x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = Cofork.π s
⊢ m = (fun s => Submodule.liftQ (LinearMap.range f) (Cofork.π s) (_ : LinearMap.range f ≤ LinearMap.ker (Cofork.π s))) s
[PROOFSTEP]
haveI : Epi (asHom (LinearMap.range f).mkQ) :=
  (epi_iff_range_eq_top _).mpr
    (Submodule.range_mkQ _)
      -- Porting note: broken dot notation
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = Cofork.π s
this : Epi (↟(Submodule.mkQ (LinearMap.range f)))
⊢ m = (fun s => Submodule.liftQ (LinearMap.range f) (Cofork.π s) (_ : LinearMap.range f ≤ LinearMap.ker (Cofork.π s))) s
[PROOFSTEP]
apply (cancel_epi (asHom (LinearMap.range f).mkQ)).1
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = Cofork.π s
this : Epi (↟(Submodule.mkQ (LinearMap.range f)))
⊢ ↟(Submodule.mkQ (LinearMap.range f)) ≫ m =
    ↟(Submodule.mkQ (LinearMap.range f)) ≫
      (fun s => Submodule.liftQ (LinearMap.range f) (Cofork.π s) (_ : LinearMap.range f ≤ LinearMap.ker (Cofork.π s))) s
[PROOFSTEP]
convert h
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
⊢ cokernel.π f ≫ (cokernelIsoRangeQuotient f).hom = Submodule.mkQ (LinearMap.range f)
[PROOFSTEP]
convert colimit.isoColimitCocone_ι_hom (F := parallelPair f 0) _ _
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f✝ : G ⟶ H
M N : ModuleCat R
f : M ⟶ N
x y : ↑N
m : ↑M
w : x = y + ↑f m
⊢ ↑(cokernel.π f) x = ↑(cokernel.π f) y
[PROOFSTEP]
subst w
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f✝ : G ⟶ H
M N : ModuleCat R
f : M ⟶ N
y : ↑N
m : ↑M
⊢ ↑(cokernel.π f) (y + ↑f m) = ↑(cokernel.π f) y
[PROOFSTEP]
simpa only [map_add, add_right_eq_self] using cokernel.condition_apply f m


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