[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
⊢ Option.isSome (toOption o) = true ↔ o.Dom
[PROOFSTEP]
by_cases h : o.Dom
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ Option.isSome (toOption o) = true ↔ o.Dom
[PROOFSTEP]
simp [h, toOption]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ Option.isSome (toOption o) = true ↔ o.Dom
[PROOFSTEP]
simp [h, toOption]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
⊢ Option.isNone (toOption o) = true ↔ ¬o.Dom
[PROOFSTEP]
by_cases h : o.Dom
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ Option.isNone (toOption o) = true ↔ ¬o.Dom
[PROOFSTEP]
simp [h, toOption]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ Option.isNone (toOption o) = true ↔ ¬o.Dom
[PROOFSTEP]
simp [h, toOption]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := pd, get := p } h₂
⊢ { Dom := od, get := o } = { Dom := pd, get := p }
[PROOFSTEP]
have t : od = pd := propext H1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := pd, get := p } h₂
t : od = pd
⊢ { Dom := od, get := o } = { Dom := pd, get := p }
[PROOFSTEP]
cases t
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := od, get := p } h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }
[PROOFSTEP]
rw [show o = p from funext fun p => H2 p p]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : ∀ (a : α), ¬a ∈ o
⊢ ∀ (a : α), a ∈ o ↔ a ∈ none
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
⊢ some x ≠ none
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
h : some x = none
⊢ False
[PROOFSTEP]
exact true_ne_false (congr_arg Dom h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
⊢ o ≠ none ↔ ∃ x, o = some x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
⊢ o ≠ none → ∃ x, o = some x
[PROOFSTEP]
rw [Ne, eq_none_iff', not_not]
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
⊢ o.Dom → ∃ x, o = some x
[PROOFSTEP]
exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
⊢ (∃ x, o = some x) → o ≠ none
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
⊢ some x ≠ none
[PROOFSTEP]
apply some_ne_none
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Part α
ha : a.Dom
b : α
h : get a ha = b
⊢ a = some b
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Part α
ha : a.Dom
b : α
h : a = some b
⊢ get a ha = b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Part α
ha : a.Dom
b : Part α
h : a = b
⊢ get a ha = get b (_ : b.Dom)
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ toOption o ↔ a ∈ o
[PROOFSTEP]
unfold toOption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ (a ∈ if h : o.Dom then Option.some (get o h) else Option.none) ↔ a ∈ o
[PROOFSTEP]
by_cases h : o.Dom
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ (a ∈ if h : o.Dom then Option.some (get o h) else Option.none) ↔ a ∈ o
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ (a ∈ if h : o.Dom then Option.some (get o h) else Option.none) ↔ a ∈ o
[PROOFSTEP]
simp [h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ get o (_ : o.Dom) = a ↔ a ∈ o
[PROOFSTEP]
exact ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ ¬a ∈ o
[PROOFSTEP]
exact mt Exists.fst h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ toOption o = Option.some a ↔ a ∈ o
[PROOFSTEP]
rw [← Option.mem_def, mem_toOption]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
⊢ Option.elim (toOption a) b f = if h : a.Dom then f (get a h) else b
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ Option.elim (toOption a) b f = f (get a h)
[PROOFSTEP]
rw [h.toOption]
[GOAL]
case pos
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ Option.elim (Option.some (get a h)) b f = f (get a h)
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim (toOption a) b f = b
[PROOFSTEP]
rw [Part.toOption_eq_none_iff.2 h]
[GOAL]
case neg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim Option.none b f = b
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
⊢ (↑Option.none).Dom ↔ Option.isSome Option.none = true
[PROOFSTEP]
simp [ofOption, none]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
a : α
⊢ (↑(Option.some a)).Dom ↔ Option.isSome (Option.some a) = true
[PROOFSTEP]
simp [ofOption]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
o : Option α
h₁ : (↑o).Dom
h₂ : { Dom := Option.isSome o = true, get := Option.get o }.Dom
⊢ get (↑o) h₁ = get { Dom := Option.isSome o = true, get := Option.get o } h₂
[PROOFSTEP]
cases o
[GOAL]
case none
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.isSome Option.none = true, get := Option.get Option.none }.Dom
⊢ get (↑Option.none) h₁ = get { Dom := Option.isSome Option.none = true, get := Option.get Option.none } h₂
[PROOFSTEP]
simp at h₂ 
[GOAL]
case some
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) }.Dom
⊢ get (↑(Option.some val✝)) h₁ =
    get { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) } h₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Option α
