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

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

State before:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ List.map (Clause.relabel f) x = List.map (Clause.relabel g) x
Tactic:
rw [List.map_congr]
State after:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : Clause α), x_1 ∈ x → Clause.relabel f x_1 = Clause.relabel g x_1

State before:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
⊢ ∀ (x_1 : Clause α), x_1 ∈ x → Clause.relabel f x_1 = Clause.relabel g x_1
Tactic:
intro c h
State after:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
⊢ Clause.relabel f c = Clause.relabel g c

State before:
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
⊢ Clause.relabel f c = Clause.relabel g c
Tactic:
apply Clause.relabel_congr
State after:
case w
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
⊢ ∀ (a : α), Clause.mem a c → f a = g a

State before:
case w
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
⊢ ∀ (a : α), Clause.mem a c → f a = g a
Tactic:
intro a m
State after:
case w
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
a : α
m : Clause.mem a c
⊢ f a = g a

State before:
case w
α β : Type
x : CNF α
f g : α → β
w : ∀ (a : α), mem a x → f a = g a
c : Clause α
h : c ∈ x
a : α
m : Clause.mem a c
⊢ f a = g a
Tactic:
exact w _ (mem_of h m)
State after:
no goals