Theorem: LO.FirstOrder.Arith.Model.le_of_subset (Arithmetization/ISigmaOne/Bit.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 b : M
h : a ⊆ b
⊢ a ≤ b
Tactic:
induction b using hierarchy_polynomial_induction_oRing_pi₁ generalizing a
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 {b} => ∀ {a : M}, a ⊆ b → a ≤ b

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : a ⊆ 0
⊢ a ≤ 0

case even
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ : M
a✝¹ : x✝ > 0
a✝ : ∀ {a : M}, a ⊆ x✝ → a ≤ x✝
a : M
h : a ⊆ 2 * x✝
⊢ a ≤ 2 * x✝

case odd
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ : M
a✝ : ∀ {a : M}, a ⊆ x✝ → a ≤ x✝
a : M
h : a ⊆ 2 * x✝ + 1
⊢ a ≤ 2 * x✝ + 1

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 : a ⊆ 0
⊢ a ≤ 0
Tactic:
case zero =>
  simp [eq_zero_of_subset_zero h]
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
a✝ : b > 0
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
⊢ a ≤ 2 * b
Tactic:
case even b _ IH =>
  have IH : a / 2 ≤ b := IH (by simpa using subset_div_two h)
  have : 2 * (a / 2) = a :=
    mul_div_self_of_dvd.mpr (zero_mem_iff.mp $ by intro ha; have : 0 ∈ 2 * b := h ha; simp_all)
  simpa [this] using mul_le_mul_left (a := 2) IH
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
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
⊢ a ≤ 2 * b + 1
Tactic:
case odd b IH =>
  have IH : a / 2 ≤ b := IH (by simpa [div_mul_add' b 2 one_lt_two] using subset_div_two h)
  exact le_trans (le_two_mul_div_two_add_one a) (by simpa using IH)
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 {b} => ∀ {a : M}, a ⊆ b → a ≤ b
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
h : a ⊆ 0
⊢ a ≤ 0
Tactic:
simp [eq_zero_of_subset_zero h]
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
a✝ : b > 0
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
⊢ a ≤ 2 * b
Tactic:
have IH : a / 2 ≤ b := IH (by simpa using subset_div_two h)
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
⊢ a ≤ 2 * b

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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
⊢ a ≤ 2 * b
Tactic:
have : 2 * (a / 2) = a :=
  mul_div_self_of_dvd.mpr (zero_mem_iff.mp $ by intro ha; have : 0 ∈ 2 * b := h ha; simp_all)
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
this : 2 * (a / 2) = a
⊢ a ≤ 2 * b

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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
this : 2 * (a / 2) = a
⊢ a ≤ 2 * b
Tactic:
simpa [this] using mul_le_mul_left (a := 2) IH
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
a✝ : b > 0
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
⊢ a / 2 ⊆ b
Tactic:
simpa using subset_div_two h
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
⊢ 0 ∉ a
Tactic:
intro ha
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
⊢ False

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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
⊢ False
Tactic:
have : 0 ∈ 2 * b := h ha
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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
this : 0 ∈ 2 * b
⊢ False

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
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
this : 0 ∈ 2 * b
⊢ False
Tactic:
simp_all
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
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
⊢ a ≤ 2 * b + 1
Tactic:
have IH : a / 2 ≤ b := IH (by simpa [div_mul_add' b 2 one_lt_two] using subset_div_two h)
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
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
IH : a / 2 ≤ b
⊢ a ≤ 2 * b + 1

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
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
IH : a / 2 ≤ b
⊢ a ≤ 2 * b + 1
Tactic:
exact le_trans (le_two_mul_div_two_add_one a) (by simpa using IH)
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
IH : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
⊢ a / 2 ⊆ b
Tactic:
simpa [div_mul_add' b 2 one_lt_two] using subset_div_two h
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
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b + 1
IH : a / 2 ≤ b
⊢ 2 * (a / 2) + 1 ≤ 2 * b + 1
Tactic:
simpa using IH
State after:
no goals