Theorem: FinInt.comp_eq_xor_minusOne (MLIR/Util/FinInt.lean)

State before:
sz : ℕ
n : FinInt sz
⊢ comp n = n ^^^ -1
Tactic:
simp [neg_minusOne, HXor.hXor]
State after:
sz : ℕ
n : FinInt sz
⊢ comp n = xor n minusOne

State before:
sz : ℕ
n : FinInt sz
⊢ comp n = xor n minusOne
Tactic:
induction sz <;> simp [comp, xor, logic1, logic2, minusOne] at *
State after:
case zero
n : FinInt Nat.zero
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n nil

case succ
n✝ : ℕ
n_ih✝ : ∀ (n : FinInt n✝), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ n✝)
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n (I minusOne)

State before:
n : FinInt Nat.zero
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n nil
Tactic:
case zero =>
  cases n; simp
State after:
no goals

State before:
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n (I minusOne)
Tactic:
case succ sz ih =>
  match n with
  | .I m => simp [logic1, logic2, ih]
  | .O m => simp [logic1, logic2, ih]
State after:
no goals

State before:
n : FinInt Nat.zero
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n nil
Tactic:
cases n
State after:
case nil

⊢ logic1 (fun x => !x) nil = logic2 (fun x x_1 => x != x_1) nil nil

State before:
case nil

⊢ logic1 (fun x => !x) nil = logic2 (fun x x_1 => x != x_1) nil nil
Tactic:
simp
State after:
no goals

State before:
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n (I minusOne)
Tactic:
match n with
| .I m => simp [logic1, logic2, ih]
| .O m => simp [logic1, logic2, ih]
State after:
no goals

State before:
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
m : FinInt sz
⊢ logic1 (fun x => !x) (I m) = logic2 (fun x x_1 => x != x_1) (I m) (I minusOne)
Tactic:
simp [logic1, logic2, ih]
State after:
no goals

State before:
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
m : FinInt sz
⊢ logic1 (fun x => !x) (O m) = logic2 (fun x x_1 => x != x_1) (O m) (I minusOne)
Tactic:
simp [logic1, logic2, ih]
State after:
no goals