⊢ toOption ↑o = o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ toOption ↑Option.none = Option.none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
val✝ : α
⊢ toOption ↑(Option.some val✝) = Option.some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (fun o => toOption o) ↑o = toOption ↑o
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ toOption ↑o = toOption ↑o
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Part α), ⊥ ≤ a
[PROOFSTEP]
introv x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Part α
x : α
⊢ x ∈ ⊥ → x ∈ a
[PROOFSTEP]
rintro ⟨⟨_⟩, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
⊢ x ≤ y ∨ y ≤ x
[PROOFSTEP]
rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x
[PROOFSTEP]
rw [h]
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none
[PROOFSTEP]
left
[GOAL]
case inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y
[PROOFSTEP]
apply OrderBot.bot_le _
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x
[PROOFSTEP]
right
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x
[PROOFSTEP]
intro b' h₁
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
[PROOFSTEP]
rw [Part.eq_some_iff] at h₀ 
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
[PROOFSTEP]
have hx := hx _ h₀
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x
[PROOFSTEP]
have hy := hy _ h₁
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
hy : b' ∈ z
⊢ b' ∈ x
[PROOFSTEP]
have hx := Part.mem_unique hx hy
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx✝¹ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx✝ : b ∈ z
hy : b' ∈ z
hx : b = b'
⊢ b' ∈ x
[PROOFSTEP]
subst hx
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
hx : b ∈ z
h₁ : b ∈ y
hy : b ∈ z
⊢ b ∈ x
[PROOFSTEP]
exact h₀
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a : β
⊢ ¬a ∈ map f none
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
⊢ assert p f = f h
[PROOFSTEP]
dsimp [assert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } = f h
[PROOFSTEP]
cases h' : f h
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } = { Dom := Dom✝, get := get✝ }
[PROOFSTEP]
simp [h', mk.injEq, h, exists_prop_of_true, true_and]
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ HEq (fun ha => get✝ (_ : { Dom := Dom✝, get := get✝ }.Dom)) get✝
[PROOFSTEP]
apply Function.hfunext
[GOAL]
case mk.hα
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ (∃ h, (f h).Dom) = Dom✝
[PROOFSTEP]
simp only [h, h', exists_prop_of_true]
[GOAL]
case mk.h
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ ∀ (a : ∃ h, (f h).Dom) (a' : Dom✝), HEq a a' → HEq (get✝ (_ : { Dom := Dom✝, get := get✝ }.Dom)) (get✝ a')
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ assert p f = none
[PROOFSTEP]
dsimp [assert, none]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } =
    { Dom := False, get := fun t => False.rec (fun x => α) t }
[PROOFSTEP]
congr
[GOAL]
case h.e_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ h, (f h).Dom) = False
[PROOFSTEP]
simp only [h, not_false_iff, exists_prop_of_false]
[GOAL]
case h.e_3
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ HEq (fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom)) fun t => False.rec (fun x => α) t
[PROOFSTEP]
apply Function.hfunext
[GOAL]
case h.e_3.hα
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ h, (f h).Dom) = False
[PROOFSTEP]
simp only [h, not_false_iff, exists_prop_of_false]
[GOAL]
case h.e_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ ∀ (a : ∃ h, (f h).Dom) (a' : False),
    HEq a a' → HEq (get (f (_ : p)) (_ : (f (_ : p)).Dom)) (False.rec (fun x => α) a')
