no goals
α : Type u_1
β : Type ?u.46826
γ : Type ?u.46829
ι : Type ?u.46832
M : Type u_2
M' : Type ?u.46838
N : Type ?u.46841
P : Type ?u.46844
G : Type ?u.46847
H : Type ?u.46850
R : Type ?u.46853
S : Type ?u.46856
inst✝ : Zero M
a a' : α
b : M
⊢ (single a b).support ⊆ {a}
classical show ite _ _ _ ⊆ _; split_ifs <;> [exact empty_subset _; exact Subset.refl _]
α : Type u_1
β : Type ?u.46826
γ : Type ?u.46829
ι : Type ?u.46832
M : Type u_2
M' : Type ?u.46838
N : Type ?u.46841
P : Type ?u.46844
G : Type ?u.46847
H : Type ?u.46850
R : Type ?u.46853
S : Type ?u.46856
inst✝ : Zero M
a a' : α
b : M
⊢ (if b = 0 then ∅ else {a}) ⊆ {a}
α : Type u_1
β : Type ?u.46826
γ : Type ?u.46829
ι : Type ?u.46832
M : Type u_2
M' : Type ?u.46838
N : Type ?u.46841
P : Type ?u.46844
G : Type ?u.46847
H : Type ?u.46850
R : Type ?u.46853
S : Type ?u.46856
inst✝ : Zero M
a a' : α
b : M
⊢ (single a b).support ⊆ {a}
show ite _ _ _ ⊆ _
no goals
α : Type u_1
β : Type ?u.46826
γ : Type ?u.46829
ι : Type ?u.46832
M : Type u_2
M' : Type ?u.46838
N : Type ?u.46841
P : Type ?u.46844
G : Type ?u.46847
H : Type ?u.46850
R : Type ?u.46853
S : Type ?u.46856
inst✝ : Zero M
a a' : α
b : M
⊢ (if b = 0 then ∅ else {a}) ⊆ {a}
split_ifs <;> [exact empty_subset _; exact Subset.refl _]