[GOAL]
α : Type u_1
β : Type u_2
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s
[PROOFSTEP]
refine' ⟨congr_arg _, fun h => _⟩
[GOAL]
α : Type u_1
β : Type u_2
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
⊢ q₁ = q₂
[PROOFSTEP]
cases' q₁ with _ v₁
[GOAL]
case mk'
α : Type u_1
β : Type u_2
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂
[PROOFSTEP]
cases' q₂ with _ v₂
[GOAL]
case mk'.mk'
α : Type u_1
β : Type u_2
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }
[PROOFSTEP]
congr
[GOAL]
case mk'.mk'.h.e_3
α : Type u_1
β : Type u_2
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ HEq v₁ v₂
[PROOFSTEP]
exact Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur s q = blur' q h
[PROOFSTEP]
unfold blur
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur' q (_ : q.s ⊆ s ∪ q.s) = blur' q h
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u_1
β : Type u_2
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s
[PROOFSTEP]
exact Set.union_eq_self_of_subset_right h
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f a = f b
a : α
aq : a ∈ q
⊢ liftOn q f h = f a
[PROOFSTEP]
revert h
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f a = f b), liftOn q f h = f a
[PROOFSTEP]
rw [eq_mk_of_mem aq]
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ (a_1 : α), a_1 ∈ mk aq → ∀ (b : α), b ∈ mk aq → f a_1 = f b), liftOn (mk aq) f h = f a
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ (a_1 : α), a_1 ∈ mk aq → ∀ (b : α), b ∈ mk aq → f a_1 = f b
⊢ liftOn (mk aq) f h✝ = f a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ bind q f ↔ ∃ a, a ∈ q ∧ b ∈ f a
[PROOFSTEP]
simp_rw [← exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ bind q f ↔ ∃ a _h, b ∈ f a
[PROOFSTEP]
exact Set.mem_iUnion₂
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type ?u.6544
q : Semiquot α
⊢ ∀ (a : α), a ∈ id <$> q ↔ a ∈ q
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β : Type ?u.6544
x : α
f : α → Semiquot β
⊢ ∀ (a : β), a ∈ pure x >>= f ↔ a ∈ f x
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β γ : Type ?u.6544
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), a ∈ s >>= f >>= g ↔ a ∈ s >>= fun x => f x >>= g
[PROOFSTEP]
simp only [bind_def, mem_bind]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β γ : Type ?u.6544
s : Semiquot α
f : α → Semiquot β
g : β → Semiquot γ
⊢ ∀ (a : γ), (∃ a_1, (∃ a, a ∈ s ∧ a_1 ∈ f a) ∧ a ∈ g a_1) ↔ ∃ a_1, a_1 ∈ s ∧ ∃ a_2, a_2 ∈ f a_1 ∧ a ∈ g a_2
[PROOFSTEP]
exact fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩, fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β : Type ?u.6544
f : α → β
s : Semiquot α
⊢ ∀ (a : β),
    (a ∈ do
        let y ← s
        pure (f y)) ↔
      a ∈ f <$> s
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
⊢ get q p ∈ q
[PROOFSTEP]
let ⟨a, h⟩ := exists_mem q
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
h : a ∈ q
⊢ get q p ∈ q
[PROOFSTEP]
unfold get
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
h : a ∈ q
⊢ liftOn q id p ∈ q
[PROOFSTEP]
rw [liftOn_ofMem q _ _ a h]
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
h : a ∈ q
⊢ id a ∈ q
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
⊢ a ∈ q ↔ a ∈ pure (get q p)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
q : Semiquot α
p : IsPure q
a : α
⊢ a ∈ q ↔ a = get q p
[PROOFSTEP]
exact ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩
[GOAL]
α : Type u_1
β : Type u_2
a b : α
ab : b ∈ pure a
c : α
ac : c ∈ pure a
⊢ b = c
[PROOFSTEP]
rw [mem_pure] at ab ac 
[GOAL]
α : Type u_1
β : Type u_2
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c
[PROOFSTEP]
rwa [← ac] at ab 
[GOAL]
α : Type u_1
β : Type u_2
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ t ≤ s
[PROOFSTEP]
rw [eq_pure h, eq_pure (h.mono st)]
[GOAL]
α : Type u_1
β : Type u_2
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ pure (get t h) ≤ pure (get s (_ : IsPure s))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ get t h = get s (_ : IsPure s)
[PROOFSTEP]
exact h _ (get_mem _) _ (st <| get_mem _)
