Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq (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 : M
pa : Pow2 a
⊢ ∃ b, a = b ^ 2 ∨ a = 2 * b ^ 2
Tactic:
suffices ∃ b ≤ a, a = b^2 ∨ a = 2 * b^2 by
  rcases this with ⟨b, _, h⟩
  exact ⟨b, 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 : M
pa : Pow2 a
⊢ ∃ b ≤ a, a = b ^ 2 ∨ a = 2 * b ^ 2

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa : Pow2 a
⊢ ∃ b ≤ a, a = b ^ 2 ∨ a = 2 * b ^ 2
Tactic:
induction a using order_induction_iSigmaZero
State after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {a} => Pow2 a → ∃ b ≤ a, a = b ^ 2 ∨ a = 2 * b ^ 2

case ind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x✝ : M
a✝ : ∀ y < x✝, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 x✝
⊢ ∃ b ≤ x✝, x✝ = b ^ 2 ∨ x✝ = 2 * b ^ 2

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa : Pow2 a
this : ∃ b ≤ a, a = b ^ 2 ∨ a = 2 * b ^ 2
⊢ ∃ b, a = b ^ 2 ∨ a = 2 * b ^ 2
Tactic:
rcases this with ⟨b, _, h⟩
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa : Pow2 a
b : M
left✝ : b ≤ a
h : a = b ^ 2 ∨ a = 2 * b ^ 2
⊢ ∃ b, a = b ^ 2 ∨ a = 2 * b ^ 2

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa : Pow2 a
b : M
left✝ : b ≤ a
h : a = b ^ 2 ∨ a = 2 * b ^ 2
⊢ ∃ b, a = b ^ 2 ∨ a = 2 * b ^ 2
Tactic:
exact ⟨b, h⟩
State after:
no goals

State before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {a} => Pow2 a → ∃ b ≤ a, a = b ^ 2 ∨ a = 2 * b ^ 2
Tactic:
definability
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 : M
IH : ∀ y < a, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 a
⊢ ∃ b ≤ a, a = b ^ 2 ∨ a = 2 * b ^ 2
Tactic:
rcases Pow2.elim'.mp pa with (rfl | ⟨ha, a, rfl, pa'⟩)
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 ⊧ₘ* 𝐈𝚫₀
IH : ∀ y < 1, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 1
⊢ ∃ b ≤ 1, 1 = b ^ 2 ∨ 1 = 2 * b ^ 2

case inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa' : Pow2 a
IH : ∀ y < 2 * a, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * a)
ha : 1 < 2 * a
⊢ ∃ b ≤ 2 * a, 2 * a = b ^ 2 ∨ 2 * a = 2 * b ^ 2

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 ⊧ₘ* 𝐈𝚫₀
IH : ∀ y < 1, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 1
⊢ ∃ b ≤ 1, 1 = b ^ 2 ∨ 1 = 2 * b ^ 2
Tactic:
exact ⟨1, by simp⟩
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 ⊧ₘ* 𝐈𝚫₀
IH : ∀ y < 1, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 1
⊢ 1 ≤ 1 ∧ (1 = 1 ^ 2 ∨ 1 = 2 * 1 ^ 2)
Tactic:
simp
State after:
no goals

State before:
case inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa' : Pow2 a
IH : ∀ y < 2 * a, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * a)
ha : 1 < 2 * a
⊢ ∃ b ≤ 2 * a, 2 * a = b ^ 2 ∨ 2 * a = 2 * b ^ 2
Tactic:
have : 0 < a := by simpa [←pos_iff_one_le] using one_lt_iff_two_le.mp ha
State after:
case inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa' : Pow2 a
IH : ∀ y < 2 * a, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * a)
ha : 1 < 2 * a
this : 0 < a
⊢ ∃ b ≤ 2 * a, 2 * a = b ^ 2 ∨ 2 * a = 2 * b ^ 2

State before:
case inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa' : Pow2 a
IH : ∀ y < 2 * a, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * a)
ha : 1 < 2 * a
this : 0 < a
⊢ ∃ b ≤ 2 * a, 2 * a = b ^ 2 ∨ 2 * a = 2 * b ^ 2
Tactic:
rcases IH a (lt_mul_of_one_lt_left this one_lt_two) pa' with ⟨b, _, (rfl | rfl)⟩
State after:
case inr.intro.intro.intro.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (b ^ 2)
IH : ∀ y < 2 * b ^ 2, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * b ^ 2)
ha : 1 < 2 * b ^ 2
this : 0 < b ^ 2
left✝ : b ≤ b ^ 2
⊢ ∃ b_1 ≤ 2 * b ^ 2, 2 * b ^ 2 = b_1 ^ 2 ∨ 2 * b ^ 2 = 2 * b_1 ^ 2

