internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.least_number_h
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 ⊧ₘ* 𝐏𝐀⁻
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
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
w : M
hx✝ : w < x + 1
hw : P w
hx : w < x
⊢ False
Tactic:
exact IH w hx hw
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
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 ⊧ₘ* 𝐏𝐀⁻
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
⊢ False
Tactic:
have : ∃ v < w, P v := A w hw
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 ⊧ₘ* 𝐏𝐀⁻
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
this : ∃ v < w, P v
⊢ False
Theorem: LO.FirstOrder.Arith.Model.least_number_h
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 ⊧ₘ* 𝐏𝐀⁻
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
this : ∃ v < w, P v
⊢ False
Tactic:
rcases this with ⟨v, hvw, hv⟩
Proof state after:
case inr.intro.intro
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
v : M
hvw : v < w
hv : P v
⊢ False
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof state before:
case inr.intro.intro
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
v : M
hvw : v < w
hv : P v
⊢ False
Tactic:
exact IH v hvw hv
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof state before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ Structure.ORing L M
Tactic:
exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof state before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ.alt m)
Tactic:
exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof state before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
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
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
this : ∀ (z w : M), w < z → ¬P w
⊢ x < x + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_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 ⊧ₘ* 𝐈open
⊢ 𝚺₀-Predicate Pow2 via pow2Def
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 ⊧ₘ* 𝐈open
v : Fin 1 → M
⊢ (fun v => Pow2 (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val pow2Def)
Theorem: LO.FirstOrder.Arith.Model.pow2_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 ⊧ₘ* 𝐈open
v : Fin 1 → M
⊢ (fun v => Pow2 (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val pow2Def)
Tactic:
simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.vecHead, Matrix.constant_eq_singleton,
  Pow2, pow2Def, le_iff_lt_succ, dvd_defined.df.iff, numeral_eq_natCast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
⊢ 0 < 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
⊢ ∀ r ≤ 1, 1 < r → r ∣ 1 → 2 ∣ r
Tactic:
intro r hr hhr hd
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
r : M
hr : r ≤ 1
hhr : 1 < r
hd : r ∣ 1
⊢ 2 ∣ r
Theorem: LO.FirstOrder.Arith.Model.pow2_one
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
r : M
hr : r ≤ 1
hhr : 1 < r
hd : r ∣ 1
⊢ 2 ∣ r
Tactic:
rcases show r = 0 ∨ r = 1 from le_one_iff_eq_zero_or_one.mp hr with (rfl | rfl)
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 ⊧ₘ* 𝐈open
hr : 0 ≤ 1
hhr : 1 < 0
hd : 0 ∣ 1
⊢ 2 ∣ 0

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
hr : 1 ≤ 1
hhr : 1 < 1
hd : 1 ∣ 1
⊢ 2 ∣ 1
Theorem: LO.FirstOrder.Arith.Model.pow2_one
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 ⊧ₘ* 𝐈open
hr : 0 ≤ 1
hhr : 1 < 0
hd : 0 ∣ 1
⊢ 2 ∣ 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_one
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 ⊧ₘ* 𝐈open
hr : 1 ≤ 1
hhr : 1 < 1
hd : 1 ∣ 1
⊢ 2 ∣ 1
Tactic:
simp at hhr
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_pow2_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
⊢ ¬Pow2 0
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 ⊧ₘ* 𝐈open
h : Pow2 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.not_pow2_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
h : Pow2 0
⊢ False
Tactic:
have := h.pos
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
h : Pow2 0
this : 0 < 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.not_pow2_zero
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
h : Pow2 0
this : 0 < 0
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.two_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
h : Pow2 a
lt : 1 < a
⊢ a ∣ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.two_dvd'
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
h : Pow2 a
lt : a ≠ 1
⊢ 1 < a
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 ⊧ₘ* 𝐈open
a : M
h : Pow2 a
lt : a ≠ 1
A : ¬1 < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Pow2.two_dvd'
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
h : Pow2 a
lt : a ≠ 1
A : ¬1 < a
⊢ False
Tactic:
simp [le_one_iff_eq_zero_or_one] 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 ⊧ₘ* 𝐈open
a : M
h : Pow2 a
lt : a ≠ 1
A : a = 0 ∨ a = 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Pow2.two_dvd'
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
h : Pow2 a
lt : a ≠ 1
A : a = 0 ∨ a = 1
⊢ False
Tactic:
rcases A with (rfl | rfl) <;> simp at h lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.two_dvd'
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
h : Pow2 a
lt : a ≠ 1
⊢ a ∣ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
⊢ Pow2 a → Pow2 b
Tactic:
intro ha
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
⊢ Pow2 b
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
⊢ Pow2 b
Tactic:
have : 0 < b := by
  by_contra e
  have : a = 0 := by simpa [show b = 0 from by simpa using e] using h
  rcases this with rfl
  simpa using ha.pos
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
this : 0 < b
⊢ Pow2 b
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
this : 0 < b
⊢ Pow2 b
Tactic:
exact ⟨this, fun r hr ltr hb ↦
  ha.dvd (show r ≤ a from le_trans hr (le_of_dvd ha.pos h)) ltr (dvd_trans hb h)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
⊢ 0 < b
Tactic:
by_contra e
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
e : ¬0 < b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
e : ¬0 < b
⊢ False
Tactic:
have : a = 0 := by simpa [show b = 0 from by simpa using e] using 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 ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
e : ¬0 < b
this : a = 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
e : ¬0 < b
this : a = 0
⊢ False
Tactic:
rcases this with 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 ⊧ₘ* 𝐈open
b : M
e : ¬0 < b
h : b ∣ 0
ha : Pow2 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
b : M
e : ¬0 < b
h : b ∣ 0
ha : Pow2 0
⊢ False
Tactic:
simpa using ha.pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
e : ¬0 < b
⊢ a = 0
Tactic:
simpa [show b = 0 from by simpa using e] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.of_dvd
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : b ∣ a
ha : Pow2 a
e : ¬0 < b
⊢ b = 0
Tactic:
simpa using e
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
⊢ Pow2 (2 * a) → Pow2 a
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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
⊢ Pow2 a
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
⊢ Pow2 a
Tactic:
have : ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r := by
  intro r hr ltr dvd
  exact H.dvd (show r ≤ 2 * a from le_trans hr (le_mul_of_one_le_left (by simp) one_le_two)) ltr (Dvd.dvd.mul_left dvd 2)
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
this : ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
⊢ Pow2 a
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
this : ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
⊢ Pow2 a
Tactic:
exact ⟨by simpa using H.pos, this⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
⊢ ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
Tactic:
intro r hr ltr dvd
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
r : M
hr : r ≤ a
ltr : 1 < r
dvd : r ∣ a
⊢ 2 ∣ r
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
r : M
hr : r ≤ a
ltr : 1 < r
dvd : r ∣ a
⊢ 2 ∣ r
Tactic:
exact H.dvd (show r ≤ 2 * a from le_trans hr (le_mul_of_one_le_left (by simp) one_le_two)) ltr (Dvd.dvd.mul_left dvd 2)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
r : M
hr : r ≤ a
ltr : 1 < r
dvd : r ∣ a
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 (2 * a)
this : ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
⊢ 0 < a
Tactic:
simpa using H.pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
⊢ Pow2 a → Pow2 (2 * a)
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 ⊧ₘ* 𝐈open
a : M
H : Pow2 a
⊢ Pow2 (2 * a)
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 a
⊢ 0 < 2 * a
Tactic:
simpa using H.pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 a
⊢ ∀ r ≤ 2 * a, 1 < r → r ∣ 2 * a → 2 ∣ r
Tactic:
intro r _ hr hd
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd : r ∣ 2 * a
⊢ 2 ∣ r
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_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 ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd : r ∣ 2 * a
⊢ 2 ∣ r
Tactic:
rcases two_prime.left_dvd_or_dvd_right_of_dvd_mul hd with (hd | hd)
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 ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd✝ : r ∣ 2 * a
hd : 2 ∣ r
⊢ 2 ∣ r

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd✝ : r ∣ 2 * a
hd : r ∣ a
⊢ 2 ∣ r
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_two
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 ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd✝ : r ∣ 2 * a
hd : 2 ∣ r
⊢ 2 ∣ r
Tactic:
exact hd
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_two
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 ⊧ₘ* 𝐈open
a : M
H : Pow2 a
r : M
a✝ : r ≤ 2 * a
hr : 1 < r
hd✝ : r ∣ 2 * a
hd : r ∣ a
⊢ 2 ∣ r
Tactic:
exact H.dvd (show r ≤ a from le_of_dvd H.pos hd) hr hd
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pow2_mul_four
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
a : M
⊢ Pow2 (4 * a) ↔ Pow2 a
Tactic:
simp [←two_mul_two_eq_four, mul_assoc, pow2_mul_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
⊢ Pow2 p → p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
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 ⊧ₘ* 𝐈open
p : M
H : Pow2 p
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
H : Pow2 p
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Tactic:
by_cases hp : 1 < p
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 ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : 1 < p
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : ¬1 < p
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
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 ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : 1 < p
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Tactic:
have : 2 ∣ p := H.two_dvd hp
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 ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : 1 < p
this : 2 ∣ p
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
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 ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : 1 < p
this : 2 ∣ p
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Tactic:
rcases this with ⟨q, rfl⟩
Proof state after:
case pos.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
H : Pow2 (2 * q)
hp : 1 < 2 * q
⊢ 2 * q = 1 ∨ ∃ q_1, 2 * q = 2 * q_1 ∧ Pow2 q_1
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
Proof state before:
case pos.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
H : Pow2 (2 * q)
hp : 1 < 2 * q
⊢ 2 * q = 1 ∨ ∃ q_1, 2 * q = 2 * q_1 ∧ Pow2 q_1
Tactic:
right
Proof state after:
case pos.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
H : Pow2 (2 * q)
hp : 1 < 2 * q
⊢ ∃ q_1, 2 * q = 2 * q_1 ∧ Pow2 q_1
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
Proof state before:
case pos.intro.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
q : M
H : Pow2 (2 * q)
hp : 1 < 2 * q
⊢ ∃ q_1, 2 * q = 2 * q_1 ∧ Pow2 q_1
Tactic:
exact ⟨q, rfl, pow2_mul_two.mp H⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
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 ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : ¬1 < p
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Tactic:
have : p = 1 := le_antisymm (by simpa using hp) (pos_iff_one_le.mp H.pos)
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 ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : ¬1 < p
this : p = 1
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
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 ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : ¬1 < p
this : p = 1
⊢ p = 1 ∨ ∃ q, p = 2 * q ∧ Pow2 q
Tactic:
left
Proof state after:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : ¬1 < p
this : p = 1
⊢ p = 1
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
Proof state before:
case neg.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : ¬1 < p
this : p = 1
⊢ p = 1
Tactic:
exact this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Pow2.elim
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
p : M
H : Pow2 p
hp : ¬1 < p
⊢ p ≤ 1
Tactic:
simpa using hp
Proof state after:
no goals