internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₂
⊢ ∃ z', z₂ = z' * u * u
Tactic:
rcases h with ⟨u', rfl⟩
Proof state after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ ∃ z', u ^ 2 * u' = z' * u * u
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right
Proof state before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ ∃ z', u ^ 2 * u' = z' * u * u
Tactic:
exact ⟨u', by simp [mul_comm _ u', mul_assoc]; simp [sq]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ u ^ 2 * u' = u' * u * u
Tactic:
simp [mul_comm _ u', mul_assoc]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ u ^ 2 = u * u ∨ u' = 0
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_right
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ : M
pos : 0 < u
u' : M
⊢ u ^ 2 = u * u ∨ u' = 0
Tactic:
simp [sq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_left
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₁
⊢ ext u (z₁ + z₂) = ext u z₂
Tactic:
rw [add_comm]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₁
⊢ ext u (z₂ + z₁) = ext u z₂
Theorem: LO.FirstOrder.Arith.Model.ext_add_of_dvd_sq_left
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
u z₁ z₂ : M
pos : 0 < u
h : u ^ 2 ∣ z₁
⊢ ext u (z₂ + z₁) = ext u z₂
Tactic:
exact ext_add_of_dvd_sq_right pos h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_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 ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
⊢ ext i (z % j) = ext i z
Tactic:
have := div_add_mod z j
Proof 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 z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this : j * (z / j) + z % j = z
⊢ ext i (z % j) = ext i z
Theorem: LO.FirstOrder.Arith.Model.ext_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 ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this : j * (z / j) + z % j = z
⊢ ext i (z % j) = ext i z
Tactic:
have : i^2 ∣ j := ppi.pow2.sq.dvd_of_le ppj.pow2 (PPow2.sq_le_of_lt ppi ppj hij)
Proof 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 z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (z % j) = ext i z
Theorem: LO.FirstOrder.Arith.Model.ext_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 ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (z % j) = ext i z
Tactic:
calc
  ext i (z % j) = ext i (j * (z / j) + (z % j)) := by symm; exact ext_add_of_dvd_sq_left ppi.pos (Dvd.dvd.mul_right this (z / j))
  _               = ext i z                          := by simp [div_add_mod]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_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 ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (z % j) = ext i (j * (z / j) + z % j)
Tactic:
symm
Proof 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 z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (j * (z / j) + z % j) = ext i (z % j)
Theorem: LO.FirstOrder.Arith.Model.ext_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 ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (j * (z / j) + z % j) = ext i (z % j)
Tactic:
exact ext_add_of_dvd_sq_left ppi.pos (Dvd.dvd.mul_right this (z / j))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.ext_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 ⊧ₘ* 𝐈𝚫₀
i j z : M
ppi : PPow2 i
ppj : PPow2 j
hij : i < j
this✝ : j * (z / j) + z % j = z
this : i ^ 2 ∣ j
⊢ ext i (j * (z / j) + z % j) = ext i z
Tactic:
simp [div_add_mod]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
⊢ Seqₛ y X Y →
    ∀ u ≤ y,
      u ≠ 2 →
        PPow2 u →
          ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
              ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
            (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
              ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Tactic:
intro H u hu ne2 ppu
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Tactic:
rcases H u hu ne2 ppu with (H | H)
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Tactic:
exact Or.inl ⟨⟨ext u X, by simp [H.1]⟩, ⟨ext u Y, by simp [H.2]⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ext u X ≤ X ∧ ext u X = ext u X ∧ 2 * ext u X = ext (u ^ 2) X
Tactic:
simp [H.1]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ext u Y ≤ Y ∧ ext u Y = ext u Y ∧ ext u Y ^ 2 = ext (u ^ 2) Y
Tactic:
simp [H.2]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Tactic:
exact Or.inr ⟨⟨ext u X, by simp [H.1]⟩, ⟨ext u Y, by simp [H.2]⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ext u X ≤ X ∧ ext u X = ext u X ∧ 2 * ext u X + 1 = ext (u ^ 2) X
Tactic:
simp [H.1]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ext u Y ≤ Y ∧ ext u Y = ext u Y ∧ 2 * ext u Y ^ 2 = ext (u ^ 2) Y
Tactic:
simp [H.2]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
⊢ (∀ u ≤ y,
      u ≠ 2 →
        PPow2 u →
          ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
              ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
            (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
              ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y) →
    Seqₛ y X Y
Tactic:
intro H u hu ne2 ppu
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ Even X Y u ∨ Odd X Y u
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ Even X Y u ∨ Odd X Y u
Tactic:
rcases H u hu ne2 ppu with (⟨⟨_, _, rfl, hx⟩, ⟨_, _, rfl, hy⟩⟩ | ⟨⟨_, _, rfl, hx⟩, ⟨_, _, rfl, hy⟩⟩)
Proof state after:
case inl.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : ext u Y ^ 2 = ext (u ^ 2) Y
⊢ Even X Y u ∨ Odd X Y u

case inr.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X + 1 = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : 2 * ext u Y ^ 2 = ext (u ^ 2) Y
⊢ Even X Y u ∨ Odd X Y u
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
case inl.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : ext u Y ^ 2 = ext (u ^ 2) Y
⊢ Even X Y u ∨ Odd X Y u
Tactic:
exact Or.inl ⟨by simp [hx, hy], by simp [hx, hy]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : ext u Y ^ 2 = ext (u ^ 2) Y
⊢ ext (u ^ 2) X = 2 * ext u X
Tactic:
simp [hx, hy]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : ext u Y ^ 2 = ext (u ^ 2) Y
⊢ ext (u ^ 2) Y = ext u Y ^ 2
Tactic:
simp [hx, hy]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X + 1 = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : 2 * ext u Y ^ 2 = ext (u ^ 2) Y
⊢ Even X Y u ∨ Odd X Y u
Tactic:
exact Or.inr ⟨by simp [hx, hy], by simp [hx, hy]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X + 1 = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : 2 * ext u Y ^ 2 = ext (u ^ 2) Y
⊢ ext (u ^ 2) X = 2 * ext u X + 1
Tactic:
simp [hx, hy]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X + 1 = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : 2 * ext u Y ^ 2 = ext (u ^ 2) Y
⊢ ext (u ^ 2) Y = 2 * ext u Y ^ 2
Tactic:
simp [hx, hy]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Relation₃ Seqₛ via def
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 3 → M
⊢ (fun v => Seqₛ (v 0) (v 1) (v 2)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val def)
Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.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 3 → M
⊢ (fun v => Seqₛ (v 0) (v 1) (v 2)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val def)
Tactic:
simp [Exponential.Seqₛ.iff, Exponential.Seqₛ.def, ppow2_defined.df.iff,
ext_defined.df.iff, ←le_iff_lt_succ, sq, numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.graph_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
⊢ Exponential x y →
    x = 0 ∧ y = 1 ∨
      ∃ X ≤ y ^ 4,
        ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y
Tactic:
rintro (H | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, hX, hY⟩⟩)
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : x = 0 ∧ y = 1
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y

case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
bX : X ≤ y ^ 4
Y : M
bY : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : ext u X = x
hY : ext u Y = y
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y
Theorem: LO.FirstOrder.Arith.Model.Exponential.graph_iff
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : x = 0 ∧ y = 1
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y
Tactic:
exact Or.inl H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.graph_iff
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
bX : X ≤ y ^ 4
Y : M
bY : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : ext u X = x
hY : ext u Y = y
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y
Tactic:
exact Or.inr ⟨X, bX, Y, bY, ⟨H₀.1.symm, H₀.2.symm⟩, Hₛ, ⟨u, hu, ne2, ppu, hX.symm, hY.symm⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.graph_iff
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
⊢ (x = 0 ∧ y = 1 ∨
      ∃ X ≤ y ^ 4,
        ∃ Y ≤ y ^ 4,
          (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y) →
    Exponential x y
Tactic:
rintro (H | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, hX, hY⟩⟩)
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : x = 0 ∧ y = 1
⊢ Exponential x y

case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
bX : X ≤ y ^ 4
Y : M
bY : Y ≤ y ^ 4
H₀ : 1 = ext 4 X ∧ 2 = ext 4 Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : x = ext u X
hY : y = ext u Y
⊢ Exponential x y
Theorem: LO.FirstOrder.Arith.Model.Exponential.graph_iff
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 ⊧ₘ* 𝐈𝚫₀
x y : M
H : x = 0 ∧ y = 1
⊢ Exponential x y
Tactic:
exact Or.inl H
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Exponential.graph_iff
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
bX : X ≤ y ^ 4
Y : M
bY : Y ≤ y ^ 4
H₀ : 1 = ext 4 X ∧ 2 = ext 4 Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : x = ext u X
hY : y = ext u Y
⊢ Exponential x y
Tactic:
exact Or.inr ⟨X, bX, Y, bY, ⟨H₀.1.symm, H₀.2.symm⟩, Hₛ, ⟨u, hu, ne2, ppu, hX.symm, hY.symm⟩⟩
Proof state after:
no goals