Theorem: LO.FirstOrder.Arith.Model.not_mem_iff_mul_exp_add (Arithmetization/ISigmaOne/Bit.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
⊢ i ∉ a ↔ ∃ k, ∃ r < exp i, a = k * exp (i + 1) + r
Tactic:
simp [mem_iff_bit, exp_succ]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
⊢ ¬Bit i a ↔ ∃ k, ∃ r < exp i, a = k * (2 * exp i) + r

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
⊢ ¬Bit i a ↔ ∃ k, ∃ r < exp i, a = k * (2 * exp i) + r
Tactic:
exact not_lenbit_iff_add_mul (exp_pow2 i) (a := a)
State after:
no goals