Theorem: CNF.Clause.relabel_relabel' (LeanSAT/Reflect/CNF/Relabel.lean)

State before:
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
⊢ relabel f ∘ relabel g = relabel (f ∘ g)
Tactic:
funext i
State after:
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ (relabel f ∘ relabel g) i = relabel (f ∘ g) i

State before:
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ (relabel f ∘ relabel g) i = relabel (f ∘ g) i
Tactic:
simp only [Function.comp_apply, relabel, List.map_map]
State after:
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ List.map ((fun x => (f x.fst, x.snd)) ∘ fun x => (g x.fst, x.snd)) i = List.map (fun x => (f (g x.fst), x.snd)) i

State before:
case h
α✝² α✝¹ : Type
f : α✝² → α✝¹
α✝ : Type
g : α✝ → α✝²
i : Clause α✝
⊢ List.map ((fun x => (f x.fst, x.snd)) ∘ fun x => (g x.fst, x.snd)) i = List.map (fun x => (f (g x.fst), x.snd)) i
Tactic:
rfl
State after:
no goals