Theorem: List.map_congr (LeanSAT/Reflect/CNF/Relabel.lean)

State before:
α : Type u_1
β : Type u_2
f g : α → β
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → f x = g x
⊢ map f (a :: l) = map g (a :: l)
Tactic:
let ⟨h₁, h₂⟩ := forall_mem_cons.1 h
State after:
α : Type u_1
β : Type u_2
f g : α → β
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → f x = g x
h₁ : f a = g a
h₂ : ∀ (x : α), x ∈ l → f x = g x
⊢ map f (a :: l) = map g (a :: l)

State before:
α : Type u_1
β : Type u_2
f g : α → β
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → f x = g x
h₁ : f a = g a
h₂ : ∀ (x : α), x ∈ l → f x = g x
⊢ map f (a :: l) = map g (a :: l)
Tactic:
rw [map, map, h₁, map_congr h₂]
State after:
no goals