no goals
α : Type u_2
β : Type ?u.488182
γ : Type ?u.488185
ι : Type ?u.488188
M : Type u_3
M' : Type ?u.488194
N : Type u_1
P : Type ?u.488200
G : Type ?u.488203
H : Type ?u.488206
R : Type ?u.488209
S : Type ?u.488212
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ (x : α), x ∈ v.support → p x
x✝ : Subtype p
⊢ ∀ (ha : x✝ ∈ (subtypeDomain p v).support), (fun p_1 x => ↑p_1) x✝ ha ∈ v.support
classical exact mem_subtype.1
no goals
α : Type u_2
β : Type ?u.488182
γ : Type ?u.488185
ι : Type ?u.488188
M : Type u_3
M' : Type ?u.488194
N : Type u_1
P : Type ?u.488200
G : Type ?u.488203
H : Type ?u.488206
R : Type ?u.488209
S : Type ?u.488212
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ (x : α), x ∈ v.support → p x
x✝ : Subtype p
⊢ ∀ (ha : x✝ ∈ (subtypeDomain p v).support), (fun p_1 x => ↑p_1) x✝ ha ∈ v.support
exact mem_subtype.1
no goals
α : Type u_2
β : Type ?u.488182
γ : Type ?u.488185
ι : Type ?u.488188
M : Type u_3
M' : Type ?u.488194
N : Type u_1
P : Type ?u.488200
G : Type ?u.488203
H : Type ?u.488206
R : Type ?u.488209
S : Type ?u.488212
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ (x : α), x ∈ v.support → p x
b : α
hb : b ∈ v.support
⊢ { val := b, property := (_ : p b) } ∈ (subtypeDomain p v).support
classical exact mem_subtype.2 hb
no goals
α : Type u_2
β : Type ?u.488182
γ : Type ?u.488185
ι : Type ?u.488188
M : Type u_3
M' : Type ?u.488194
N : Type u_1
P : Type ?u.488200
G : Type ?u.488203
H : Type ?u.488206
R : Type ?u.488209
S : Type ?u.488212
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ (x : α), x ∈ v.support → p x
b : α
hb : b ∈ v.support
⊢ { val := b, property := (_ : p b) } ∈ (subtypeDomain p v).support
exact mem_subtype.2 hb