-- Mathlib/LinearAlgebra/Pi.lean
theorem iInf_ker_proj_le_iSup_range_single {I : Finset ι} {J : Set ι} (hu : Set.univ ⊆ ↑I ∪ J) :
    ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i) ≤ ⨆ i ∈ I, range (single R φ i) :=
  SetLike.le_def.2
    (by
      intro b hb
      simp only [mem_iInf, mem_ker, proj_apply] at hb
      rw [←
        show (∑ i ∈ I, Pi.single i (b i)) = b by
          ext i
          rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
          refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
          intro hiI
          rw [Pi.single_eq_same]
          exact hb _ ((hu trivial).resolve_left hiI)]
      exact sum_mem_biSup fun i _ => mem_range_self (single R φ i) (b i))

Proof state:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
⊢ ∑ c ∈ I, Pi.single c (b c) i = Pi.single i (b i) i

Tactic:
refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_

Result:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
⊢ i ∉ I → Pi.single i (b i) i = 0

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, ker (proj i)
⊢ b ∈ ⨆ i ∈ I, range (single R φ i)

Tactic:
simp only [mem_iInf, mem_ker, proj_apply] at hb

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
⊢ b ∈ ⨆ i ∈ I, range (single R φ i)

Proof state:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0

Tactic:
exact hb _ ((hu trivial).resolve_left hiI)

Result:
no goals

Proof state:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
hiI : i ∉ I
⊢ Pi.single i (b i) i = 0

Tactic:
rw [Pi.single_eq_same]

Result:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0

Proof state:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
⊢ (∑ i ∈ I, Pi.single i (b i)) i = b i

Tactic:
rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]

Result:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
⊢ ∑ c ∈ I, Pi.single c (b c) i = Pi.single i (b i) i

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, ker (proj i) → x ∈ ⨆ i ∈ I, range (single R φ i)

Tactic:
intro b hb

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, ker (proj i)
⊢ b ∈ ⨆ i ∈ I, range (single R φ i)

Proof state:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
⊢ i ∉ I → Pi.single i (b i) i = 0

Tactic:
intro hiI

Result:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
hiI : i ∉ I
⊢ Pi.single i (b i) i = 0

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
⊢ ∑ i ∈ I, Pi.single i (b i) = b

Tactic:
ext i

Result:
case h
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
i : ι
⊢ (∑ i ∈ I, Pi.single i (b i)) i = b i

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
⊢ ∑ i ∈ I, Pi.single i (b i) ∈ ⨆ i ∈ I, range (single R φ i)

Tactic:
exact sum_mem_biSup fun i _ => mem_range_self (single R φ i) (b i)

Result:
no goals

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
⊢ b ∈ ⨆ i ∈ I, range (single R φ i)

Tactic:
rw [←
  show (∑ i ∈ I, Pi.single i (b i)) = b by
    ext i
    rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
    refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
    intro hiI
    rw [Pi.single_eq_same]
    exact hb _ ((hu trivial).resolve_left hiI)]

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
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 ∈ J, b i = 0
⊢ ∑ i ∈ I, Pi.single i (b i) ∈ ⨆ i ∈ I, range (single R φ i)