-- Mathlib/Data/List/Permutation.lean
theorem map_permutationsAux2' {α' β'} (g : α → α') (g' : β → β') (t : α) (ts ys : List α)
    (r : List β) (f : List α → β) (f' : List α' → β') (H : ∀ a, g' (f a) = f' (map g a)) :
    map g' (permutationsAux2 t ts r ys f).2 =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').2

Proof state:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r ys f).2 = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').2

Tactic:
induction' ys with ys_hd _ ys_ih generalizing f f'

Result:
case nil
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r [] f).2 = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').2

case cons
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).2 = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').2
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r (ys_hd :: tail✝) f).2 =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g (ys_hd :: tail✝)) f').2

Proof state:
case cons.H
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).2 = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').2
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ ∀ (a : List α), g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)

Tactic:
intro a

Result:
case cons.H
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).2 = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').2
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
a : List α
⊢ g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)

Proof state:
case cons
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).2 = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').2
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts))

Tactic:
simp only [← map_cons, ← map_append]

Result:
case cons
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).2 = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').2
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (map g (t :: ys_hd :: (tail✝ ++ ts)))