α : Type u_1
β : Type ?u.2311
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur' q (_ : q.s ⊆ s ∪ q.s) = blur' q h
α : Type u_1
β : Type ?u.2311
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur s q = blur' q h
unfold blur
case e_s
α : Type u_1
β : Type ?u.2311
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s
α : Type u_1
β : Type ?u.2311
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur' q (_ : q.s ⊆ s ∪ q.s) = blur' q h
congr
no goals
case e_s
α : Type u_1
β : Type ?u.2311
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s
exact Set.union_eq_self_of_subset_right h