Theorem: LO.FirstOrder.Arith.Model.sppow2_defined (Arithmetization/ISigmaZero/Exponential/PPow2.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate SPPow2 via sppow2Def
Tactic:
intro v
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
⊢ (fun v => SPPow2 (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val sppow2Def)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
⊢ (fun v => SPPow2 (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val sppow2Def)
Tactic:
simp [SPPow2, sppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.df.iff,
  pow2_defined.df.iff, sqrt_defined.df.iff, ←le_iff_lt_succ, sq, numeral_eq_natCast]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
⊢ ¬LenBit 1 (v 0) →
    LenBit 2 (v 0) →
      ((∀ i ≤ v 0, Pow2 i → 2 < i → (LenBit i (v 0) ↔ √i * √i = i ∧ LenBit (√i) (v 0))) ↔
        ∀ x ≤ v 0, Pow2 x → 2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)))

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
⊢ ¬LenBit 1 (v 0) →
    LenBit 2 (v 0) →
      ((∀ i ≤ v 0, Pow2 i → 2 < i → (LenBit i (v 0) ↔ √i * √i = i ∧ LenBit (√i) (v 0))) ↔
        ∀ x ≤ v 0, Pow2 x → 2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)))
Tactic:
intro _ _
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝¹ : ¬LenBit 1 (v 0)
a✝ : LenBit 2 (v 0)
⊢ (∀ i ≤ v 0, Pow2 i → 2 < i → (LenBit i (v 0) ↔ √i * √i = i ∧ LenBit (√i) (v 0))) ↔
    ∀ x ≤ v 0, Pow2 x → 2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0))

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝¹ : ¬LenBit 1 (v 0)
a✝ : LenBit 2 (v 0)
⊢ (∀ i ≤ v 0, Pow2 i → 2 < i → (LenBit i (v 0) ↔ √i * √i = i ∧ LenBit (√i) (v 0))) ↔
    ∀ x ≤ v 0, Pow2 x → 2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0))
Tactic:
apply forall₂_congr
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝¹ : ¬LenBit 1 (v 0)
a✝ : LenBit 2 (v 0)
⊢ ∀ a ≤ v 0,
    Pow2 a → 2 < a → (LenBit a (v 0) ↔ √a * √a = a ∧ LenBit (√a) (v 0)) ↔
      Pow2 a → 2 < a → (LenBit a (v 0) ↔ ∃ x ≤ a, x = √a ∧ x * x = a ∧ LenBit x (v 0))

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝¹ : ¬LenBit 1 (v 0)
a✝ : LenBit 2 (v 0)
⊢ ∀ a ≤ v 0,
    Pow2 a → 2 < a → (LenBit a (v 0) ↔ √a * √a = a ∧ LenBit (√a) (v 0)) ↔
      Pow2 a → 2 < a → (LenBit a (v 0) ↔ ∃ x ≤ a, x = √a ∧ x * x = a ∧ LenBit x (v 0))
Tactic:
intro x _
State after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝¹ : ¬LenBit 1 (v 0)
a✝ : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
⊢ Pow2 x → 2 < x → (LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
    Pow2 x → 2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0))

State before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝¹ : ¬LenBit 1 (v 0)
a✝ : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
⊢ Pow2 x → 2 < x → (LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
    Pow2 x → 2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0))
Tactic:
apply imp_congr_right
State after:
case h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝¹ : ¬LenBit 1 (v 0)
a✝ : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
⊢ Pow2 x →
    (2 < x → (LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
      2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)))

State before:
case h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝¹ : ¬LenBit 1 (v 0)
a✝ : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
⊢ Pow2 x →
    (2 < x → (LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
      2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)))
Tactic:
intro _
State after:
case h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝² : ¬LenBit 1 (v 0)
a✝¹ : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝ : Pow2 x
⊢ 2 < x → (LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
    2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0))

State before:
case h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝² : ¬LenBit 1 (v 0)
a✝¹ : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝ : Pow2 x
⊢ 2 < x → (LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
    2 < x → (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0))
Tactic:
apply imp_congr_right
State after:
case h.h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝² : ¬LenBit 1 (v 0)
a✝¹ : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝ : Pow2 x
⊢ 2 < x →
    ((LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
      (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)))

State before:
case h.h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝² : ¬LenBit 1 (v 0)
a✝¹ : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝ : Pow2 x
⊢ 2 < x →
    ((LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
      (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)))
Tactic:
intro _
State after:
case h.h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ (LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
    (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0))

State before:
case h.h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ (LenBit x (v 0) ↔ √x * √x = x ∧ LenBit (√x) (v 0)) ↔
    (LenBit x (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0))
Tactic:
apply iff_congr
State after:
case h.h.h.h₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ LenBit x (v 0) ↔ LenBit x (v 0)

case h.h.h.h₂
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ √x * √x = x ∧ LenBit (√x) (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)

State before:
case h.h.h.h₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ LenBit x (v 0) ↔ LenBit x (v 0)
Tactic:
simp
State after:
no goals

State before:
case h.h.h.h₂
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ √x * √x = x ∧ LenBit (√x) (v 0) ↔ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)
Tactic:
constructor
State after:
case h.h.h.h₂.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ √x * √x = x ∧ LenBit (√x) (v 0) → ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)

case h.h.h.h₂.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ (∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)) → √x * √x = x ∧ LenBit (√x) (v 0)

State before:
case h.h.h.h₂.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ √x * √x = x ∧ LenBit (√x) (v 0) → ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)
Tactic:
intro h
State after:
case h.h.h.h₂.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
h : √x * √x = x ∧ LenBit (√x) (v 0)
⊢ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)

State before:
case h.h.h.h₂.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
h : √x * √x = x ∧ LenBit (√x) (v 0)
⊢ ∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)
Tactic:
exact ⟨√x, by simpa using 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 ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
h : √x * √x = x ∧ LenBit (√x) (v 0)
⊢ √x ≤ x ∧ √x = √x ∧ √x * √x = x ∧ LenBit (√x) (v 0)
Tactic:
simpa using h
State after:
no goals

State before:
case h.h.h.h₂.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
⊢ (∃ x_1 ≤ x, x_1 = √x ∧ x_1 * x_1 = x ∧ LenBit x_1 (v 0)) → √x * √x = x ∧ LenBit (√x) (v 0)
Tactic:
rintro ⟨_, _, rfl, h⟩
State after:
case h.h.h.h₂.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 ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
left✝ : √x ≤ x
h : √x * √x = x ∧ LenBit (√x) (v 0)
⊢ √x * √x = x ∧ LenBit (√x) (v 0)

State before:
case h.h.h.h₂.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 ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
a✝³ : ¬LenBit 1 (v 0)
a✝² : LenBit 2 (v 0)
x : M
b✝ : x ≤ v 0
a✝¹ : Pow2 x
a✝ : 2 < x
left✝ : √x ≤ x
h : √x * √x = x ∧ LenBit (√x) (v 0)
⊢ √x * √x = x ∧ LenBit (√x) (v 0)
Tactic:
exact h
State after:
no goals