-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem biSup_eq_range_dfinsupp_lsum (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) :
    ⨆ (i) (_ : p i), S i =
      LinearMap.range
        (LinearMap.comp
          (DFinsupp.lsum ℕ (M := fun i ↦ ↥(S i)) (fun i => (S i).subtype))
            (DFinsupp.filterLinearMap R _ p))

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ ⨆ i, ⨆ (_ : p i), S i = LinearMap.range (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p)

Tactic:
apply le_antisymm

Result:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ ⨆ i, ⨆ (_ : p i), S i ≤ LinearMap.range (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p)

case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ LinearMap.range (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p) ≤ ⨆ i, ⨆ (_ : p i), S i

Proof state:
case neg
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i => ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ ((fun i => (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
simp [hp]

Result:
no goals

Proof state:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ ⨆ i, ⨆ (_ : p i), S i ≤ LinearMap.range (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p)

Tactic:
refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩

Result:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p) (single i ⟨y, hy⟩) = y

Proof state:
case pos
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i => ↥(S i)) p) v) i ≠ 0
hp : p i
⊢ ((fun i => (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
simp [hp]

Result:
no goals

Proof state:
case a.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i => ↥(S i)) p) v) i ≠ 0
⊢ ((fun i => (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i => ↥(S i)) p) v) i) ∈ ⨆ i, ⨆ (_ : p i), S i

Tactic:
refine mem_iSup_of_mem i ?_

Result:
case a.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i => ↥(S i)) p) v) i ≠ 0
⊢ ((fun i => (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Proof state:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ LinearMap.range (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p) ≤ ⨆ i, ⨆ (_ : p i), S i

Tactic:
rintro x ⟨v, rfl⟩

Result:
case a.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
⊢ (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p) v ∈ ⨆ i, ⨆ (_ : p i), S i

Proof state:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ((lsum ℕ) fun i => (S i).subtype) (single i ⟨y, hy⟩) = y

Tactic:
simp only [lsum_apply_apply, sumAddHom_single, LinearMap.toAddMonoidHom_coe, coe_subtype]

Result:
no goals

Proof state:
case a.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i => ↥(S i)) p) v) i ≠ 0
⊢ ((fun i => (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
by_cases hp : p i

Result:
case pos
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i => ↥(S i)) p) v) i ≠ 0
hp : p i
⊢ ((fun i => (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

case neg
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i => ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ ((fun i => (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i => ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Proof state:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p) (single i ⟨y, hy⟩) = y

Tactic:
rw [LinearMap.comp_apply, filterLinearMap_apply, filter_single_pos _ _ hi]

Result:
case a
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ((lsum ℕ) fun i => (S i).subtype) (single i ⟨y, hy⟩) = y

Proof state:
case a.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
⊢ (((lsum ℕ) fun i => (S i).subtype) ∘ₗ filterLinearMap R (fun i => ↥(S i)) p) v ∈ ⨆ i, ⨆ (_ : p i), S i

Tactic:
refine dfinsupp_sumAddHom_mem _ _ _ fun i _ => ?_

Result:
case a.intro
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i => ↥(S i)) p) v) i ≠ 0
⊢ ((fun i => (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i => ↥(S i)) p) v) i) ∈ ⨆ i, ⨆ (_ : p i), S i