internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
⊢ (p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q) → Pow2 p
Tactic:
rintro (rfl | ⟨q, rfl, hq⟩) <;> simp [pow2_one, pow2_mul_two, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
⊢ 2 = 2 * 1 ∧ Pow2 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.div_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
h : Pow2 p
ne : p ≠ 1
⊢ Pow2 (p / 2)
Tactic:
rcases Pow2.elim.mp h with (rfl | ⟨q, rfl, pq⟩)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
h : Pow2 1
ne : 1 ≠ 1
⊢ Pow2 (1 / 2)

case inr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
pq : Pow2 q
h : Pow2 (2 * q)
ne : 2 * q ≠ 1
⊢ Pow2 (2 * q / 2)
Theorem: LO.FirstOrder.Arith.Model.Pow2.div_two
Proof state before:
case inr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
pq : Pow2 q
h : Pow2 (2 * q)
ne : 2 * q ≠ 1
⊢ Pow2 (2 * q / 2)
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.div_two
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
h : Pow2 1
ne : 1 ≠ 1
⊢ Pow2 (1 / 2)
Tactic:
simp at ne
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.two_mul_div_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
h : Pow2 p
ne : p ≠ 1
⊢ 2 * (p / 2) = p
Tactic:
rcases Pow2.elim.mp h with (rfl | ⟨q, rfl, _⟩)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
h : Pow2 1
ne : 1 ≠ 1
⊢ 2 * (1 / 2) = 1

case inr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
right✝ : Pow2 q
h : Pow2 (2 * q)
ne : 2 * q ≠ 1
⊢ 2 * (2 * q / 2) = 2 * q
Theorem: LO.FirstOrder.Arith.Model.Pow2.two_mul_div_two
Proof state before:
case inr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
right✝ : Pow2 q
h : Pow2 (2 * q)
ne : 2 * q ≠ 1
⊢ 2 * (2 * q / 2) = 2 * q
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.two_mul_div_two
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
h : Pow2 1
ne : 1 ≠ 1
⊢ 2 * (1 / 2) = 1
Tactic:
simp at ne
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.div_two_mul_two
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
h : Pow2 p
ne : p ≠ 1
⊢ p / 2 * 2 = p
Tactic:
simp [mul_comm, h.two_mul_div_two ne]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim'
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
⊢ Pow2 p ↔ p = 1 ∨ 1 < p ∧ ∃ q, p = 2 * q ∧ Pow2 q
Tactic:
by_cases hp : 1 < p <;> simp [hp]
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
hp : 1 < p
⊢ Pow2 p ↔ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
hp : ¬1 < p
⊢ Pow2 p ↔ p = 1
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim'
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
hp : 1 < p
⊢ Pow2 p ↔ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Tactic:
exact Pow2.elim
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim'
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
hp : ¬1 < p
⊢ Pow2 p ↔ p = 1
Tactic:
have : p = 0 ∨ p = 1 := le_one_iff_eq_zero_or_one.mp (show p ≤ 1 from by simpa using hp)
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
hp : ¬1 < p
this : p = 0 ∨ p = 1
⊢ Pow2 p ↔ p = 1
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim'
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
hp : ¬1 < p
this : p = 0 ∨ p = 1
⊢ Pow2 p ↔ p = 1
Tactic:
rcases this with (rfl | rfl) <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim'
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
hp : ¬1 < p
⊢ p ≤ 1
Tactic:
simpa using hp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lenbit_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
⊢ 𝚺₀-Relation LenBit via lenbitDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
⊢ (fun v => LenBit (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val lenbitDef)
Theorem: LO.FirstOrder.Arith.Model.lenbit_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
⊢ (fun v => LenBit (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val lenbitDef)
Tactic:
simp[sqrt_graph, lenbitDef, Matrix.vecHead, Matrix.vecTail, LenBit, ←le_iff_lt_succ, numeral_eq_natCast]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
⊢ ¬2 ∣ v 1 / v 0 ↔ ∃ x ≤ v 1, x = v 1 / v 0 ∧ ¬2 ∣ x
Theorem: LO.FirstOrder.Arith.Model.lenbit_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
⊢ ¬2 ∣ v 1 / v 0 ↔ ∃ x ≤ v 1, x = v 1 / v 0 ∧ ¬2 ∣ x
Tactic:
constructor
Proof state after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
⊢ ¬2 ∣ v 1 / v 0 → ∃ x ≤ v 1, x = v 1 / v 0 ∧ ¬2 ∣ x

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
⊢ (∃ x ≤ v 1, x = v 1 / v 0 ∧ ¬2 ∣ x) → ¬2 ∣ v 1 / v 0
Theorem: LO.FirstOrder.Arith.Model.lenbit_defined
Proof state before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
⊢ ¬2 ∣ v 1 / v 0 → ∃ x ≤ v 1, x = v 1 / v 0 ∧ ¬2 ∣ x
Tactic:
intro h
Proof state after:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
h : ¬2 ∣ v 1 / v 0
⊢ ∃ x ≤ v 1, x = v 1 / v 0 ∧ ¬2 ∣ x
Theorem: LO.FirstOrder.Arith.Model.lenbit_defined
Proof state before:
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
h : ¬2 ∣ v 1 / v 0
⊢ ∃ x ≤ v 1, x = v 1 / v 0 ∧ ¬2 ∣ x
Tactic:
exact ⟨v 1 / v 0, by simp, rfl, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lenbit_defined
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
h : ¬2 ∣ v 1 / v 0
⊢ v 1 / v 0 ≤ v 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lenbit_defined
Proof state before:
case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
⊢ (∃ x ≤ v 1, x = v 1 / v 0 ∧ ¬2 ∣ x) → ¬2 ∣ v 1 / v 0
Tactic:
rintro ⟨z, hz, rfl, h⟩
Proof state after:
case mpr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
hz : v 1 / v 0 ≤ v 1
h : ¬2 ∣ v 1 / v 0
⊢ ¬2 ∣ v 1 / v 0
Theorem: LO.FirstOrder.Arith.Model.lenbit_defined
Proof state before:
case mpr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
v : Fin 2 → M
hz : v 1 / v 0 ≤ v 1
h : ¬2 ∣ v 1 / v 0
⊢ ¬2 ∣ v 1 / v 0
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.le
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : LenBit i a
⊢ i ≤ a
Tactic:
by_contra A
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : LenBit i a
A : ¬i ≤ a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.LenBit.le
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : LenBit i a
A : ¬i ≤ a
⊢ False
Tactic:
simp [LenBit, show a < i from by simpa using A] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.le
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : LenBit i a
A : ¬i ≤ a
⊢ a < i
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_lenbit_of_lt
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : a < i
⊢ ¬LenBit i a
Tactic:
intro A
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : a < i
A : LenBit i a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.not_lenbit_of_lt
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : a < i
A : LenBit i a
⊢ False
Tactic:
exact not_le.mpr h A.le
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
⊢ ¬LenBit 0 a
Tactic:
simp [LenBit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.on_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
⊢ ¬LenBit a 0
Tactic:
simp [LenBit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
⊢ LenBit 1 a ↔ ¬2 ∣ a
Tactic:
simp [LenBit]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.iff_rem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
⊢ LenBit i a ↔ a / i % 2 = 1
Tactic:
simp [LenBit]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
⊢ ¬2 ∣ a / i ↔ a / i % 2 = 1
Theorem: LO.FirstOrder.Arith.Model.LenBit.iff_rem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
⊢ ¬2 ∣ a / i ↔ a / i % 2 = 1
Tactic:
rcases mod_two (a / i) with (h | h) <;> simp [h, ←mod_eq_zero_iff_dvd]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_lenbit_iff_rem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
⊢ ¬LenBit i a ↔ a / i % 2 = 0
Tactic:
simp [LenBit, ←mod_eq_zero_iff_dvd]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.self
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
pos : 0 < a
⊢ LenBit a a
Tactic:
simp [LenBit.iff_rem, pos, one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
h : 2 * i ∣ k
⊢ LenBit i (a % k) ↔ LenBit i a
Tactic:
have : 0 ≤ i := zero_le i
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
h : 2 * i ∣ k
this : 0 ≤ i
⊢ LenBit i (a % k) ↔ LenBit i a
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
h : 2 * i ∣ k
this : 0 ≤ i
⊢ LenBit i (a % k) ↔ LenBit i a
Tactic:
rcases (eq_or_lt_of_le this) with (rfl | pos)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a k : M
h : 2 * 0 ∣ k
this : 0 ≤ 0
⊢ LenBit 0 (a % k) ↔ LenBit 0 a

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
h : 2 * i ∣ k
this : 0 ≤ i
pos : 0 < i
⊢ LenBit i (a % k) ↔ LenBit i a
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
h : 2 * i ∣ k
this : 0 ≤ i
pos : 0 < i
⊢ LenBit i (a % k) ↔ LenBit i a
Tactic:
rcases h with ⟨k', hk'⟩
Proof state after:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
this : 0 ≤ i
pos : 0 < i
k' : M
hk' : k = 2 * i * k'
⊢ LenBit i (a % k) ↔ LenBit i a
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
this : 0 ≤ i
pos : 0 < i
k' : M
hk' : k = 2 * i * k'
⊢ LenBit i (a % k) ↔ LenBit i a
Tactic:
calc
  LenBit i (a % k) ↔ ((a % k) / i) % 2 = 1                            := LenBit.iff_rem
  _                  ↔ ((2 * k') * (a / k) + a % k / i) % 2 = 1       := by simp [mul_assoc]
  _                  ↔ (((2 * k') * (a / k) * i + a % k) / i) % 2 = 1 := by simp [div_mul_add_self, pos]
  _                  ↔ ((k * (a / k) + a % k) / i) % 2 = 1            := iff_of_eq (by
                                                                                    congr 3
                                                                                    simp [mul_right_comm _ (a / k), mul_right_comm 2 k' i, ←hk'])
  _                  ↔ LenBit i a                                     := by simp [div_add_mod a k, LenBit.iff_rem]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a k : M
h : 2 * 0 ∣ k
this : 0 ≤ 0
⊢ LenBit 0 (a % k) ↔ LenBit 0 a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
this : 0 ≤ i
pos : 0 < i
k' : M
hk' : k = 2 * i * k'
⊢ a % k / i % 2 = 1 ↔ (2 * k' * (a / k) + a % k / i) % 2 = 1
Tactic:
simp [mul_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
this : 0 ≤ i
pos : 0 < i
k' : M
hk' : k = 2 * i * k'
⊢ (2 * k' * (a / k) + a % k / i) % 2 = 1 ↔ (2 * k' * (a / k) * i + a % k) / i % 2 = 1
Tactic:
simp [div_mul_add_self, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
this : 0 ≤ i
pos : 0 < i
k' : M
hk' : k = 2 * i * k'
⊢ ((2 * k' * (a / k) * i + a % k) / i % 2 = 1) = ((k * (a / k) + a % k) / i % 2 = 1)
Tactic:
congr 3
Proof state after:
case e_a.e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
this : 0 ≤ i
pos : 0 < i
k' : M
hk' : k = 2 * i * k'
⊢ 2 * k' * (a / k) * i + a % k = k * (a / k) + a % k
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
case e_a.e_a.e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
this : 0 ≤ i
pos : 0 < i
k' : M
hk' : k = 2 * i * k'
⊢ 2 * k' * (a / k) * i + a % k = k * (a / k) + a % k
Tactic:
simp [mul_right_comm _ (a / k), mul_right_comm 2 k' i, ←hk']
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a k : M
this : 0 ≤ i
pos : 0 < i
k' : M
hk' : k = 2 * i * k'
⊢ (k * (a / k) + a % k) / i % 2 = 1 ↔ LenBit i a
Tactic:
simp [div_add_mod a k, LenBit.iff_rem]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.mod_two_mul_self
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a i : M
⊢ 2 * i ∣ 2 * i
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
have : 0 ≤ i := zero_le i
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
this : 0 ≤ i
⊢ LenBit i (a + b) ↔ LenBit i a
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
this : 0 ≤ i
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
rcases (eq_or_lt_of_le this) with (rfl | pos)
Proof state after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : 2 * 0 ∣ b
this : 0 ≤ 0
⊢ LenBit 0 (a + b) ↔ LenBit 0 a

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
this : 0 ≤ i
pos : 0 < i
⊢ LenBit i (a + b) ↔ LenBit i a
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
h : 2 * i ∣ b
this : 0 ≤ i
pos : 0 < i
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
rcases h with ⟨b', hb'⟩
Proof state after:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb' : b = 2 * i * b'
⊢ LenBit i (a + b) ↔ LenBit i a
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb' : b = 2 * i * b'
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
have hb' : b = 2 * b' * i := by simp [hb', mul_right_comm]
Proof state after:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb'✝ : b = 2 * i * b'
hb' : b = 2 * b' * i
⊢ LenBit i (a + b) ↔ LenBit i a
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb'✝ : b = 2 * i * b'
hb' : b = 2 * b' * i
⊢ LenBit i (a + b) ↔ LenBit i a
Tactic:
calc
  LenBit i (a + b) ↔ ((a + b) / i) % 2 = 1    := LenBit.iff_rem
  _                ↔ (a / i + 2 * b') % 2 = 1 := by rw [hb', div_add_mul_self _ _ pos]
  _                ↔ LenBit i a               := by simp [LenBit.iff_rem]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : 2 * 0 ∣ b
this : 0 ≤ 0
⊢ LenBit 0 (a + b) ↔ LenBit 0 a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb' : b = 2 * i * b'
⊢ b = 2 * b' * i
Tactic:
simp [hb', mul_right_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb'✝ : b = 2 * i * b'
hb' : b = 2 * b' * i
⊢ (a + b) / i % 2 = 1 ↔ (a / i + 2 * b') % 2 = 1
Tactic:
rw [hb', div_add_mul_self _ _ pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.add
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a b : M
this : 0 ≤ i
pos : 0 < i
b' : M
hb'✝ : b = 2 * i * b'
hb' : b = 2 * b' * i
⊢ (a / i + 2 * b') % 2 = 1 ↔ LenBit i a
Tactic:
simp [LenBit.iff_rem]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.add_self
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : a < i
⊢ LenBit i (a + i)
Tactic:
have pos : 0 < i := by exact pos_of_gt h
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : a < i
pos : 0 < i
⊢ LenBit i (a + i)
Theorem: LO.FirstOrder.Arith.Model.LenBit.add_self
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : a < i
pos : 0 < i
⊢ LenBit i (a + i)
Tactic:
simp [LenBit.iff_rem, div_add_self_right _ pos, h, one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.add_self
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
i a : M
h : a < i
⊢ 0 < i
Tactic:
exact pos_of_gt h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.LenBit.add_self_of_not_lenbit
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a i : M
pos : 0 < i
h : ¬LenBit i a
⊢ LenBit i (a + i)
Tactic:
have : a / i % 2 = 0 := by simpa [LenBit.iff_rem] using h
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a i : M
pos : 0 < i
h : ¬LenBit i a
this : a / i % 2 = 0
⊢ LenBit i (a + i)
Theorem: LO.FirstOrder.Arith.Model.LenBit.add_self_of_not_lenbit
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a i : M
pos : 0 < i
h : ¬LenBit i a
this : a / i % 2 = 0
⊢ LenBit i (a + i)
Tactic:
simp [LenBit.iff_rem, div_add_self_right, pos]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a i : M
pos : 0 < i
h : ¬LenBit i a
this : a / i % 2 = 0
⊢ (a / i + 1) % 2 = 1