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

State before:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ relabel f x = relabel g x
Tactic:
simp only [relabel]
State after:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (fun x => (f x.fst, x.snd)) x = List.map (fun x => (g x.fst, x.snd)) x

State before:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (fun x => (f x.fst, x.snd)) x = List.map (fun x => (g x.fst, x.snd)) x
Tactic:
rw [List.map_congr]
State after:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : α × Bool), x_1 ∈ x → (f x_1.fst, x_1.snd) = (g x_1.fst, x_1.snd)

State before:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : α × Bool), x_1 ∈ x → (f x_1.fst, x_1.snd) = (g x_1.fst, x_1.snd)
Tactic:
intro ⟨i, b⟩ h
State after:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
i : α
b : Bool
h : (i, b) ∈ x
⊢ (f (i, b).fst, (i, b).snd) = (g (i, b).fst, (i, b).snd)

State before:
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
i : α
b : Bool
h : (i, b) ∈ x
⊢ (f (i, b).fst, (i, b).snd) = (g (i, b).fst, (i, b).snd)
Tactic:
congr
State after:
case e_fst
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
i : α
b : Bool
h : (i, b) ∈ x
⊢ f (i, b).fst = g (i, b).fst

State before:
case e_fst
α β : Type
x : Clause α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
i : α
b : Bool
h : (i, b) ∈ x
⊢ f (i, b).fst = g (i, b).fst
Tactic:
apply w _ (mem_of h)
State after:
no goals