case inr.intro.intro.intro.intro.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ ∃ b_1 ≤ 2 * (2 * b ^ 2), 2 * (2 * b ^ 2) = b_1 ^ 2 ∨ 2 * (2 * b ^ 2) = 2 * b_1 ^ 2

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa' : Pow2 a
IH : ∀ y < 2 * a, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * a)
ha : 1 < 2 * a
⊢ 0 < a
Tactic:
simpa [←pos_iff_one_le] using one_lt_iff_two_le.mp ha
State after:
no goals

State before:
case inr.intro.intro.intro.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (b ^ 2)
IH : ∀ y < 2 * b ^ 2, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * b ^ 2)
ha : 1 < 2 * b ^ 2
this : 0 < b ^ 2
left✝ : b ≤ b ^ 2
⊢ ∃ b_1 ≤ 2 * b ^ 2, 2 * b ^ 2 = b_1 ^ 2 ∨ 2 * b ^ 2 = 2 * b_1 ^ 2
Tactic:
exact ⟨b, le_trans (by simp) le_two_mul_left, by right; rfl⟩
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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (b ^ 2)
IH : ∀ y < 2 * b ^ 2, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * b ^ 2)
ha : 1 < 2 * b ^ 2
this : 0 < b ^ 2
left✝ : b ≤ b ^ 2
⊢ b ≤ b ^ 2
Tactic:
simp
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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (b ^ 2)
IH : ∀ y < 2 * b ^ 2, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * b ^ 2)
ha : 1 < 2 * b ^ 2
this : 0 < b ^ 2
left✝ : b ≤ b ^ 2
⊢ 2 * b ^ 2 = b ^ 2 ∨ 2 * b ^ 2 = 2 * b ^ 2
Tactic:
right
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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (b ^ 2)
IH : ∀ y < 2 * b ^ 2, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * b ^ 2)
ha : 1 < 2 * b ^ 2
this : 0 < b ^ 2
left✝ : b ≤ b ^ 2
⊢ 2 * b ^ 2 = 2 * b ^ 2

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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (b ^ 2)
IH : ∀ y < 2 * b ^ 2, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * b ^ 2)
ha : 1 < 2 * b ^ 2
this : 0 < b ^ 2
left✝ : b ≤ b ^ 2
⊢ 2 * b ^ 2 = 2 * b ^ 2
Tactic:
rfl
State after:
no goals

State before:
case inr.intro.intro.intro.intro.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ ∃ b_1 ≤ 2 * (2 * b ^ 2), 2 * (2 * b ^ 2) = b_1 ^ 2 ∨ 2 * (2 * b ^ 2) = 2 * b_1 ^ 2
Tactic:
exact ⟨2 * b, by simp; exact le_trans (by simp) le_two_mul_left,
by left; simp [_root_.sq, mul_assoc, mul_left_comm]⟩
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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ 2 * b ≤ 2 * (2 * b ^ 2)
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ b ≤ 2 * b ^ 2

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ b ≤ 2 * b ^ 2
Tactic:
exact le_trans (by simp) le_two_mul_left
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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ b ≤ b ^ 2
Tactic:
simp
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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ 2 * (2 * b ^ 2) = (2 * b) ^ 2 ∨ 2 * (2 * b ^ 2) = 2 * (2 * b) ^ 2
Tactic:
left
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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ 2 * (2 * b ^ 2) = (2 * b) ^ 2

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 ⊧ₘ* 𝐈𝚫₀
b : M
pa' : Pow2 (2 * b ^ 2)
IH : ∀ y < 2 * (2 * b ^ 2), Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * (2 * b ^ 2))
ha : 1 < 2 * (2 * b ^ 2)
this : 0 < 2 * b ^ 2
left✝ : b ≤ 2 * b ^ 2
⊢ 2 * (2 * b ^ 2) = (2 * b) ^ 2
Tactic:
simp [_root_.sq, mul_assoc, mul_left_comm]
State after:
no goals