internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_two
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ a ≤ b
Tactic:
suffices a ∣ b from le_of_dvd hb.pos this
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ a ∣ b
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_two
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ a ∣ b
Tactic:
have : a / 2 ∣ b := by
  have : 2 * (a / 2) ∣ 2 * b := by
    simpa [ha.two_mul_div_two ea] using dvd_of_le ha (by simpa using hb) (LT.lt.le h)
  exact (mul_dvd_mul_iff_left (by simp)).mp this
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
this : a / 2 ∣ b
⊢ a ∣ b
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_two
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
this : a / 2 ∣ b
⊢ a ∣ b
Tactic:
rcases this with ⟨b', rfl⟩
Proof state after:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
⊢ a ∣ a / 2 * b'
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_two
Proof state before:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
⊢ a ∣ a / 2 * b'
Tactic:
have hb' : Pow2 b' := by simp at hb; exact hb.2
Proof state after:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
⊢ a ∣ a / 2 * b'
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_two
Proof state before:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
⊢ a ∣ a / 2 * b'
Tactic:
have : 2 ∣ b' := hb'.two_dvd' (by rintro rfl; simp [ha.two_mul_div_two ea] at h)
Proof state after:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
this : 2 ∣ b'
⊢ a ∣ a / 2 * b'
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_two
Proof state before:
case neg.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
this : 2 ∣ b'
⊢ a ∣ a / 2 * b'
Tactic:
rcases this with ⟨b'', rfl⟩
Proof state after:
case neg.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
ha : Pow2 a
ea : ¬a = 1
b'' : M
hb : Pow2 (a / 2 * (2 * b''))
h : a < 2 * (a / 2 * (2 * b''))
hb' : Pow2 (2 * b'')
⊢ a ∣ a / 2 * (2 * b'')
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_two
Proof state before:
case neg.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
ha : Pow2 a
ea : ¬a = 1
b'' : M
hb : Pow2 (a / 2 * (2 * b''))
h : a < 2 * (a / 2 * (2 * b''))
hb' : Pow2 (2 * b'')
⊢ a ∣ a / 2 * (2 * b'')
Tactic:
simp [←mul_assoc, ha.div_two_mul_two ea]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ a / 2 ∣ b
Tactic:
have : 2 * (a / 2) ∣ 2 * b := by
  simpa [ha.two_mul_div_two ea] using dvd_of_le ha (by simpa using hb) (LT.lt.le 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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
this : 2 * (a / 2) ∣ 2 * b
⊢ a / 2 ∣ b
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
this : 2 * (a / 2) ∣ 2 * b
⊢ a / 2 ∣ b
Tactic:
exact (mul_dvd_mul_iff_left (by simp)).mp this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ 2 * (a / 2) ∣ 2 * b
Tactic:
simpa [ha.two_mul_div_two ea] using dvd_of_le ha (by simpa using hb) (LT.lt.le h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
⊢ Pow2 (2 * b)
Tactic:
simpa using hb
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
h : a < 2 * b
ea : ¬a = 1
this : 2 * (a / 2) ∣ 2 * b
⊢ 2 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
⊢ Pow2 b'
Tactic:
simp at hb
Proof 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
ha : Pow2 a
ea : ¬a = 1
b' : M
h : a < 2 * (a / 2 * b')
hb : Pow2 (a / 2) ∧ Pow2 b'
⊢ Pow2 b'
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
h : a < 2 * (a / 2 * b')
hb : Pow2 (a / 2) ∧ Pow2 b'
⊢ Pow2 b'
Tactic:
exact hb.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
b' : M
hb : Pow2 (a / 2 * b')
h : a < 2 * (a / 2 * b')
hb' : Pow2 b'
⊢ b' ≠ 1
Tactic:
rintro rfl
Proof 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
ha : Pow2 a
ea : ¬a = 1
hb : Pow2 (a / 2 * 1)
h : a < 2 * (a / 2 * 1)
hb' : Pow2 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Pow2.le_iff_lt_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 ⊧ₘ* 𝐈𝚫₀
a : M
ha : Pow2 a
ea : ¬a = 1
hb : Pow2 (a / 2 * 1)
h : a < 2 * (a / 2 * 1)
hb' : Pow2 1
⊢ False
Tactic:
simp [ha.two_mul_div_two ea] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.lt_iff_two_mul_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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
⊢ a < b ↔ 2 * a ≤ b
Tactic:
by_cases eb : b = 1
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : b = 1
⊢ a < b ↔ 2 * a ≤ b

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : ¬b = 1
⊢ a < b ↔ 2 * a ≤ b
Theorem: LO.FirstOrder.Arith.Model.Pow2.lt_iff_two_mul_le
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : b = 1
⊢ a < b ↔ 2 * a ≤ b
Tactic:
simp [eb, ←lt_two_iff_le_one]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.lt_iff_two_mul_le
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : ¬b = 1
⊢ a < b ↔ 2 * a ≤ b
Tactic:
rw [←hb.two_mul_div_two eb]
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : ¬b = 1
⊢ a < 2 * (b / 2) ↔ 2 * a ≤ 2 * (b / 2)
Theorem: LO.FirstOrder.Arith.Model.Pow2.lt_iff_two_mul_le
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 ⊧ₘ* 𝐈𝚫₀
a b : M
ha : Pow2 a
hb : Pow2 b
eb : ¬b = 1
⊢ a < 2 * (b / 2) ↔ 2 * a ≤ 2 * (b / 2)
Tactic:
simp [le_iff_lt_two ha (hb.div_two eb)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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'⟩)
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 ⊧ₘ* 𝐈𝚫₀
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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
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 ⊧ₘ* 𝐈𝚫₀
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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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)⟩
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
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 ⊧ₘ* 𝐈𝚫₀
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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
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 ⊧ₘ* 𝐈𝚫₀
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
Proof 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
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 ⊧ₘ* 𝐈𝚫₀
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
Theorem: LO.FirstOrder.Arith.Model.Pow2.sq_or_dsq
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 ⊧ₘ* 𝐈𝚫₀
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.sqrt
Proof 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
h : Pow2 a
hsq : (√a) ^ 2 = a
⊢ Pow2 (√a)
Tactic:
rw [←hsq] at 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 ⊧ₘ* 𝐈𝚫₀
a : M
h : Pow2 ((√a) ^ 2)
hsq : (√a) ^ 2 = a
⊢ Pow2 (√a)
Theorem: LO.FirstOrder.Arith.Model.Pow2.sqrt
Proof 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
h : Pow2 ((√a) ^ 2)
hsq : (√a) ^ 2 = a
⊢ Pow2 (√a)
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.not_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ ¬Pow2 3
Tactic:
intro 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 ⊧ₘ* 𝐈𝚫₀
h : Pow2 3
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Pow2.not_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : Pow2 3
⊢ False
Tactic:
have : (2 : M) ∣ 3 := h.two_dvd (by simp [←two_add_one_eq_three])
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : Pow2 3
this : 2 ∣ 3
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Pow2.not_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : Pow2 3
this : 2 ∣ 3
⊢ False
Tactic:
simp [←two_add_one_eq_three, ←mod_eq_zero_iff_dvd, one_lt_two] at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.not_three
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h : Pow2 3
⊢ 1 < 3
Tactic:
simp [←two_add_one_eq_three]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.four_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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : Pow2 i
lt : 2 < i
⊢ 4 ≤ 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 ⊧ₘ* 𝐈𝚫₀
i : M
hi : Pow2 i
lt : 2 < i
A : ¬4 ≤ i
⊢ False