[PROOFSTEP]
simp at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
⊢ Part.bind o f = f (get o h)
[PROOFSTEP]
ext b
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ b ∈ Part.bind o f ↔ b ∈ f (get o h)
[PROOFSTEP]
simp only [Part.mem_bind_iff, exists_prop]
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) ↔ b ∈ f (get o h)
[PROOFSTEP]
refine' ⟨_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) → b ∈ f (get o h)
[PROOFSTEP]
rintro ⟨a, ha, hb⟩
[GOAL]
case H.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb : b ∈ f a
⊢ b ∈ f (get o h)
[PROOFSTEP]
rwa [Part.get_eq_of_mem ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
a : β
⊢ ¬a ∈ Part.bind none f
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
f : α → Part β
⊢ ∀ (a_1 : β), a_1 ∈ Part.bind (some a) f ↔ a_1 ∈ f a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ Part.bind o f = f a
[PROOFSTEP]
rw [eq_some_iff.2 h, bind_some]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x : Part α
⊢ ∀ (a : β), a ∈ Part.bind x (some ∘ f) ↔ a ∈ map f x
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
[PROOFSTEP]
by_cases h : o.Dom
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : o.Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
[PROOFSTEP]
simp_rw [h.toOption, h.bind]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : o.Dom
⊢ toOption (f (get o h)) = Option.elim (Option.some (get o h)) Option.none fun a => toOption (f a)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : ¬o.Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
[PROOFSTEP]
rw [Part.toOption_eq_none_iff.2 h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : ¬o.Dom
⊢ toOption (Part.bind o f) = Option.elim Option.none Option.none fun a => toOption (f a)
[PROOFSTEP]
exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ a ∈ Part.bind (Part.bind f g) k ↔ a ∈ Part.bind f fun x => Part.bind (g x) k
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ (∃ a_1, (∃ a, a ∈ f ∧ a_1 ∈ g a) ∧ a ∈ k a_1) ↔ ∃ a_1, a_1 ∈ f ∧ ∃ a_2, a_2 ∈ g a_1 ∧ a ∈ k a_2
[PROOFSTEP]
exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩, fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ Part.bind (map f x) g = Part.bind x fun y => g (f y)
[PROOFSTEP]
rw [← bind_some_eq_map, bind_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (Part.bind x fun x => Part.bind ((some ∘ f) x) g) = Part.bind x fun y => g (f y)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ map g (Part.bind x f) = Part.bind x fun y => map g (f y)
[PROOFSTEP]
rw [← bind_some_eq_map, bind_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ (Part.bind x fun x => Part.bind (f x) (some ∘ g)) = Part.bind x fun y => map g (f y)
[PROOFSTEP]
simp [bind_some_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
o : Part α
⊢ map g (map f o) = map (g ∘ f) o
[PROOFSTEP]
erw [← bind_some_eq_map, bind_map, bind_some_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ {α β : Type ?u.35509}, Functor.mapConst = Functor.map ∘ const β
[PROOFSTEP]
simp [Functor.mapConst, Functor.map]
  --Porting TODO : In Lean3 these were automatic by a tactic
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type ?u.35509
f : Part α✝
⊢ id <$> f = f
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type ?u.35509
Dom✝ : Prop
get✝ : Dom✝ → α✝
⊢ id <$> { Dom := Dom✝, get := get✝ } = { Dom := Dom✝, get := get✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type ?u.35509
x : Part α✝
y : Part β✝
⊢ (SeqLeft.seqLeft x fun x => y).Dom ↔ (Seq.seq (const β✝ <$> x) fun x => y).Dom
[PROOFSTEP]
simp [SeqLeft.seqLeft, Part.bind, assert, Seq.seq, const, (· <$> ·), and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type ?u.35509
x : Part α✝
y : Part β✝
⊢ (SeqRight.seqRight x fun x => y).Dom ↔ (Seq.seq (const α✝ id <$> x) fun x => y).Dom
[PROOFSTEP]
simp [SeqRight.seqRight, Part.bind, assert, Seq.seq, const, (· <$> ·), and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type ?u.35509
x : α✝ → β✝
y : Part α✝
⊢ (Seq.seq (pure x) fun x => y).Dom ↔ (x <$> y).Dom
[PROOFSTEP]
simp [Seq.seq, Part.bind, assert, (· <$> ·), pure]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type ?u.35509
x : Part (α✝ → β✝)
y : Part α✝
⊢ (do
        let x ← x
        x <$> y).Dom ↔
    (Seq.seq x fun x => y).Dom
[PROOFSTEP]
simp [(· >>= ·), Part.bind, assert, Seq.seq, get, (· <$> ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o
[PROOFSTEP]
rw [show f = id from funext H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o
[PROOFSTEP]
exact id_map o
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : Part α
⊢ Part.bind x some = x
[PROOFSTEP]
erw [bind_some_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : Part α
⊢ map (fun a => a) x = x
[PROOFSTEP]
simp [map_id']
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y
[PROOFSTEP]
intro h
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ (∀ (a : α), a ∈ x → f a ≤ y) → x >>= f ≤ y
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
⊢ ∀ (a : α), a ∈ x → f a ≤ y
[PROOFSTEP]
intro a h' b
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ f a → b ∈ y
[PROOFSTEP]
have h := h b
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ b ∈ f a → b ∈ y
[PROOFSTEP]
simp only [and_imp, exists_prop, bind_eq_bind, mem_bind_iff, exists_imp] at h 
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : ∀ (x_1 : α), x_1 ∈ x → b ∈ f x_1 → b ∈ y
⊢ b ∈ f a → b ∈ y
[PROOFSTEP]
apply h _ h'
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
⊢ x >>= f ≤ y
[PROOFSTEP]
intro b h'
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y
[PROOFSTEP]
simp only [exists_prop, bind_eq_bind, mem_bind_iff] at h' 
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : ∃ a, a ∈ x ∧ b ∈ f a
⊢ b ∈ y
[PROOFSTEP]
rcases h' with ⟨a, h₀, h₁⟩
[GOAL]
case mpr.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
a : α
h₀ : a ∈ x
h₁ : b ∈ f a
⊢ b ∈ y
[PROOFSTEP]
apply h _ h₀ _ h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o
[PROOFSTEP]
dsimp [restrict, mem_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, get o (_ : o.Dom) = a) ↔ p ∧ ∃ h, get o h = a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, get o (_ : o.Dom) = a) → p ∧ ∃ h, get o h = a
[PROOFSTEP]
rintro ⟨h₀, h₁⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : get o (_ : o.Dom) = a
⊢ p ∧ ∃ h, get o h = a
[PROOFSTEP]
exact ⟨h₀, ⟨_, h₁⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ h, get o h = a) → ∃ h_1, get o (_ : o.Dom) = a
[PROOFSTEP]
rintro ⟨h₀, _, h₂⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w✝ : o.Dom
h₂ : get o w✝ = a
⊢ ∃ h_1, get o (_ : o.Dom) = a
[PROOFSTEP]
exact ⟨h₀, h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ get (a * b)
      (_ : ∃ h, ((fun b_1 => (fun y => map y ((fun x => b) ())) (get ((fun x x_1 => x * x_1) <$> a) b_1)) h).Dom) =
    ma * mb
[PROOFSTEP]
simp [← ha.2, ← hb.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ get (a * b)
      (_ : ∃ h, ((fun b_1 => (fun y => map y ((fun x => b) ())) (get ((fun x x_1 => x * x_1) <$> a) b_1)) h).Dom) =
    get a (_ : a.Dom) * get b (_ : b.Dom)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul α
a b : α
⊢ some a * some b = some (a * b)
[PROOFSTEP]
simp [mul_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ma⁻¹ ∈ a⁻¹
[PROOFSTEP]
simp [inv_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1, a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma / mb ∈ a / b
[PROOFSTEP]
simp [div_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 / a = ma / mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ get (a / b) hab = get a (_ : a.Dom) / get b (_ : b.Dom)
[PROOFSTEP]
simp [div_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ get (Part.bind a fun y => map (fun x => y / x) b) (_ : (Part.bind a fun y => map (fun x => y / x) b).Dom) =
    get a (_ : a.Dom) / get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : α
⊢ some a / some b = some (a / b)
[PROOFSTEP]
simp [div_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma % mb ∈ a % b
[PROOFSTEP]
simp [mod_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 % a = ma % mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ get (a % b) hab = get a (_ : a.Dom) % get b (_ : b.Dom)
[PROOFSTEP]
simp [mod_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ get (Part.bind a fun y => map (fun x => y % x) b) (_ : (Part.bind a fun y => map (fun x => y % x) b).Dom) =
    get a (_ : a.Dom) % get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : α
⊢ some a % some b = some (a % b)
[PROOFSTEP]
simp [mod_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ++ mb ∈ a ++ b
[PROOFSTEP]
simp [append_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ++ a = ma ++ mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ get (a ++ b) hab = get a (_ : a.Dom) ++ get b (_ : b.Dom)
[PROOFSTEP]
simp [append_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y ++ x) b) (_ : (Part.bind a fun y => map (fun x => y ++ x) b).Dom) =
    get a (_ : a.Dom) ++ get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : α
⊢ some a ++ some b = some (a ++ b)
[PROOFSTEP]
simp [append_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∩ mb ∈ a ∩ b
[PROOFSTEP]
simp [inter_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∩ a = ma ∩ mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ get (a ∩ b) hab = get a (_ : a.Dom) ∩ get b (_ : b.Dom)
[PROOFSTEP]
simp [inter_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y ∩ x) b) (_ : (Part.bind a fun y => map (fun x => y ∩ x) b).Dom) =
    get a (_ : a.Dom) ∩ get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : α
⊢ some a ∩ some b = some (a ∩ b)
[PROOFSTEP]
simp [inter_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∪ mb ∈ a ∪ b
[PROOFSTEP]
simp [union_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∪ a = ma ∪ mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ get (a ∪ b) hab = get a (_ : a.Dom) ∪ get b (_ : b.Dom)
[PROOFSTEP]
simp [union_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y ∪ x) b) (_ : (Part.bind a fun y => map (fun x => y ∪ x) b).Dom) =
    get a (_ : a.Dom) ∪ get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : α
⊢ some a ∪ some b = some (a ∪ b)
[PROOFSTEP]
simp [union_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma \ mb ∈ a \ b
[PROOFSTEP]
simp [sdiff_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 \ a = ma \ mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ get (a \ b) hab = get a (_ : a.Dom) \ get b (_ : b.Dom)
[PROOFSTEP]
simp [sdiff_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y \ x) b) (_ : (Part.bind a fun y => map (fun x => y \ x) b).Dom) =
    get a (_ : a.Dom) \ get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : α
⊢ some a \ some b = some (a \ b)
[PROOFSTEP]
simp [sdiff_def]
