[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
y : β
o : Option α
⊢ y ∈ Option.map f o ↔ ∃ x, x ∈ o ∧ f x = y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
H : Function.Injective f
a : α
o : Option α
⊢ f a ∈ Option.map f o ↔ a ∈ o
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
o : Option α
p : β → Prop
⊢ (∀ (y : β), y ∈ Option.map f o → p y) ↔ ∀ (x : α), x ∈ o → p (f x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
o : Option α
p : β → Prop
⊢ (∃ y, y ∈ Option.map f o ∧ p y) ↔ ∃ x, x ∈ o ∧ p (f x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
Hf : Function.Injective f
a₁ a₂ : α
H : Option.map f (some a₁) = Option.map f (some a₂)
⊢ some a₁ = some a₂
[PROOFSTEP]
rw [Hf (Option.some.inj H)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x : Option α
f : α → Option β
b : β
⊢ Option.bind x f = some b ↔ ∃ a, x = some a ∧ f a = some b
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → Option β
b : β
⊢ Option.bind none f = some b ↔ ∃ a, none = some a ∧ f a = some b
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → Option β
b : β
val✝ : α
⊢ Option.bind (some val✝) f = some b ↔ ∃ a, some val✝ = some a ∧ f a = some b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o : Option α
f : α → Option β
⊢ Option.bind o f = none ↔ ∀ (b : β) (a : α), a ∈ o → ¬b ∈ f a
[PROOFSTEP]
simp only [eq_none_iff_forall_not_mem, mem_def, bind_eq_some, not_exists, not_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f g : α → β
h : Option.map f = Option.map g
x : α
⊢ some (f x) = some (g x)
[PROOFSTEP]
simp only [← map_some', h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))
[PROOFSTEP]
rw [map_map, h, ← map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : α → Option β
x : Option α
⊢ (pbind x fun a x => f a) = Option.bind x f
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : α → Option β
⊢ (pbind none fun a x => f a) = Option.bind none f
[PROOFSTEP]
simp only [pbind, none_bind', some_bind']
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : α → Option β
val✝ : α
⊢ (pbind (some val✝) fun a x => f a) = Option.bind (some val✝) f
[PROOFSTEP]
simp only [pbind, none_bind', some_bind']
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p : α✝ → Prop
f✝ : (a : α✝) → p a → β✝
x✝ : Option α✝
α β γ : Type u_5
f : β → γ
x : Option α
g : α → Option β
⊢ Option.map f (x >>= g) = do
    let a ← x
    Option.map f (g a)
[PROOFSTEP]
simp only [← map_eq_map, ← bind_pure_comp, LawfulMonad.bind_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : β → γ
x : Option α
g : α → Option β
⊢ Option.map f (Option.bind x g) = Option.bind x fun a => Option.map f (g a)
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : β → γ
g : α → Option β
⊢ Option.map f (Option.bind none g) = Option.bind none fun a => Option.map f (g a)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : β → γ
g : α → Option β
val✝ : α
⊢ Option.map f (Option.bind (some val✝) g) = Option.bind (some val✝) fun a => Option.map f (g a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : β → γ
x : Option α
g : (a : α) → a ∈ x → Option β
⊢ Option.map f (pbind x g) = pbind x fun a H => Option.map f (g a H)
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : β → γ
g : (a : α) → a ∈ none → Option β
⊢ Option.map f (pbind none g) = pbind none fun a H => Option.map f (g a H)
[PROOFSTEP]
simp only [pbind, map_none']
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : β → γ
val✝ : α
g : (a : α) → a ∈ some val✝ → Option β
⊢ Option.map f (pbind (some val✝) g) = pbind (some val✝) fun a H => Option.map f (g a H)
[PROOFSTEP]
simp only [pbind, map_none']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : α → β
x : Option α
g : (b : β) → b ∈ Option.map f x → Option γ
⊢ pbind (Option.map f x) g = pbind x fun a h => g (f a) (_ : f a ∈ Option.map f x)
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : α → β
g : (b : β) → b ∈ Option.map f none → Option γ
⊢ pbind (Option.map f none) g = pbind none fun a h => g (f a) (_ : f a ∈ Option.map f none)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : α → β
val✝ : α
g : (b : β) → b ∈ Option.map f (some val✝) → Option γ
⊢ pbind (Option.map f (some val✝)) g = pbind (some val✝) fun a h => g (f a) (_ : f a ∈ Option.map f (some val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ f a (_ : p a) ∈ pmap f x h
[PROOFSTEP]
rw [mem_def] at ha ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a (_ : p a))
[PROOFSTEP]
subst ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
ha : a ∈ some a
⊢ pmap f (some a) h = some (f a (_ : p a))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x✝ : Option α
g : γ → α
x : Option γ
H : ∀ (a : α), a ∈ Option.map g x → p a
⊢ pmap f (Option.map g x) H = pmap (fun a h => f (g a) h) x (_ : ∀ (a : γ), a ∈ x → p (g a))
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : γ → α
H : ∀ (a : α), a ∈ Option.map g none → p a
⊢ pmap f (Option.map g none) H = pmap (fun a h => f (g a) h) none (_ : ∀ (a : γ), a ∈ none → p (g a))
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : γ → α
val✝ : γ
H : ∀ (a : α), a ∈ Option.map g (some val✝) → p a
⊢ pmap f (Option.map g (some val✝)) H = pmap (fun a h => f (g a) h) (some val✝) (_ : ∀ (a : γ), a ∈ some val✝ → p (g a))
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
g : β → γ
f : (a : α) → p a → β
x : Option α
H : ∀ (a : α), a ∈ x → p a
⊢ Option.map g (pmap f x H) = pmap (fun a h => g (f a h)) x H
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
g : β → γ
f : (a : α) → p a → β
H : ∀ (a : α), a ∈ none → p a
⊢ Option.map g (pmap f none H) = pmap (fun a h => g (f a h)) none H
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
g : β → γ
f : (a : α) → p a → β
val✝ : α
H : ∀ (a : α), a ∈ some val✝ → p a
⊢ Option.map g (pmap f (some val✝) H) = pmap (fun a h => g (f a h)) (some val✝) H
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p✝ : α → Prop
f✝ : (a : α) → p✝ a → β
x✝ : Option α
p : α → Prop
f : α → β
x : Option α
H : ∀ (a : α), a ∈ x → p a
⊢ pmap (fun a x => f a) x H = Option.map f x
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p✝ : α → Prop
f✝ : (a : α) → p✝ a → β
x : Option α
p : α → Prop
f : α → β
H : ∀ (a : α), a ∈ none → p a
⊢ pmap (fun a x => f a) none H = Option.map f none
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p✝ : α → Prop
f✝ : (a : α) → p✝ a → β
x : Option α
p : α → Prop
f : α → β
val✝ : α
H : ∀ (a : α), a ∈ some val✝ → p a
⊢ pmap (fun a x => f a) (some val✝) H = Option.map f (some val✝)
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x✝ : Option α✝
α β γ : Type u_5
x : Option α
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
H : ∀ (a : β), a ∈ x >>= g → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ x >>= g
⊢ pmap f (x >>= g) H = do
    let a ← x
    pmap f (g a) (_ : ∀ (b : β), b ∈ g a → p b)
[PROOFSTEP]
cases x
[GOAL]
case none
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x : Option α✝
α β γ : Type u_5
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
H : ∀ (a : β), a ∈ none >>= g → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ none >>= g
⊢ pmap f (none >>= g) H = do
    let a ← none
    pmap f (g a) (_ : ∀ (b : β), b ∈ g a → p b)
[PROOFSTEP]
simp only [pmap, bind_eq_bind, none_bind, some_bind]
[GOAL]
case some
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x : Option α✝
α β γ : Type u_5
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
val✝ : α
H : ∀ (a : β), a ∈ some val✝ >>= g → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ some val✝ >>= g
⊢ pmap f (some val✝ >>= g) H = do
    let a ← some val✝
    pmap f (g a) (_ : ∀ (b : β), b ∈ g a → p b)
[PROOFSTEP]
simp only [pmap, bind_eq_bind, none_bind, some_bind]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x✝ : Option α✝
α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : β → Option γ
H : ∀ (a : α), a ∈ x → p a
⊢ pmap f x H >>= g = pbind x fun a h => g (f a (_ : p a))
[PROOFSTEP]
cases x
[GOAL]
case none
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x : Option α✝
α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
g : β → Option γ
H : ∀ (a : α), a ∈ none → p a
⊢ pmap f none H >>= g = pbind none fun a h => g (f a (_ : p a))
[PROOFSTEP]
simp only [pmap, bind_eq_bind, none_bind, some_bind, pbind]
[GOAL]
case some
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x : Option α✝
α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
g : β → Option γ
val✝ : α
H : ∀ (a : α), a ∈ some val✝ → p a
⊢ pmap f (some val✝) H >>= g = pbind (some val✝) fun a h => g (f a (_ : p a))
[PROOFSTEP]
simp only [pmap, bind_eq_bind, none_bind, some_bind, pbind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → a ∈ x → Option β
h' : ∀ (a : α) (H : a ∈ x), f a H = none → x = none
⊢ pbind x f = none ↔ x = none
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
f : (a : α) → a ∈ none → Option β
h' : ∀ (a : α) (H : a ∈ none), f a H = none → none = none
⊢ pbind none f = none ↔ none = none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ pbind (some val✝) f = none ↔ some val✝ = none
[PROOFSTEP]
simp only [pbind, iff_false]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ ¬f val✝ (_ : some val✝ = some val✝) = none
[PROOFSTEP]
intro h
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
h : f val✝ (_ : some val✝ = some val✝) = none
⊢ False
[PROOFSTEP]
cases h' _ rfl h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → a ∈ x → Option β
y : β
⊢ pbind x f = some y ↔ ∃ z H, f z H = some y
[PROOFSTEP]
rcases x with (_ | x)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
⊢ pbind none f = some y ↔ ∃ z H, f z H = some y
[PROOFSTEP]
simp only [pbind, false_iff, not_exists]
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
⊢ ∀ (x : α) (x_1 : x ∈ none), ¬f x x_1 = some y
[PROOFSTEP]
intro z h
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
z : α
h : z ∈ none
⊢ ¬f z h = some y
[PROOFSTEP]
simp at h 
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ pbind (some x) f = some y ↔ ∃ z H, f z H = some y
[PROOFSTEP]
simp only [pbind]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ f x (_ : some x = some x) = some y ↔ ∃ z H, f z H = some y
[PROOFSTEP]
refine ⟨λ h => ⟨x, rfl, h⟩, ?_⟩
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ (∃ z H, f z H = some y) → f x (_ : some x = some x) = some y
[PROOFSTEP]
rintro ⟨z, H, hz⟩
[GOAL]
case some.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H : z ∈ some x
hz : f z H = some y
⊢ f x (_ : some x = some x) = some y
[PROOFSTEP]
simp only [mem_def, Option.some_inj] at H 
[GOAL]
case some.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H✝ : z ∈ some x
hz : f z H✝ = some y
H : x = z
⊢ f x (_ : some x = some x) = some y
[PROOFSTEP]
simpa [H] using hz
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
h : ∀ (a : α), a ∈ x → p a
⊢ pmap f x h = none ↔ x = none
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ none → p a
⊢ pmap f none h = none ↔ none = none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
val✝ : α
h : ∀ (a : α), a ∈ some val✝ → p a
⊢ pmap f (some val✝) h = none ↔ some val✝ = none
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
hf : ∀ (a : α), a ∈ x → p a
y : β
⊢ pmap f x hf = some y ↔ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
rcases x with (_ | x)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
hf : ∀ (a : α), a ∈ none → p a
⊢ pmap f none hf = some y ↔ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
simp only [not_mem_none, exists_false, pmap, not_false_iff, exists_prop_of_false]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
⊢ pmap f (some x) hf = some y ↔ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
constructor
[GOAL]
case some.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
⊢ pmap f (some x) hf = some y → ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
intro h
[GOAL]
case some.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
h : pmap f (some x) hf = some y
⊢ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
simp only [pmap, Option.some_inj] at h 
[GOAL]
case some.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
h : f x (_ : p x) = y
⊢ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
refine ⟨x, rfl, h⟩
[GOAL]
case some.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
⊢ (∃ a H, f a (_ : p a) = y) → pmap f (some x) hf = some y
[PROOFSTEP]
rintro ⟨a, H, rfl⟩
[GOAL]
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : α
hf : ∀ (a : α), a ∈ some x → p a
a : α
H : some x = some a
⊢ pmap f (some x) hf = some (f a (_ : p a))
[PROOFSTEP]
simp only [mem_def, Option.some_inj] at H 
[GOAL]
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : α
hf : ∀ (a : α), a ∈ some x → p a
a : α
H✝ : some x = some a
H : x = a
⊢ pmap f (some x) hf = some (f a (_ : p a))
[PROOFSTEP]
simp only [H, pmap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : (a : α) → p a → β
x : Option (Option α)
H : ∀ (a : Option α), a ∈ x → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) x H) = pmap f (join x) (_ : ∀ (a : α), a ∈ join x → p a)
[PROOFSTEP]
rcases x with (_ | _ | x)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → p a → β
H : ∀ (a : Option α), a ∈ none → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) none H) = pmap f (join none) (_ : ∀ (a : α), a ∈ join none → p a)
[PROOFSTEP]
simp
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → p a → β
H : ∀ (a : Option α), a ∈ some none → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) (some none) H) = pmap f (join (some none)) (_ : ∀ (a : α), a ∈ join (some none) → p a)
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : (a : α) → p a → β
x : α
H : ∀ (a : Option α), a ∈ some (some x) → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) (some (some x)) H) = pmap f (join (some (some x))) (_ : ∀ (a : α), a ∈ join (some (some x)) → p a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x : Option α
⊢ (Option.orElse none fun x_1 => x) = x
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
⊢ (Option.orElse none fun x => none) = none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
val✝ : α
⊢ (Option.orElse none fun x => some val✝) = some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x : Option α
⊢ (Option.orElse x fun x => none) = x
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
⊢ (Option.orElse none fun x => none) = none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
val✝ : α
⊢ (Option.orElse (some val✝) fun x => none) = some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Inhabited α
o : Option α
⊢ getD o default = iget o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Inhabited α
⊢ getD none default = iget none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Inhabited α
val✝ : α
⊢ getD (some val✝) default = iget (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : Prop
inst✝ : Decidable p
u : Unit
⊢ _root_.guard p = some u ↔ p
[PROOFSTEP]
cases u
[GOAL]
case unit
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : Prop
inst✝ : Decidable p
⊢ _root_.guard p = some PUnit.unit ↔ p
[PROOFSTEP]
by_cases h : p
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : Prop
inst✝ : Decidable p
h : p
⊢ _root_.guard p = some PUnit.unit ↔ p
[PROOFSTEP]
simp [_root_.guard, h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ _root_.guard p = some PUnit.unit ↔ p
[PROOFSTEP]
simp [_root_.guard, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b
[PROOFSTEP]
simpa [liftOrGet] using h a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
o : Option α
⊢ casesOn' o (f none) (f ∘ fun a => some a) = f o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
⊢ casesOn' none (f none) (f ∘ fun a => some a) = f none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
val✝ : α
⊢ casesOn' (some val✝) (f none) (f ∘ fun a => some a) = f (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o o' : Option α
x : α
⊢ (HOrElse.hOrElse o fun x => o') = some x ↔ o = some x ∨ o = none ∧ o' = some x
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o' : Option α
x : α
⊢ (HOrElse.hOrElse none fun x => o') = some x ↔ none = some x ∨ none = none ∧ o' = some x
[PROOFSTEP]
simp only [true_and, false_or, eq_self_iff_true, none_orElse]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o' : Option α
x val✝ : α
⊢ (HOrElse.hOrElse (some val✝) fun x => o') = some x ↔ some val✝ = some x ∨ some val✝ = none ∧ o' = some x
[PROOFSTEP]
simp only [some_orElse, or_false, false_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o o' : Option α
⊢ (HOrElse.hOrElse o fun x => o') = none ↔ o = none ∧ o' = none
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o' : Option α
⊢ (HOrElse.hOrElse none fun x => o') = none ↔ none = none ∧ o' = none
[PROOFSTEP]
simp only [true_and, none_orElse, eq_self_iff_true]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o' : Option α
val✝ : α
⊢ (HOrElse.hOrElse (some val✝) fun x => o') = none ↔ some val✝ = none ∧ o' = none
[PROOFSTEP]
simp only [some_orElse, false_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
o : Option α
⊢ Option.elim o (f none) (f ∘ some) = f o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
⊢ Option.elim none (f none) (f ∘ some) = f none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
val✝ : α
⊢ Option.elim (some val✝) (f none) (f ∘ some) = f (some val✝)
[PROOFSTEP]
rfl
