Theorem: List.mem_pmap (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
l : List α
hp : ∀ (a : α), a ∈ l → p a
⊢ b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
Tactic:
induction l with
| nil => simp
| cons a l IH =>
  dsimp [pmap]
  simp only [mem_cons, exists_and_left, exists_eq_or_imp, IH]
  apply or_congr_left
  constructor
  . intro h; exact .intro _ h
  . intro h; cases h; assumption
State after:
no goals

State before:
case nil
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
hp : ∀ (a : α), a ∈ [] → p a
⊢ b ∈ pmap f [] hp ↔ ∃ a h, a ∈ [] ∧ b = f a h
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b ∈ pmap f (a :: l) hp ↔ ∃ a_1 h, a_1 ∈ a :: l ∧ b = f a_1 h
Tactic:
dsimp [pmap]
State after:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b ∈ f a (_ : p a) :: pmap f l (_ : ∀ (x : α), x ∈ l → p x) ↔ ∃ a_1 h, a_1 ∈ a :: l ∧ b = f a_1 h

State before:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b ∈ f a (_ : p a) :: pmap f l (_ : ∀ (x : α), x ∈ l → p x) ↔ ∃ a_1 h, a_1 ∈ a :: l ∧ b = f a_1 h
Tactic:
simp only [mem_cons, exists_and_left, exists_eq_or_imp, IH]
State after:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (b = f a (_ : p a) ∨ ∃ a, a ∈ l ∧ ∃ x, b = f a x) ↔ (∃ x, b = f a x) ∨ ∃ a, a ∈ l ∧ ∃ x, b = f a x

State before:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (b = f a (_ : p a) ∨ ∃ a, a ∈ l ∧ ∃ x, b = f a x) ↔ (∃ x, b = f a x) ∨ ∃ a, a ∈ l ∧ ∃ x, b = f a x
Tactic:
apply or_congr_left
State after:
case cons.h
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) ↔ ∃ x, b = f a x

State before:
case cons.h
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) ↔ ∃ x, b = f a x
Tactic:
constructor
State after:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) → ∃ x, b = f a x

case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)

State before:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) → ∃ x, b = f a x

case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)
Tactic:
. intro h; exact .intro _ h
State after:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)

State before:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)
Tactic:
. intro h; cases h; assumption
State after:
no goals

State before:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) → ∃ x, b = f a x
Tactic:
intro h
State after:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
h : b = f a (_ : p a)
⊢ ∃ x, b = f a x

State before:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
h : b = f a (_ : p a)
⊢ ∃ x, b = f a x
Tactic:
exact .intro _ h
State after:
no goals

State before:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)
Tactic:
intro h
State after:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
h : ∃ x, b = f a x
⊢ b = f a (_ : p a)

State before:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
h : ∃ x, b = f a x
⊢ b = f a (_ : p a)
Tactic:
cases h
State after:
case cons.h.mpr.intro
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
w✝ : p a
h✝ : b = f a w✝
⊢ b = f a (_ : p a)

State before:
case cons.h.mpr.intro
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
w✝ : p a
h✝ : b = f a w✝
⊢ b = f a (_ : p a)
Tactic:
assumption
State after:
no goals