[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
U U₁ U₂ : Submodule R M
x x₁ x₂ y y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
⊢ x ≡ y [SMOD U] ↔ x - y ∈ U
[PROOFSTEP]
rw [SModEq.def, Submodule.Quotient.eq]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
U U₁ U₂ : Submodule R M
x x₁ x₂ y y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
⊢ x ≡ y [SMOD ⊥] ↔ x = y
[PROOFSTEP]
rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
U U₁ U₂ : Submodule R M
x x₁ x₂ y y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
⊢ x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
[PROOFSTEP]
rw [SModEq.def] at hxy₁ hxy₂ ⊢
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
U U₁ U₂ : Submodule R M
x x₁ x₂ y y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk (x₁ + x₂) = Submodule.Quotient.mk (y₁ + y₂)
[PROOFSTEP]
simp_rw [Quotient.mk_add, hxy₁, hxy₂]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
U U₁ U₂ : Submodule R M
x x₁ x₂ y y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
hxy : x ≡ y [SMOD U]
c : R
⊢ c • x ≡ c • y [SMOD U]
[PROOFSTEP]
rw [SModEq.def] at hxy ⊢
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
U U₁ U₂ : Submodule R M
x x₁ x₂ y y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y
c : R
⊢ Submodule.Quotient.mk (c • x) = Submodule.Quotient.mk (c • y)
[PROOFSTEP]
simp_rw [Quotient.mk_smul, hxy]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
U U₁ U₂ : Submodule R M
x x₁ x₂ y y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
⊢ x ≡ 0 [SMOD U] ↔ x ∈ U
[PROOFSTEP]
rw [SModEq.def, Submodule.Quotient.eq, sub_zero]
[GOAL]
R✝ : Type u_1
inst✝⁵ : Ring R✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_4
inst✝ : CommRing R
I : Ideal R
x y : R
h : x ≡ y [SMOD I]
f : R[X]
⊢ Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]
[PROOFSTEP]
rw [SModEq.def] at h ⊢
[GOAL]
R✝ : Type u_1
inst✝⁵ : Ring R✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_4
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ Submodule.Quotient.mk (Polynomial.eval x f) = Submodule.Quotient.mk (Polynomial.eval y f)
[PROOFSTEP]
show Ideal.Quotient.mk I (f.eval x) = Ideal.Quotient.mk I (f.eval y)
[GOAL]
R✝ : Type u_1
inst✝⁵ : Ring R✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_4
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ ↑(Ideal.Quotient.mk I) (Polynomial.eval x f) = ↑(Ideal.Quotient.mk I) (Polynomial.eval y f)
[PROOFSTEP]
replace h : Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := h
[GOAL]
R✝ : Type u_1
inst✝⁵ : Ring R✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_4
inst✝ : CommRing R
I : Ideal R
x y : R
f : R[X]
h : ↑(Ideal.Quotient.mk I) x = ↑(Ideal.Quotient.mk I) y
⊢ ↑(Ideal.Quotient.mk I) (Polynomial.eval x f) = ↑(Ideal.Quotient.mk I) (Polynomial.eval y f)
[PROOFSTEP]
rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval₂_at_apply, h]


[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(aeval f) (charpoly f) = 0
[PROOFSTEP]
apply (LinearEquiv.map_eq_zero_iff (algEquivMatrix (chooseBasis R M)).toLinearEquiv).1
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(AlgEquiv.toLinearEquiv (algEquivMatrix (chooseBasis R M))) (↑(aeval f) (charpoly f)) = 0
[PROOFSTEP]
rw [AlgEquiv.toLinearEquiv_apply, ← AlgEquiv.coe_algHom, ← Polynomial.aeval_algHom_apply _ _ _, charpoly_def]
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(aeval (↑↑(algEquivMatrix (chooseBasis R M)) f))
      (Matrix.charpoly (↑(toMatrix (chooseBasis R M) (chooseBasis R M)) f)) =
    0
[PROOFSTEP]
exact Matrix.aeval_self_charpoly _
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
⊢ f ^ k = ↑(aeval f) (X ^ k %ₘ charpoly f)
[PROOFSTEP]
rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
⊢ coeff (minpoly R f) 0 ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
⊢ False
[PROOFSTEP]
obtain ⟨P, hP⟩ := X_dvd_iff.2 h
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ False
[PROOFSTEP]
have hdegP : P.degree < (minpoly R f).degree := by
  rw [hP, mul_comm]
  refine' degree_lt_degree_mul_X fun h => _
  rw [h, mul_zero] at hP
  exact minpoly.ne_zero (isIntegral f) hP
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ degree P < degree (minpoly R f)
[PROOFSTEP]
rw [hP, mul_comm]
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ degree P < degree (P * X)
[PROOFSTEP]
refine' degree_lt_degree_mul_X fun h => _
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h✝ : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
h : P = 0
⊢ False
[PROOFSTEP]
rw [h, mul_zero] at hP
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h✝ : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = 0
h : P = 0
⊢ False
[PROOFSTEP]
exact minpoly.ne_zero (isIntegral f) hP
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
⊢ False
[PROOFSTEP]
have hPmonic : P.Monic :=
  by
  suffices (minpoly R f).Monic by rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
  exact minpoly.monic (isIntegral f)
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
⊢ Monic P
[PROOFSTEP]
suffices (minpoly R f).Monic by rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
this : Monic (minpoly R f)
⊢ Monic P
[PROOFSTEP]
rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
[GOAL]
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
⊢ Monic (minpoly R f)
[PROOFSTEP]
exact minpoly.monic (isIntegral f)
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
hPmonic : Monic P
⊢ False
[PROOFSTEP]
have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
hPmonic : Monic P
hzero : ↑(aeval f) (minpoly R f) = 0
⊢ False
[PROOFSTEP]
simp only [hP, mul_eq_comp, ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp, AlgHom.map_mul, zero_apply,
  Function.comp_apply] at hzero
[GOAL]
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
hf : Function.Injective ↑f
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : degree P < degree (minpoly R f)
hPmonic : Monic P
hzero : ∀ (x : M), ↑(↑(aeval f) P) x = 0
⊢ False
[PROOFSTEP]
exact not_le.2 hdegP (minpoly.min _ _ hPmonic (ext hzero))


[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)]


