[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ ker (pi f) = ⨅ (i : ι), ker (f i)
[PROOFSTEP]
ext c
[GOAL]
case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
⊢ c ∈ ker (pi f) ↔ c ∈ ⨅ (i : ι), ker (f i)
[PROOFSTEP]
simp [funext_iff]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ pi f = 0 ↔ ∀ (i : ι), f i = 0
[PROOFSTEP]
simp only [LinearMap.ext_iff, pi_apply, funext_iff]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ (∀ (x : M₂) (a : ι), ↑(f a) x = ↑0 x a) ↔ ∀ (i : ι) (x : M₂), ↑(f i) x = ↑0 x
[PROOFSTEP]
exact ⟨fun h a b => h b a, fun h a b => h b a⟩
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
⊢ (pi fun i => 0) = 0
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
x✝¹ : M₂
x✝ : ι
⊢ ↑(pi fun i => 0) x✝¹ x✝ = ↑0 x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
a : (i : ι) → φ i
h : a ∈ ⨅ (i : ι), ker (proj i)
⊢ a ∈ ⊥
[PROOFSTEP]
simp only [mem_iInf, mem_ker, proj_apply] at h 
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
a : (i : ι) → φ i
h : ∀ (i : ι), a i = 0
⊢ a ∈ ⊥
[PROOFSTEP]
exact (mem_bot _).2 (funext fun i => h i)
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : M₂ →ₗ[R] M₃
I : Type u_1
src✝ : (I → M₂) →+ I → M₃ := AddMonoidHom.compLeft (toAddMonoidHom f) I
c : R
h : I → M₂
⊢ AddHom.toFun
      { toFun := fun h => ↑f ∘ h,
        map_add' :=
          (_ : ∀ (x y : I → M₂), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (c • h) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun h => ↑f ∘ h,
          map_add' :=
            (_ : ∀ (x y : I → M₂), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        h
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : M₂ →ₗ[R] M₃
I : Type u_1
src✝ : (I → M₂) →+ I → M₃ := AddMonoidHom.compLeft (toAddMonoidHom f) I
c : R
h : I → M₂
x : I
⊢ AddHom.toFun
      { toFun := fun h => ↑f ∘ h,
        map_add' :=
          (_ : ∀ (x y : I → M₂), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (c • h) x =
    (↑(RingHom.id R) c •
        AddHom.toFun
          { toFun := fun h => ↑f ∘ h,
            map_add' :=
              (_ :
                ∀ (x y : I → M₂), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
          h)
      x
[PROOFSTEP]
exact f.map_smul' c (h x)
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
S : Type ?u.45562
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f g : (i : ι) → φ i →ₗ[R] M
⊢ (fun f => ∑ i : ι, comp (f i) (proj i)) (f + g) =
    (fun f => ∑ i : ι, comp (f i) (proj i)) f + (fun f => ∑ i : ι, comp (f i) (proj i)) g
[PROOFSTEP]
simp only [Pi.add_apply, add_comp, Finset.sum_add_distrib]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
S : Type ?u.45562
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
c : S
f : (i : ι) → φ i →ₗ[R] M
⊢ AddHom.toFun
      { toFun := fun f => ∑ i : ι, comp (f i) (proj i),
        map_add' :=
          (_ :
            ∀ (f g : (i : ι) → φ i →ₗ[R] M),
              ∑ i : ι, comp ((f + g) i) (proj i) = ∑ x : ι, comp (f x) (proj x) + ∑ x : ι, comp (g x) (proj x)) }
      (c • f) =
    ↑(RingHom.id S) c •
      AddHom.toFun
        { toFun := fun f => ∑ i : ι, comp (f i) (proj i),
          map_add' :=
            (_ :
              ∀ (f g : (i : ι) → φ i →ₗ[R] M),
                ∑ i : ι, comp ((f + g) i) (proj i) = ∑ x : ι, comp (f x) (proj x) + ∑ x : ι, comp (g x) (proj x)) }
        f
[PROOFSTEP]
simp only [Pi.smul_apply, smul_comp, Finset.smul_sum, RingHom.id_apply]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
S : Type ?u.45562
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : (i : ι) → φ i →ₗ[R] M
⊢ (fun f i => comp f (single i))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => ∑ i : ι, comp (f i) (proj i),
                map_add' :=
                  (_ :
                    ∀ (f g : (i : ι) → φ i →ₗ[R] M),
                      ∑ i : ι, comp ((f + g) i) (proj i) =
                        ∑ x : ι, comp (f x) (proj x) + ∑ x : ι, comp (g x) (proj x)) },
            map_smul' :=
              (_ :
                ∀ (c : S) (f : (i : ι) → φ i →ₗ[R] M),
                  ∑ i : ι, comp ((c • f) i) (proj i) = c • ∑ x : ι, comp (f x) (proj x)) }.toAddHom
        f) =
    f
[PROOFSTEP]
ext i x
[GOAL]
case h.h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
S : Type ?u.45562
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : (i : ι) → φ i →ₗ[R] M
i : ι
x : φ i
⊢ ↑((fun f i => comp f (single i))
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => ∑ i : ι, comp (f i) (proj i),
                    map_add' :=
                      (_ :
                        ∀ (f g : (i : ι) → φ i →ₗ[R] M),
                          ∑ i : ι, comp ((f + g) i) (proj i) =
                            ∑ x : ι, comp (f x) (proj x) + ∑ x : ι, comp (g x) (proj x)) },
                map_smul' :=
                  (_ :
                    ∀ (c : S) (f : (i : ι) → φ i →ₗ[R] M),
                      ∑ i : ι, comp ((c • f) i) (proj i) = c • ∑ x : ι, comp (f x) (proj x)) }.toAddHom
            f)
          i)
      x =
    ↑(f i) x
[PROOFSTEP]
simp [apply_single]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
S : Type ?u.45562
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => ∑ i : ι, comp (f i) (proj i),
              map_add' :=
                (_ :
                  ∀ (f g : (i : ι) → φ i →ₗ[R] M),
                    ∑ i : ι, comp ((f + g) i) (proj i) = ∑ x : ι, comp (f x) (proj x) + ∑ x : ι, comp (g x) (proj x)) },
          map_smul' :=
            (_ :
              ∀ (c : S) (f : (i : ι) → φ i →ₗ[R] M),
                ∑ i : ι, comp ((c • f) i) (proj i) = c • ∑ x : ι, comp (f x) (proj x)) }.toAddHom
      ((fun f i => comp f (single i)) f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
S : Type ?u.45562
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ ↑(AddHom.toFun
          {
              toAddHom :=
                { toFun := fun f => ∑ i : ι, comp (f i) (proj i),
                  map_add' :=
                    (_ :
                      ∀ (f g : (i : ι) → φ i →ₗ[R] M),
                        ∑ i : ι, comp ((f + g) i) (proj i) =
                          ∑ x : ι, comp (f x) (proj x) + ∑ x : ι, comp (g x) (proj x)) },
              map_smul' :=
                (_ :
                  ∀ (c : S) (f : (i : ι) → φ i →ₗ[R] M),
                    ∑ i : ι, comp ((c • f) i) (proj i) = c • ∑ x : ι, comp (f x) (proj x)) }.toAddHom
          ((fun f i => comp f (single i)) f))
      x =
    ↑f x
[PROOFSTEP]
suffices f (∑ j, Pi.single j (x j)) = f x by simpa [apply_single]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
S : Type ?u.45562
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
this : ↑f (∑ j : ι, Pi.single j (x j)) = ↑f x
⊢ ↑(AddHom.toFun
          {
              toAddHom :=
                { toFun := fun f => ∑ i : ι, comp (f i) (proj i),
                  map_add' :=
                    (_ :
                      ∀ (f g : (i : ι) → φ i →ₗ[R] M),
                        ∑ i : ι, comp ((f + g) i) (proj i) =
                          ∑ x : ι, comp (f x) (proj x) + ∑ x : ι, comp (g x) (proj x)) },
              map_smul' :=
                (_ :
                  ∀ (c : S) (f : (i : ι) → φ i →ₗ[R] M),
                    ∑ i : ι, comp ((c • f) i) (proj i) = c • ∑ x : ι, comp (f x) (proj x)) }.toAddHom
          ((fun f i => comp f (single i)) f))
      x =
    ↑f x
[PROOFSTEP]
simpa [apply_single]
[GOAL]
case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
S : Type ?u.45562
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ ↑f (∑ j : ι, Pi.single j (x j)) = ↑f x
[PROOFSTEP]
rw [Finset.univ_sum_single]
[GOAL]
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι✝ : Type x
ι' : Type x'
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R✝ M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : Module R✝ M₃
φ : ι✝ → Type i
inst✝⁶ : (i : ι✝) → AddCommMonoid (φ i)
inst✝⁵ : (i : ι✝) → Module R✝ (φ i)
ι : Type u_1
R : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : CommRing R
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
x : (i : ι) → M i
⊢ ↑(↑(lsum R M R) single) x = ↑id x
[PROOFSTEP]
simp [Finset.univ_sum_single]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M₃
φ : ι → Type i
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : Finite ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), comp f (single i) = comp g (single i)
⊢ f = g
[PROOFSTEP]
refine' pi_ext fun i x => _
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M₃
φ : ι → Type i
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : Finite ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), comp f (single i) = comp g (single i)
i : ι
x : φ i
⊢ ↑f (Pi.single i x) = ↑g (Pi.single i x)
[PROOFSTEP]
convert LinearMap.congr_fun (h i) x
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ { x // x ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i) } ≃ₗ[R] (i : ↑I) → φ ↑i
[PROOFSTEP]
refine'
  LinearEquiv.ofLinear (pi fun i => (proj (i : ι)).comp (Submodule.subtype _))
    (codRestrict _ (pi fun i => if h : i ∈ I then proj (⟨i, h⟩ : I) else 0) _) _ _
[GOAL]
case refine'_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ ∀ (c : (i : ↑I) → φ ↑i),
    ↑(pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0) c ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
[PROOFSTEP]
intro b
[GOAL]
case refine'_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
⊢ ↑(pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0) b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
[PROOFSTEP]
simp only [mem_iInf, mem_ker, funext_iff, proj_apply, pi_apply]
[GOAL]
case refine'_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
⊢ ∀ (i : ι), i ∈ J → ↑(if h : i ∈ I then proj { val := i, property := h } else 0) b = 0
[PROOFSTEP]
intro j hjJ
[GOAL]
case refine'_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
⊢ ↑(if h : j ∈ I then proj { val := j, property := h } else 0) b = 0
[PROOFSTEP]
have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩
[GOAL]
case refine'_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
this : ¬j ∈ I
⊢ ↑(if h : j ∈ I then proj { val := j, property := h } else 0) b = 0
[PROOFSTEP]
rw [dif_neg this, zero_apply]
[GOAL]
case refine'_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ comp (pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i))))
      (codRestrict (⨅ (i : ι) (_ : i ∈ J), ker (proj i))
        (pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0)
        (_ :
          ∀ (b : (i : ↑I) → φ ↑i),
            ↑(pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0) b ∈
              ⨅ (i : ι) (_ : i ∈ J), ker (proj i))) =
    id
[PROOFSTEP]
simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop]
[GOAL]
case refine'_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (pi fun i => if h : True then proj { val := ↑i, property := (_ : ↑i ∈ I) } else 0) = id
[PROOFSTEP]
ext b ⟨j, hj⟩
[GOAL]
case refine'_2.h.h.mk
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hj : j ∈ I
⊢ ↑(pi fun i => if h : True then proj { val := ↑i, property := (_ : ↑i ∈ I) } else 0) b { val := j, property := hj } =
    ↑id b { val := j, property := hj }
