case none
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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

case some
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
rcases x with (_|x)
no goals
case none
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
simp only [not_mem_none, exists_false, pmap, not_false_iff, exists_prop_of_false]
case some.mp
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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

case some.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
case some
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
constructor
case some.mp
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
case some.mp
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
intro h
case some.mp
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
case some.mp
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
simp only [pmap, Option.some_inj] at h
no goals
case some.mp
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
refine ⟨x, rfl, h⟩
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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))
case some.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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
rintro ⟨a, H, rfl⟩
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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))
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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))
simp only [mem_def, Option.some_inj] at H
no goals
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.12874
δ : Type ?u.12877
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))
simp only [H, pmap]