α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
⊢ supported M R (⋃ (i : δ), s i) ≤ ⨆ (i : δ), supported M R (s i)
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
⊢ supported M R (⋃ (i : δ), s i) = ⨆ (i : δ), supported M R (s i)
refine' le_antisymm _ (iSup_le fun i => supported_mono <| Set.subset_iUnion _ _)
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
⊢ supported M R (⋃ (i : δ), s i) ≤ ⨆ (i : δ), supported M R (s i)
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
⊢ supported M R (⋃ (i : δ), s i) ≤ ⨆ (i : δ), supported M R (s i)
haveI := Classical.decPred fun x => x ∈ ⋃ i, s i
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
⊢ LinearMap.range (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i))) ≤
    ⨆ (i : δ), supported M R (s i)
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
⊢ supported M R (⋃ (i : δ), s i) ≤ ⨆ (i : δ), supported M R (s i)
suffices
  LinearMap.range ((Submodule.subtype _).comp (restrictDom M R (⋃ i, s i))) ≤
    ⨆ i, supported M R (s i) by
  rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
⊢ ⊤ ≤
    comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
      (⨆ (i : δ), supported M R (s i))
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
⊢ LinearMap.range (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i))) ≤
    ⨆ (i : δ), supported M R (s i)
rw [range_le_iff_comap, eq_top_iff]
case intro
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l : α →₀ M
⊢ l ∈
    comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
      (⨆ (i : δ), supported M R (s i))
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
⊢ ⊤ ≤
    comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
      (⨆ (i : δ), supported M R (s i))
rintro l ⟨⟩
case intro.refine_1
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l : α →₀ M
⊢ 0 ∈
    comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
      (⨆ (i : δ), supported M R (s i))

case intro.refine_2
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l : α →₀ M
⊢ ∀ (a : α) (b : M) (f : α →₀ M),
    ¬a ∈ f.support →
      b ≠ 0 →
        f ∈
            comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
              (⨆ (i : δ), supported M R (s i)) →
          single a b + f ∈
            comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
              (⨆ (i : δ), supported M R (s i))
case intro
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l : α →₀ M
⊢ l ∈
    comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
      (⨆ (i : δ), supported M R (s i))
refine Finsupp.induction l ?_ ?_
no goals
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this✝ : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
this :
  LinearMap.range (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i))) ≤
    ⨆ (i : δ), supported M R (s i)
⊢ supported M R (⋃ (i : δ), s i) ≤ ⨆ (i : δ), supported M R (s i)
rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
no goals
case intro.refine_1
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l : α →₀ M
⊢ 0 ∈
    comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
      (⨆ (i : δ), supported M R (s i))
exact zero_mem _
case intro.refine_2
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : ¬x ∈ l.support
x✝ : a ≠ 0
⊢ single x a ∈
    comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
      (⨆ (i : δ), supported M R (s i))
case intro.refine_2
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l : α →₀ M
⊢ ∀ (a : α) (b : M) (f : α →₀ M),
    ¬a ∈ f.support →
      b ≠ 0 →
        f ∈
            comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
              (⨆ (i : δ), supported M R (s i)) →
          single a b + f ∈
            comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
              (⨆ (i : δ), supported M R (s i))
refine' fun x a l _ _ => add_mem _
case pos
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : ¬x ∈ l.support
x✝ : a ≠ 0
h : ∃ i, x ∈ s i
⊢ single x a ∈ ⨆ (i : δ), supported M R (s i)
case intro.refine_2
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : ¬x ∈ l.support
x✝ : a ≠ 0
⊢ single x a ∈
    comap (comp (Submodule.subtype (supported M R (⋃ (i : δ), s i))) (restrictDom M R (⋃ (i : δ), s i)))
      (⨆ (i : δ), supported M R (s i))
by_cases h : ∃ i, x ∈ s i <;> simp [h]
case pos.intro
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : ¬x ∈ l.support
x✝ : a ≠ 0
i : δ
hi : x ∈ s i
⊢ single x a ∈ ⨆ (i : δ), supported M R (s i)
case pos
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : ¬x ∈ l.support
x✝ : a ≠ 0
h : ∃ i, x ∈ s i
⊢ single x a ∈ ⨆ (i : δ), supported M R (s i)
cases' h with i hi
no goals
case pos.intro
α : Type u_2
M : Type u_3
N : Type ?u.93459
P : Type ?u.93462
R : Type u_4
S : Type ?u.93468
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
δ : Type u_1
s : δ → Set α
this : DecidablePred fun x => x ∈ ⋃ (i : δ), s i
l✝ : α →₀ M
x : α
a : M
l : α →₀ M
x✝¹ : ¬x ∈ l.support
x✝ : a ≠ 0
i : δ
hi : x ∈ s i
⊢ single x a ∈ ⨆ (i : δ), supported M R (s i)
exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)