Theorem: LO.FirstOrder.Arith.Model.lenbit_sub_pow2_iff_of_lenbit (Arithmetization/ISigmaZero/Exponential/Pow2.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
⊢ LenBit i (a - j) ↔ i ≠ j ∧ LenBit i a
Tactic:
generalize ha' : a - j = a'
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
a' : M
ha' : a - j = a'
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
a' : M
ha' : a - j = a'
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i a
Tactic:
have h' : ¬LenBit j a' := by simpa [←ha'] using LenBit.sub_self_of_lenbit pj.pos h
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
a' : M
ha' : a - j = a'
h' : ¬LenBit j a'
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
a' : M
ha' : a - j = a'
h' : ¬LenBit j a'
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i a
Tactic:
have : a = a' + j := by simp [←ha', sub_add_self_of_le h.le]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
a' : M
ha' : a - j = a'
h' : ¬LenBit j a'
this : a = a' + j
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i a

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
a' : M
ha' : a - j = a'
h' : ¬LenBit j a'
this : a = a' + j
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i a
Tactic:
rcases this with rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j : M
pi : Pow2 i
pj : Pow2 j
a' : M
h' : ¬LenBit j a'
h : LenBit j (a' + j)
ha' : a' + j - j = a'
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i (a' + j)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j : M
pi : Pow2 i
pj : Pow2 j
a' : M
h' : ¬LenBit j a'
h : LenBit j (a' + j)
ha' : a' + j - j = a'
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i (a' + j)
Tactic:
have : LenBit i (a' + j) ↔ i = j ∨ LenBit i a' := lenbit_add_pow2_iff_of_not_lenbit pi pj h'
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j : M
pi : Pow2 i
pj : Pow2 j
a' : M
h' : ¬LenBit j a'
h : LenBit j (a' + j)
ha' : a' + j - j = a'
this : LenBit i (a' + j) ↔ i = j ∨ LenBit i a'
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i (a' + j)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j : M
pi : Pow2 i
pj : Pow2 j
a' : M
h' : ¬LenBit j a'
h : LenBit j (a' + j)
ha' : a' + j - j = a'
this : LenBit i (a' + j) ↔ i = j ∨ LenBit i a'
⊢ LenBit i a' ↔ i ≠ j ∧ LenBit i (a' + j)
Tactic:
simp [this, and_or_left]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j : M
pi : Pow2 i
pj : Pow2 j
a' : M
h' : ¬LenBit j a'
h : LenBit j (a' + j)
ha' : a' + j - j = a'
this : LenBit i (a' + j) ↔ i = j ∨ LenBit i a'
⊢ LenBit i a' → ¬i = j

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j : M
pi : Pow2 i
pj : Pow2 j
a' : M
h' : ¬LenBit j a'
h : LenBit j (a' + j)
ha' : a' + j - j = a'
this : LenBit i (a' + j) ↔ i = j ∨ LenBit i a'
⊢ LenBit i a' → ¬i = j
Tactic:
rintro _ rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
pi : Pow2 i
a' : M
a✝ : LenBit i a'
pj : Pow2 i
h' : ¬LenBit i a'
h : LenBit i (a' + i)
ha' : a' + i - i = a'
this : LenBit i (a' + i) ↔ i = i ∨ LenBit i a'
⊢ False

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
pi : Pow2 i
a' : M
a✝ : LenBit i a'
pj : Pow2 i
h' : ¬LenBit i a'
h : LenBit i (a' + i)
ha' : a' + i - i = a'
this : LenBit i (a' + i) ↔ i = i ∨ LenBit i a'
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
a' : M
ha' : a - j = a'
⊢ ¬LenBit j a'
Tactic:
simpa [←ha'] using LenBit.sub_self_of_lenbit pj.pos h
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a i j : M
pi : Pow2 i
pj : Pow2 j
h : LenBit j a
a' : M
ha' : a - j = a'
h' : ¬LenBit j a'
⊢ a = a' + j
Tactic:
simp [←ha', sub_add_self_of_le h.le]
State after:
no goals