R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
⊢ b ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
⊢ ∀ ⦃x : (i : ι) → φ i⦄, (x ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)) → x ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
intro b hb
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ b ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
⊢ b ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
simp only [mem_iInf, mem_ker, proj_apply] at hb
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ∑ i in I, ↑(stdBasis R φ i) (b i) ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ b ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
rw [←
  show (∑ i in I, stdBasis R φ i (b i)) = b by
    ext i
    rw [Finset.sum_apply, ← stdBasis_same R φ i (b i)]
    refine Finset.sum_eq_single i (fun j _ ne => stdBasis_ne _ _ _ _ ne.symm _) ?_
    intro hiI
    rw [stdBasis_same]
    exact hb _ ((hu trivial).resolve_left hiI)]
no goals
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ∑ i in I, ↑(stdBasis R φ i) (b i) ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
exact sum_mem_biSup fun i _ => mem_range_self (stdBasis R φ i) (b i)
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ Finset.sum I (fun i => ↑(stdBasis R φ i) (b i)) i = b i
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ∑ i in I, ↑(stdBasis R φ i) (b i) = b
ext i
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ ∑ c in I, ↑(stdBasis R φ c) (b c) i = ↑(stdBasis R φ i) (b i) i
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ Finset.sum I (fun i => ↑(stdBasis R φ i) (b i)) i = b i
rw [Finset.sum_apply, ← stdBasis_same R φ i (b i)]
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ ¬i ∈ I → ↑(stdBasis R φ i) (b i) i = 0
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ ∑ c in I, ↑(stdBasis R φ c) (b c) i = ↑(stdBasis R φ i) (b i) i
refine Finset.sum_eq_single i (fun j _ ne => stdBasis_ne _ _ _ _ ne.symm _) ?_
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ ↑(stdBasis R φ i) (b i) i = 0
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ ¬i ∈ I → ↑(stdBasis R φ i) (b i) i = 0
intro hiI
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ b i = 0
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ ↑(stdBasis R φ i) (b i) i = 0
rw [stdBasis_same]
no goals
case h
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ b i = 0
exact hb _ ((hu trivial).resolve_left hiI)