internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
⊢ P x
Tactic:
rcases zero_le x 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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
IH : ∀ y < 0, P y
⊢ P 0

case inr
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
⊢ P x
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
IH : ∀ y < 0, P y
⊢ P 0
Tactic:
exact zero
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
⊢ P x
Tactic:
have : x / 2 < x := div_lt_of_pos_of_one_lt pos one_lt_two
Proof state after:
case inr
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
⊢ P x
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
⊢ P x
Tactic:
rcases even_or_odd' x with (hx | hx)
Proof state after:
case inr.inl
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
⊢ P x

case inr.inr
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2) + 1
⊢ P x
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
case inr.inl
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
⊢ P x
Tactic:
simpa [←hx] using even (x / 2) (by by_contra A; simp at A; simp [show x = 0 from by simpa [A] using hx] at pos) (IH (x / 2) this)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
⊢ x / 2 > 0
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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : ¬x / 2 > 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : ¬x / 2 > 0
⊢ False
Tactic:
simp at 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 ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : x / 2 = 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : x / 2 = 0
⊢ False
Tactic:
simp [show x = 0 from by simpa [A] using hx] at pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2)
A : x / 2 = 0
⊢ x = 0
Tactic:
simpa [A] using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
case inr.inr
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
IH : ∀ y < x, P y
pos : 0 < x
this : x / 2 < x
hx : x = 2 * (x / 2) + 1
⊢ P x
Tactic:
simpa [←hx] using odd (x / 2) (IH (x / 2) this)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sppow2_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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate SPPow2 via sppow2Def
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 ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
⊢ (fun v => SPPow2 (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val sppow2Def)
Theorem: LO.FirstOrder.Arith.Model.sppow2_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 ⊧ₘ* 𝐈𝚫₀
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]
Proof 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)))
Theorem: LO.FirstOrder.Arith.Model.sppow2_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 ⊧ₘ* 𝐈𝚫₀
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 _ _
Proof 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))
Theorem: LO.FirstOrder.Arith.Model.sppow2_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 ⊧ₘ* 𝐈𝚫₀
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
Proof 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))
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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 _
Proof 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))
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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
Proof 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)))
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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 _
Proof 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))
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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
Proof 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)))
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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 _
Proof 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))
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sppow2_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 ⊧ₘ* 𝐈𝚫₀
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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⟩
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.sppow2_defined
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ppow2_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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate PPow2 via ppow2Def
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 ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
⊢ (fun v => PPow2 (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val ppow2Def)
Theorem: LO.FirstOrder.Arith.Model.ppow2_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 ⊧ₘ* 𝐈𝚫₀
v : Fin 1 → M
⊢ (fun v => PPow2 (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val ppow2Def)
Tactic:
simp[PPow2, ppow2Def, Matrix.vecHead, Matrix.vecTail,
lenbit_defined.df.iff, pow2_defined.df.iff, sppow2_defined.df.iff, numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.SPPow2.one_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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
hi : LenBit i m
⊢ 1 < i
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 ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
hi : LenBit i m
A : ¬1 < i
⊢ False