case h.a.h
α : Type u_1
M : Type u_2
N : Type ?u.73225
P : Type ?u.73228
R : Type u_3
S : Type ?u.73234
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
s : Set α
l : { x // x ∈ supported M R s }
a : α
⊢ ↑↑(↑(comp (restrictDom M R s) (Submodule.subtype (supported M R s))) l) a = ↑↑(↑LinearMap.id l) a
α : Type u_1
M : Type u_2
N : Type ?u.73225
P : Type ?u.73228
R : Type u_3
S : Type ?u.73234
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
s : Set α
⊢ comp (restrictDom M R s) (Submodule.subtype (supported M R s)) = LinearMap.id
ext (l a)
case neg
α : Type u_1
M : Type u_2
N : Type ?u.73225
P : Type ?u.73228
R : Type u_3
S : Type ?u.73234
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
s : Set α
l : { x // x ∈ supported M R s }
a : α
h : ¬a ∈ s
⊢ 0 = ↑↑l a
case h.a.h
α : Type u_1
M : Type u_2
N : Type ?u.73225
P : Type ?u.73228
R : Type u_3
S : Type ?u.73234
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
s : Set α
l : { x // x ∈ supported M R s }
a : α
⊢ ↑↑(↑(comp (restrictDom M R s) (Submodule.subtype (supported M R s))) l) a = ↑↑(↑LinearMap.id l) a
by_cases h : a ∈ s <;> simp [h]
no goals
case neg
α : Type u_1
M : Type u_2
N : Type ?u.73225
P : Type ?u.73228
R : Type u_3
S : Type ?u.73234
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
s : Set α
l : { x // x ∈ supported M R s }
a : α
h : ¬a ∈ s
⊢ 0 = ↑↑l a
exact ((mem_supported' R l.1).1 l.2 a h).symm