[PROOFSTEP]
simp only [dif_pos, Function.comp_apply, Function.eval_apply, LinearMap.codRestrict_apply, LinearMap.coe_comp,
  LinearMap.coe_proj, LinearMap.pi_apply, Submodule.subtype_apply, Subtype.coe_prop]
[GOAL]
case refine'_2.h.h.mk
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hj : j ∈ I
⊢ eval { val := j, property := (_ : j ∈ I) } b = ↑id b { val := j, property := hj }
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ comp
      (codRestrict (⨅ (i : ι) (_ : i ∈ J), ker (proj i))
        (pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0)
        (_ :
          ∀ (b : (i : ↑I) → φ ↑i),
            ↑(pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0) b ∈
              ⨅ (i : ι) (_ : i ∈ J), ker (proj i)))
      (pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i)))) =
    id
[PROOFSTEP]
ext1 ⟨b, hb⟩
[GOAL]
case refine'_3.h.mk
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
⊢ ↑(comp
          (codRestrict (⨅ (i : ι) (_ : i ∈ J), ker (proj i))
            (pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0)
            (_ :
              ∀ (b : (i : ↑I) → φ ↑i),
                ↑(pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0) b ∈
                  ⨅ (i : ι) (_ : i ∈ J), ker (proj i)))
          (pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i)))))
      { val := b, property := hb } =
    ↑id { val := b, property := hb }
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case refine'_3.h.mk.a
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
⊢ ↑(↑(comp
            (codRestrict (⨅ (i : ι) (_ : i ∈ J), ker (proj i))
              (pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0)
              (_ :
                ∀ (b : (i : ↑I) → φ ↑i),
                  ↑(pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0) b ∈
                    ⨅ (i : ι) (_ : i ∈ J), ker (proj i)))
            (pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i)))))
        { val := b, property := hb }) =
    ↑(↑id { val := b, property := hb })
