Theorem: FinInt.sub_add_dist (MLIR/Dialects/ArithSemantics.lean)

State before:
sz : ℕ
⊢ ∀ (C X C2 : FinInt sz), C - (X + C2) = C - C2 - X
Tactic:
intros C X C2
State after:
sz : ℕ
C X C2 : FinInt sz
⊢ C - (X + C2) = C - C2 - X

State before:
sz : ℕ
C X C2 : FinInt sz
⊢ C - (X + C2) = C - C2 - X
Tactic:
apply eq_of_toUint_cong2
State after:
case a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint (C - (X + C2)) ≡ toUint (C - C2 - X) [2^sz]

State before:
case a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint (C - (X + C2)) ≡ toUint (C - C2 - X) [2^sz]
Tactic:
simp [cong2, FinInt.sub_toUint, FinInt.add_toUint]
State after:
case a
sz : ℕ
C X C2 : FinInt sz
⊢ mod2 (toUint C - (toUint X + toUint C2)) sz = mod2 (toUint C - toUint C2 - toUint X) sz

State before:
case a
sz : ℕ
C X C2 : FinInt sz
⊢ mod2 (toUint C - (toUint X + toUint C2)) sz = mod2 (toUint C - toUint C2 - toUint X) sz
Tactic:
apply FinInt.mod2_fequal
State after:
case a.a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint C - (toUint X + toUint C2) = toUint C - toUint C2 - toUint X

State before:
case a.a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint C - (toUint X + toUint C2) = toUint C - toUint C2 - toUint X
Tactic:
simp [Int.sub_add_dist, Int.sub_assoc]
State after:
no goals