Theorem: List.mem_map (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
⊢ b ∈ map f (x :: xs) ↔ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
have ih := @mem_map α β f b xs
State after:
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) ↔ ∃ a, a ∈ x :: xs ∧ f a = b

State before:
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) ↔ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) → ∃ a, a ∈ x :: xs ∧ f a = b

case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)

State before:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) → ∃ a, a ∈ x :: xs ∧ f a = b

case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
Tactic:
. intro h
  cases h with
  | head =>
    exact Exists.intro x (And.intro (List.Mem.head _) rfl)
  | tail x h' =>
    have ih_val := ih.mp h'
    cases ih_val with | intro a ha =>
    exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
State after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)

State before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
Tactic:
. intro h
  cases h with | intro a ha =>
  simp only [map]
  cases ha.left with
  | head => rw [ha.right]; constructor
  | tail x h' =>
    have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
    exact Mem.tail _ h_in_tail
State after:
no goals

State before:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ b ∈ map f (x :: xs) → ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
intro h
State after:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : b ∈ map f (x :: xs)
⊢ ∃ a, a ∈ x :: xs ∧ f a = b

State before:
case mp
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : b ∈ map f (x :: xs)
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
cases h with
| head =>
  exact Exists.intro x (And.intro (List.Mem.head _) rfl)
| tail x h' =>
  have ih_val := ih.mp h'
  cases ih_val with | intro a ha =>
  exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
State after:
no goals

State before:
case mp.head
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : f x ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = f x
⊢ ∃ a, a ∈ x :: xs ∧ f a = f x
Tactic:
exact Exists.intro x (And.intro (List.Mem.head _) rfl)
State after:
no goals

State before:
case mp.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h' : Mem b (map f xs)
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
have ih_val := ih.mp h'
State after:
case mp.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h' : Mem b (map f xs)
ih_val : ∃ a, a ∈ xs ∧ f a = b
⊢ ∃ a, a ∈ x :: xs ∧ f a = b

State before:
case mp.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h' : Mem b (map f xs)
ih_val : ∃ a, a ∈ xs ∧ f a = b
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
cases ih_val with | intro a ha =>
exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
State after:
no goals

State before:
case mp.tail.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h' : Mem b (map f xs)
a : α
ha : a ∈ xs ∧ f a = b
⊢ ∃ a, a ∈ x :: xs ∧ f a = b
Tactic:
exact Exists.intro a (And.intro (Mem.tail _ ha.left) ha.right)
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
⊢ (∃ a, a ∈ x :: xs ∧ f a = b) → b ∈ map f (x :: xs)
Tactic:
intro h
State after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : ∃ a, a ∈ x :: xs ∧ f a = b
⊢ b ∈ map f (x :: xs)

State before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
h : ∃ a, a ∈ x :: xs ∧ f a = b
⊢ b ∈ map f (x :: xs)
Tactic:
cases h with | intro a ha =>
simp only [map]
cases ha.left with
| head => rw [ha.right]; constructor
| tail x h' =>
  have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
  exact Mem.tail _ h_in_tail
State after:
no goals

State before:
case mpr.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
⊢ b ∈ map f (x :: xs)
Tactic:
simp only [map]
State after:
case mpr.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
⊢ b ∈ f x :: map f xs

State before:
case mpr.intro
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
⊢ b ∈ f x :: map f xs
Tactic:
cases ha.left with
| head => rw [ha.right]; constructor
| tail x h' =>
  have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
  exact Mem.tail _ h_in_tail
State after:
no goals

State before:
case mpr.intro.head
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
ha : x ∈ x :: xs ∧ f x = b
⊢ b ∈ f x :: map f xs
Tactic:
rw [ha.right]
State after:
case mpr.intro.head
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
ha : x ∈ x :: xs ∧ f x = b
⊢ b ∈ b :: map f xs

State before:
case mpr.intro.head
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
ha : x ∈ x :: xs ∧ f x = b
⊢ b ∈ b :: map f xs
Tactic:
constructor
State after:
no goals

State before:
case mpr.intro.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
h' : Mem a xs
⊢ b ∈ f x :: map f xs
Tactic:
have h_in_tail := ih.mpr (Exists.intro a ⟨h', ha.right⟩)
State after:
case mpr.intro.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
h' : Mem a xs
h_in_tail : b ∈ map f xs
⊢ b ∈ f x :: map f xs

State before:
case mpr.intro.tail
α : Type u_1
β : Type u_2
f : α → β
b : β
x : α
xs : List α
ih : b ∈ map f xs ↔ ∃ a, a ∈ xs ∧ f a = b
a : α
ha : a ∈ x :: xs ∧ f a = b
h' : Mem a xs
h_in_tail : b ∈ map f xs
⊢ b ∈ f x :: map f xs
Tactic:
exact Mem.tail _ h_in_tail
State after:
no goals