-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_atom {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size}
    (h : relabel r decls[idx] = .atom a) :
    ∃ x, decls[idx] = .atom x ∧ a = r x

Proof state:
case h_3
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Tactic:
contradiction

Result:
no goals

Proof state:
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h : relabel r decls[idx] = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Tactic:
unfold relabel at h

Result:
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (r a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Proof state:
case h_1
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
b✝ : Bool
heq✝ : decls[idx] = const b✝
h : const b✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Tactic:
contradiction

Result:
no goals

Proof state:
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : r x = a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Tactic:
exists x

Result:
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : r x = a
⊢ decls[idx] = atom x ∧ a = r x

Proof state:
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (r a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Tactic:
split at h

Result:
case h_1
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
b✝ : Bool
heq✝ : decls[idx] = const b✝
h : const b✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

case h_2
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (r a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

case h_3
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Proof state:
case h_2
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (r a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Tactic:
next x heq =>
injection h with h
exists x
simp [heq, h]

Result:
no goals

Proof state:
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : atom (r x) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Tactic:
injection h with h

Result:
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : r x = a
⊢ ∃ x, decls[idx] = atom x ∧ a = r x

Proof state:
α β : Type
idx : Nat
a : β
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
decl✝ : Decl α
x : α
heq : decls[idx] = atom x
h : r x = a
⊢ decls[idx] = atom x ∧ a = r x

Tactic:
simp [heq, h]

Result:
no goals