[PROOFSTEP]
ext j
[GOAL]
case refine'_3.h.mk.a.h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
j : ι
⊢ ↑(↑(comp
              (codRestrict (⨅ (i : ι) (_ : i ∈ J), ker (proj i))
                (pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0)
                (_ :
                  ∀ (b : (i : ↑I) → φ ↑i),
                    ↑(pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0) b ∈
                      ⨅ (i : ι) (_ : i ∈ J), ker (proj i)))
              (pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i)))))
          { val := b, property := hb })
      j =
    ↑(↑id { val := b, property := hb }) j
[PROOFSTEP]
have hb : ∀ i ∈ J, b i = 0 := by simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
j : ι
⊢ ∀ (i : ι), i ∈ J → b i = 0
[PROOFSTEP]
simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb
[GOAL]
case refine'_3.h.mk.a.h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
j : ι
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ↑(↑(comp
              (codRestrict (⨅ (i : ι) (_ : i ∈ J), ker (proj i))
                (pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0)
                (_ :
                  ∀ (b : (i : ↑I) → φ ↑i),
                    ↑(pi fun i => if h : i ∈ I then proj { val := i, property := h } else 0) b ∈
                      ⨅ (i : ι) (_ : i ∈ J), ker (proj i)))
              (pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i)))))
          { val := b, property := hb✝ })
      j =
    ↑(↑id { val := b, property := hb✝ }) j
