-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem unsat_relabel_iff {f : CNF α} {r : α → β}
    (hw : ∀ {v1 v2}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2) :
    Unsat (relabel r f) ↔ Unsat f

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ (if h : ∃ a, Mem a f ∧ r a = r v then h.choose else a₀) = v

Tactic:
rw [dif_pos ⟨v, h, rfl⟩]

Result:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ ⋯.choose = v

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
this : ∀ (a : α), Mem a f → g (r a) = a
⊢ relabel g (relabel r f) = f

Tactic:
rw [relabel_relabel, relabel_congr, relabel_id]

Result:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
this : ∀ (a : α), Mem a f → g (r a) = a
⊢ ∀ (v : α), Mem v f → (g ∘ r) v = id v

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ Mem ⋯.choose f

Tactic:
exact (Exists.choose_spec (⟨v, h, rfl⟩ : ∃ a', Mem a' f ∧ r a' = r v)).1

Result:
no goals

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
⊢ f.Unsat

Tactic:
suffices w : relabel g (relabel r f) = f by
  rwa [w] at h'

Result:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
⊢ relabel g (relabel r f) = f

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
⊢ (relabel r f).Unsat ↔ f.Unsat

Tactic:
refine ⟨fun h => ?_, unsat_relabel r⟩

Result:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
⊢ f.Unsat

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ ⋯.choose = v

Tactic:
apply hw _ h

Result:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ r ⋯.choose = r v

α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ Mem ⋯.choose f

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
⊢ (relabel r f).Unsat ↔ f.Unsat

Tactic:
rcases nonempty_or_impossible f with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩)

Result:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
⊢ (relabel r f).Unsat ↔ f.Unsat

case inr.intro
α : Type u_1
β : Type u_2
r : α → β
n : Nat
hw : ∀ {v1 v2 : α}, Mem v1 (List.replicate n []) → Mem v2 (List.replicate n []) → r v1 = r v2 → v1 = v2
⊢ (relabel r (List.replicate n [])).Unsat ↔ Unsat (List.replicate n [])

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
⊢ f.Unsat

Tactic:
have em := Classical.propDecidable

Result:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
⊢ f.Unsat

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
⊢ ∀ (a : α), Mem a f → g (r a) = a

Tactic:
intro v h

Result:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ g (r v) = v

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h✝ : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
v : α
h : Mem v f
⊢ r ⋯.choose = r v

Tactic:
exact (Exists.choose_spec (⟨v, h, rfl⟩ : ∃ a', Mem a' f ∧ r a' = r v)).2

Result:
no goals

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
this : ∀ (a : α), Mem a f → g (r a) = a
⊢ ∀ (v : α), Mem v f → (g ∘ r) v = id v

Tactic:
exact this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
w : relabel g (relabel r f) = f
⊢ f.Unsat

Tactic:
rwa [w] at h'

Result:
no goals

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
⊢ f.Unsat

Tactic:
have h' := unsat_relabel g h

Result:
case inl.intro
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
hw : ∀ {v1 v2 : α}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2
a₀ : α
h : (relabel r f).Unsat
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀
h' : (relabel g (relabel r f)).Unsat
⊢ f.Unsat