-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_cons_iff {f : α → β} {l : List α} :
    map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

Proof state:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
a : α
l₁ : List α
⊢ f a = f a ∧ map f l₁ = map f l₁

Tactic:
constructor <;> rfl

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
a : α
l₁ : List α
⊢ f a = b ∧ map f l₁ = l₂ → ∃ a_2 l₁_1, (a = a_2 ∧ l₁ = l₁_1) ∧ f a_2 = b ∧ map f l₁_1 = l₂

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
f : α → β
a : α
l₁ : List α
⊢ ∃ a_1 l₁_1, (a = a_1 ∧ l₁ = l₁_1) ∧ f a_1 = f a ∧ map f l₁_1 = map f l₁

Proof state:
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
a : α
l₁ : List α
⊢ f a = b ∧ map f l₁ = l₂ ↔ ∃ a_1 l₁_1, (a = a_1 ∧ l₁ = l₁_1) ∧ f a_1 = b ∧ map f l₁_1 = l₂

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
a : α
l₁ : List α
⊢ f a = b ∧ map f l₁ = l₂ → ∃ a_2 l₁_1, (a = a_2 ∧ l₁ = l₁_1) ∧ f a_2 = b ∧ map f l₁_1 = l₂

case mpr
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
a : α
l₁ : List α
⊢ (∃ a_1 l₁_1, (a = a_1 ∧ l₁ = l₁_1) ∧ f a_1 = b ∧ map f l₁_1 = l₂) → f a = b ∧ map f l₁ = l₂

Proof state:
case nil
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
⊢ map f [] = b :: l₂ ↔ ∃ a l₁, [] = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

case cons
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
head✝ : α
tail✝ : List α
⊢ map f (head✝ :: tail✝) = b :: l₂ ↔ ∃ a l₁, head✝ :: tail✝ = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

Tactic:
case nil => simp

Result:
case cons
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
head✝ : α
tail✝ : List α
⊢ map f (head✝ :: tail✝) = b :: l₂ ↔ ∃ a l₁, head✝ :: tail✝ = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

Proof state:
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
a : α
l₁ : List α
⊢ map f (a :: l₁) = b :: l₂ ↔ ∃ a_1 l₁_1, a :: l₁ = a_1 :: l₁_1 ∧ f a_1 = b ∧ map f l₁_1 = l₂

Tactic:
simp only [map_cons, cons.injEq]

Result:
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
a : α
l₁ : List α
⊢ f a = b ∧ map f l₁ = l₂ ↔ ∃ a_1 l₁_1, (a = a_1 ∧ l₁ = l₁_1) ∧ f a_1 = b ∧ map f l₁_1 = l₂

Proof state:
case mpr
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
a : α
l₁ : List α
⊢ (∃ a_1 l₁_1, (a = a_1 ∧ l₁ = l₁_1) ∧ f a_1 = b ∧ map f l₁_1 = l₂) → f a = b ∧ map f l₁ = l₂

Tactic:
rintro ⟨a, l₁, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩

Result:
case mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
a : α
l₁ : List α
⊢ f a = f a ∧ map f l₁ = map f l₁

Proof state:
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
l : List α
⊢ map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

Tactic:
cases l

Result:
case nil
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
⊢ map f [] = b :: l₂ ↔ ∃ a l₁, [] = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

case cons
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
head✝ : α
tail✝ : List α
⊢ map f (head✝ :: tail✝) = b :: l₂ ↔ ∃ a l₁, head✝ :: tail✝ = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
f : α → β
a : α
l₁ : List α
⊢ ∃ a_1 l₁_1, (a = a_1 ∧ l₁ = l₁_1) ∧ f a_1 = f a ∧ map f l₁_1 = map f l₁

Tactic:
exact ⟨a, l₁, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
⊢ map f [] = b :: l₂ ↔ ∃ a l₁, [] = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

Tactic:
simp

Result:
no goals