[PROOFSTEP]
simp only [comp_apply, pi_apply, id_apply, proj_apply, subtype_apply, codRestrict_apply]
[GOAL]
case refine'_3.h.mk.a.h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
j : ι
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ↑(if h : j ∈ I then proj { val := j, property := h } else 0)
      (↑(pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i))))
        { val := b, property := hb✝ }) =
    b j
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
j : ι
hb : ∀ (i : ι), i ∈ J → b i = 0
h : j ∈ I
⊢ ↑(proj { val := j, property := h })
      (↑(pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i))))
        { val := b, property := hb✝ }) =
    b j
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i => i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
j : ι
hb : ∀ (i : ι), i ∈ J → b i = 0
h : ¬j ∈ I
⊢ ↑0
      (↑(pi fun i => comp (proj ↑i) (Submodule.subtype (⨅ (i : ι) (_ : i ∈ J), ker (proj i))))
        { val := b, property := hb✝ }) =
    b j
[PROOFSTEP]
exact (hb _ <| (hu trivial).resolve_left h).symm
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
⊢ ↑(update f i b j) c = update (fun i => ↑(f i) c) i (↑b c) j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ ↑(update f i b j) c = update (fun i => ↑(f i) c) i (↑b c) j
[PROOFSTEP]
rw [h, update_same, update_same]
[GOAL]
case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ ↑(update f i b j) c = update (fun i => ↑(f i) c) i (↑b c) j
[PROOFSTEP]
rw [update_noteq h, update_noteq h]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ ⨅ (i : ι) (_ : i ∈ I), comap (proj i) (p i) = pi I p
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ x : (i : ι) → φ i
⊢ x ∈ ⨅ (i : ι) (_ : i ∈ I), comap (proj i) (p i) ↔ x ∈ pi I p
[PROOFSTEP]
simp
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ ⨅ (i : ι), comap (proj i) (p i) = pi Set.univ p
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ x : (i : ι) → φ i
⊢ x ∈ ⨅ (i : ι), comap (proj i) (p i) ↔ x ∈ pi Set.univ p
[PROOFSTEP]
simp
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
⊢ ⨆ (i : ι), map (single i) (p i) = pi Set.univ p
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ ⨆ (i : ι), map (single i) (p i) = pi Set.univ p
[PROOFSTEP]
refine' (iSup_le fun i => _).antisymm _
[GOAL]
case intro.refine'_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
i : ι
⊢ map (single i) (p i) ≤ pi Set.univ p
[PROOFSTEP]
rintro _ ⟨x, hx : x ∈ p i, rfl⟩ j -
[GOAL]
case intro.refine'_1.intro.intro
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
⊢ ↑(single i) x j ∈ (fun i => ↑(p i)) j
[PROOFSTEP]
rcases em (j = i) with (rfl | hj)
[GOAL]
case intro.refine'_1.intro.intro.inl
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
j : ι
x : φ j
hx : x ∈ p j
⊢ ↑(single j) x j ∈ (fun i => ↑(p i)) j
[PROOFSTEP]
simp [*]
[GOAL]
case intro.refine'_1.intro.intro.inr
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
hj : ¬j = i
⊢ ↑(single i) x j ∈ (fun i => ↑(p i)) j
[PROOFSTEP]
simp [*]
[GOAL]
case intro.refine'_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ pi Set.univ p ≤ ⨆ (i : ι), map (single i) (p i)
[PROOFSTEP]
intro x hx
[GOAL]
case intro.refine'_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi Set.univ p
⊢ x ∈ ⨆ (i : ι), map (single i) (p i)
[PROOFSTEP]
rw [← Finset.univ_sum_single x]
[GOAL]
case intro.refine'_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
I : Set ι
p q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi Set.univ p
⊢ ∑ i : ι, Pi.single i (x i) ∈ ⨆ (i : ι), map (single i) (p i)
[PROOFSTEP]
exact sum_mem_iSup fun i => mem_map_of_mem (hx i trivial)
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I : Set ι
p✝ q : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
⊢ p i ≤ comap (single i) (pi Set.univ p)
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I : Set ι
p✝ q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
⊢ x ∈ comap (single i) (pi Set.univ p)
[PROOFSTEP]
rw [Submodule.mem_comap, Submodule.mem_pi]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I : Set ι
p✝ q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
⊢ ∀ (i_1 : ι), i_1 ∈ Set.univ → ↑(single i) x i_1 ∈ p i_1
[PROOFSTEP]
rintro j -
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I : Set ι
p✝ q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
⊢ ↑(single i) x j ∈ p j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I : Set ι
p✝ q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : j = i
⊢ ↑(single i) x j ∈ p j
[PROOFSTEP]
rwa [h, LinearMap.coe_single, Pi.single_eq_same]
[GOAL]
case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I : Set ι
p✝ q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : ¬j = i
⊢ ↑(single i) x j ∈ p j
[PROOFSTEP]
rw [LinearMap.coe_single, Pi.single_eq_of_ne h]
[GOAL]
case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I : Set ι
p✝ q : (i : ι) → Submodule R (φ i)
x✝ : (i : ι) → φ i
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : ¬j = i
⊢ 0 ∈ p j
[PROOFSTEP]
exact (p j).zero_mem
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : (i : ι) → AddCommMonoid (ψ i)
inst✝² : (i : ι) → Module R (ψ i)
inst✝¹ : (i : ι) → AddCommMonoid (χ i)
inst✝ : (i : ι) → Module R (χ i)
e : (i : ι) → φ i ≃ₗ[R] ψ i
src✝ : ((j : ι) → φ j) ≃+ ((j : ι) → ψ j) := AddEquiv.piCongrRight fun j => toAddEquiv (e j)
c : R
f : (i : ι) → φ i
⊢ AddHom.toFun
      { toFun := fun f i => ↑(e i) (f i),
        map_add' :=
          (_ :
            ∀ (x y : (j : ι) → φ j),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun f i => ↑(e i) (f i),
          map_add' :=
            (_ :
              ∀ (x y : (j : ι) → φ j),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : (i : ι) → AddCommMonoid (ψ i)
inst✝² : (i : ι) → Module R (ψ i)
inst✝¹ : (i : ι) → AddCommMonoid (χ i)
inst✝ : (i : ι) → Module R (χ i)
e : (i : ι) → φ i ≃ₗ[R] ψ i
src✝ : ((j : ι) → φ j) ≃+ ((j : ι) → ψ j) := AddEquiv.piCongrRight fun j => toAddEquiv (e j)
c : R
f : (i : ι) → φ i
x✝ : ι
⊢ AddHom.toFun
      { toFun := fun f i => ↑(e i) (f i),
        map_add' :=
          (_ :
            ∀ (x y : (j : ι) → φ j),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (c • f) x✝ =
    (↑(RingHom.id R) c •
        AddHom.toFun
          { toFun := fun f i => ↑(e i) (f i),
            map_add' :=
              (_ :
                ∀ (x y : (j : ι) → φ j),
                  Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
          f)
      x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι✝ : Type x
ι' : Type x'
inst✝⁸ : Semiring R
φ : ι✝ → Type u_1
ψ : ι✝ → Type u_2
χ : ι✝ → Type u_3
inst✝⁷ : (i : ι✝) → AddCommMonoid (φ i)
inst✝⁶ : (i : ι✝) → Module R (φ i)
inst✝⁵ : (i : ι✝) → AddCommMonoid (ψ i)
inst✝⁴ : (i : ι✝) → Module R (ψ i)
inst✝³ : (i : ι✝) → AddCommMonoid (χ i)
inst✝² : (i : ι✝) → Module R (χ i)
ι : Type u_4
M : Option ι → Type u_5
inst✝¹ : (i : Option ι) → AddCommGroup (M i)
inst✝ : (i : Option ι) → Module R (M i)
src✝ : ((a : Option ι) → M a) ≃ M none × ((a : ι) → M (some a)) := Equiv.piOptionEquivProd
⊢ ∀ (x y : (i : Option ι) → M i), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y
[PROOFSTEP]
simp [Function.funext_iff]
[GOAL]
R : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι✝ : Type x
ι' : Type x'
inst✝⁸ : Semiring R
φ : ι✝ → Type u_1
ψ : ι✝ → Type u_2
χ : ι✝ → Type u_3
inst✝⁷ : (i : ι✝) → AddCommMonoid (φ i)
inst✝⁶ : (i : ι✝) → Module R (φ i)
inst✝⁵ : (i : ι✝) → AddCommMonoid (ψ i)
inst✝⁴ : (i : ι✝) → Module R (ψ i)
inst✝³ : (i : ι✝) → AddCommMonoid (χ i)
inst✝² : (i : ι✝) → Module R (χ i)
ι : Type u_4
M : Option ι → Type u_5
inst✝¹ : (i : Option ι) → AddCommGroup (M i)
inst✝ : (i : Option ι) → Module R (M i)
src✝ : ((a : Option ι) → M a) ≃ M none × ((a : ι) → M (some a)) := Equiv.piOptionEquivProd
⊢ ∀ (r : R) (x : (i : Option ι) → M i),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (a a_1 : (i : Option ι) → M i),
                (a none + a_1 none, fun a_2 => a (some a_2) + a_1 (some a_2)) =
                  (a none + a_1 none, (fun a_2 => a (some a_2)) + fun a => a_1 (some a))) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀ (a a_1 : (i : Option ι) → M i),
                  (a none + a_1 none, fun a_2 => a (some a_2) + a_1 (some a_2)) =
                    (a none + a_1 none, (fun a_2 => a (some a_2)) + fun a => a_1 (some a))) }
          x
[PROOFSTEP]
simp [Function.funext_iff]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹² : (i : ι) → AddCommMonoid (φ i)
inst✝¹¹ : (i : ι) → Module R (φ i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (ψ i)
inst✝⁹ : (i : ι) → Module R (ψ i)
inst✝⁸ : (i : ι) → AddCommMonoid (χ i)
inst✝⁷ : (i : ι) → Module R (χ i)
S : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ι → M
g : ι → R
⊢ ↑(↑(symm (piRing R M ι S)) f) g = ∑ i : ι, g i • f i
[PROOFSTEP]
simp [piRing, LinearMap.lsum_apply]
[GOAL]
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : (α ⊕ β → M) ≃ (α → M) × (β → M) := Equiv.sumArrowEquivProdArrow α β M
⊢ ∀ (x y : α ⊕ β → M), Equiv.toFun src✝ (x + y) = Equiv.toFun src✝ x + Equiv.toFun src✝ y
[PROOFSTEP]
intro f g
[GOAL]
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : (α ⊕ β → M) ≃ (α → M) × (β → M) := Equiv.sumArrowEquivProdArrow α β M
f g : α ⊕ β → M
⊢ Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g
[PROOFSTEP]
ext
[GOAL]
case h₁.h
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : (α ⊕ β → M) ≃ (α → M) × (β → M) := Equiv.sumArrowEquivProdArrow α β M
f g : α ⊕ β → M
x✝ : α
⊢ Prod.fst (Equiv.toFun src✝ (f + g)) x✝ = Prod.fst (Equiv.toFun src✝ f + Equiv.toFun src✝ g) x✝
[PROOFSTEP]
rfl
[GOAL]
case h₂.h
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : (α ⊕ β → M) ≃ (α → M) × (β → M) := Equiv.sumArrowEquivProdArrow α β M
f g : α ⊕ β → M
x✝ : β
⊢ Prod.snd (Equiv.toFun src✝ (f + g)) x✝ = Prod.snd (Equiv.toFun src✝ f + Equiv.toFun src✝ g) x✝
[PROOFSTEP]
rfl
[GOAL]
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : (α ⊕ β → M) ≃ (α → M) × (β → M) := Equiv.sumArrowEquivProdArrow α β M
⊢ ∀ (r : R) (x : α ⊕ β → M),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (f g : α ⊕ β → M), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' := (_ : ∀ (f g : α ⊕ β → M), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g) }
          x
[PROOFSTEP]
intro r f
[GOAL]
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : (α ⊕ β → M) ≃ (α → M) × (β → M) := Equiv.sumArrowEquivProdArrow α β M
r : R
f : α ⊕ β → M
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' := (_ : ∀ (f g : α ⊕ β → M), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g) }
      (r • f) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (f g : α ⊕ β → M), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g) }
        f
[PROOFSTEP]
ext
[GOAL]
case h₁.h
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : (α ⊕ β → M) ≃ (α → M) × (β → M) := Equiv.sumArrowEquivProdArrow α β M
r : R
f : α ⊕ β → M
x✝ : α
⊢ Prod.fst
      (AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (f g : α ⊕ β → M), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g) }
        (r • f))
      x✝ =
    Prod.fst
      (↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' := (_ : ∀ (f g : α ⊕ β → M), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g) }
          f)
      x✝
[PROOFSTEP]
rfl
[GOAL]
case h₂.h
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : (α ⊕ β → M) ≃ (α → M) × (β → M) := Equiv.sumArrowEquivProdArrow α β M
r : R
f : α ⊕ β → M
x✝ : β
⊢ Prod.snd
      (AddHom.toFun
        { toFun := src✝.toFun,
          map_add' := (_ : ∀ (f g : α ⊕ β → M), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g) }
        (r • f))
      x✝ =
    Prod.snd
      (↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' := (_ : ∀ (f g : α ⊕ β → M), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ f + Equiv.toFun src✝ g) }
          f)
      x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
η : Type x
inst✝ : Semiring R
s : ι → η
src✝ : (ι → R) →+ η → R := hom R s
r : R
f : ι → R
⊢ AddHom.toFun
      { toFun := fun f => extend s f 0,
        map_add' :=
          (_ : ∀ (x y : ι → R), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
      (r • f) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun f => extend s f 0,
          map_add' :=
            (_ : ∀ (x y : ι → R), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        f
[PROOFSTEP]
simpa using Function.extend_smul r s f 0
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
n : ℕ
f : M →ₗ[R] M₂
g : M →ₗ[R] Fin n → M₂
x y : M
⊢ (fun m => Matrix.vecCons (↑f m) (↑g m)) (x + y) =
    (fun m => Matrix.vecCons (↑f m) (↑g m)) x + (fun m => Matrix.vecCons (↑f m) (↑g m)) y
[PROOFSTEP]
simp only []
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
n : ℕ
f : M →ₗ[R] M₂
g : M →ₗ[R] Fin n → M₂
x y : M
⊢ Matrix.vecCons (↑f (x + y)) (↑g (x + y)) = Matrix.vecCons (↑f x) (↑g x) + Matrix.vecCons (↑f y) (↑g y)
[PROOFSTEP]
rw [f.map_add, g.map_add, Matrix.cons_add_cons (f x)]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
n : ℕ
f : M →ₗ[R] M₂
g : M →ₗ[R] Fin n → M₂
c : R
x : M
⊢ AddHom.toFun
      { toFun := fun m => Matrix.vecCons (↑f m) (↑g m),
        map_add' :=
          (_ :
            ∀ (x y : M),
              (fun m => Matrix.vecCons (↑f m) (↑g m)) (x + y) =
                (fun m => Matrix.vecCons (↑f m) (↑g m)) x + (fun m => Matrix.vecCons (↑f m) (↑g m)) y) }
      (c • x) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun m => Matrix.vecCons (↑f m) (↑g m),
          map_add' :=
            (_ :
              ∀ (x y : M),
                (fun m => Matrix.vecCons (↑f m) (↑g m)) (x + y) =
                  (fun m => Matrix.vecCons (↑f m) (↑g m)) x + (fun m => Matrix.vecCons (↑f m) (↑g m)) y) }
        x
[PROOFSTEP]
simp only []
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
n : ℕ
f : M →ₗ[R] M₂
g : M →ₗ[R] Fin n → M₂
c : R
x : M
⊢ Matrix.vecCons (↑f (c • x)) (↑g (c • x)) = ↑(RingHom.id R) c • Matrix.vecCons (↑f x) (↑g x)
[PROOFSTEP]
rw [f.map_smul, g.map_smul, RingHom.id_apply, Matrix.smul_cons c (f x)]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
n : ℕ
f : M →ₗ[R] M₂ →ₗ[R] M₃
g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃
x y : M
z : M₂
⊢ ↑((fun m => vecCons (↑f m) (↑g m)) (x + y)) z =
    ↑((fun m => vecCons (↑f m) (↑g m)) x + (fun m => vecCons (↑f m) (↑g m)) y) z
[PROOFSTEP]
simp only [f.map_add, g.map_add, LinearMap.add_apply, LinearMap.vecCons_apply, Matrix.cons_add_cons (f x z)]
[GOAL]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
n : ℕ
f : M →ₗ[R] M₂ →ₗ[R] M₃
g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃
r : R
x : M
z : M₂
⊢ ↑(AddHom.toFun
          { toFun := fun m => vecCons (↑f m) (↑g m),
            map_add' :=
              (_ :
                ∀ (x y : M),
                  (fun m => vecCons (↑f m) (↑g m)) (x + y) =
                    (fun m => vecCons (↑f m) (↑g m)) x + (fun m => vecCons (↑f m) (↑g m)) y) }
          (r • x))
      z =
    ↑(↑(RingHom.id R) r •
          AddHom.toFun
            { toFun := fun m => vecCons (↑f m) (↑g m),
              map_add' :=
                (_ :
                  ∀ (x y : M),
                    (fun m => vecCons (↑f m) (↑g m)) (x + y) =
                      (fun m => vecCons (↑f m) (↑g m)) x + (fun m => vecCons (↑f m) (↑g m)) y) }
            x)
      z
[PROOFSTEP]
simp [Matrix.smul_cons r (f x z)]