[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
p q : N
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i q)
[PROOFSTEP]
letI := (@Sum.inl_injective ι₁ ι₂).decidableEq
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
p q : N
this : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i q)
[PROOFSTEP]
letI := (@Sum.inr_injective ι₁ ι₂).decidableEq
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
p q : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i q)
[PROOFSTEP]
cases i
[GOAL]
case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
p q : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
val✝ : ι₁
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) q)
[PROOFSTEP]
simp [TensorProduct.add_tmul, TensorProduct.tmul_add]
[GOAL]
case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
p q : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
val✝ : ι₂
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) q)
[PROOFSTEP]
simp [TensorProduct.add_tmul, TensorProduct.tmul_add]
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
c : R
p : N
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p)
[PROOFSTEP]
letI := (@Sum.inl_injective ι₁ ι₂).decidableEq
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
c : R
p : N
this : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p)
[PROOFSTEP]
letI := (@Sum.inr_injective ι₁ ι₂).decidableEq
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
c : R
p : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p)
[PROOFSTEP]
cases i
[GOAL]
case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
c : R
p : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
val✝ : ι₁
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) p)
[PROOFSTEP]
simp [TensorProduct.smul_tmul', TensorProduct.tmul_smul]
[GOAL]
case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
c : R
p : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
val✝ : ι₂
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) p)
[PROOFSTEP]
simp [TensorProduct.smul_tmul', TensorProduct.tmul_smul]
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m₁ m₂ : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
⊢ domCoprod (m₁ + m₂) n = domCoprod m₁ n + domCoprod m₂ n
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m₁ m₂ : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
x✝ : ι₁ ⊕ ι₂ → N
⊢ ↑(domCoprod (m₁ + m₂) n) x✝ = ↑(domCoprod m₁ n + domCoprod m₂ n) x✝
[PROOFSTEP]
simp only [domCoprod_apply, TensorProduct.add_tmul, add_apply]
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
c : R
m : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
⊢ domCoprod (c • m) n = c • domCoprod m n
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
c : R
m : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
x✝ : ι₁ ⊕ ι₂ → N
⊢ ↑(domCoprod (c • m) n) x✝ = ↑(c • domCoprod m n) x✝
[PROOFSTEP]
simp only [domCoprod_apply, TensorProduct.smul_tmul', smul_apply]
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m : MultilinearMap R (fun x => N) N₁
n₁ n₂ : MultilinearMap R (fun x => N) N₂
⊢ domCoprod m (n₁ + n₂) = domCoprod m n₁ + domCoprod m n₂
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m : MultilinearMap R (fun x => N) N₁
n₁ n₂ : MultilinearMap R (fun x => N) N₂
x✝ : ι₁ ⊕ ι₂ → N
⊢ ↑(domCoprod m (n₁ + n₂)) x✝ = ↑(domCoprod m n₁ + domCoprod m n₂) x✝
[PROOFSTEP]
simp only [domCoprod_apply, TensorProduct.tmul_add, add_apply]
[GOAL]
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
c : R
m : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
⊢ domCoprod m (c • n) = c • domCoprod m n
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
c : R
m : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
x✝ : ι₁ ⊕ ι₂ → N
⊢ ↑(domCoprod m (c • n)) x✝ = ↑(c • domCoprod m n) x✝
[PROOFSTEP]
simp only [domCoprod_apply, TensorProduct.tmul_smul, smul_apply]