Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos (Arithmetization/Basic/IOpen.lean)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ ∃! u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
have : ∃ u, b * u ≤ a ∧ a < b * (u + 1) := by
  have : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1) := by
    simpa using open_leastNumber (P := fun u ↦ b * u ≤ a) ⟨“x | &b * x ≤ &a”, by simp, by intro x; simp⟩
  simp at this
  have hx : a < b * (a + 1) := by
    have : a + 0 < b * a + b :=
      add_lt_add_of_le_of_lt (le_mul_self_of_pos_left pos) pos
    simpa [mul_add] using this
  exact this hx
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃! u, b * u ≤ a ∧ a < b * (u + 1)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃! u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
rcases this with ⟨u, hu⟩
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃! u, b * u ≤ a ∧ a < b * (u + 1)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
have : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1) := by
  simpa using open_leastNumber (P := fun u ↦ b * u ≤ a) ⟨“x | &b * x ≤ &a”, by simp, by intro x; simp⟩
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
have hx : a < b * (a + 1) := by
  have : a + 0 < b * a + b :=
    add_lt_add_of_le_of_lt (le_mul_self_of_pos_left pos) pos
  simpa [mul_add] using this
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
hx : a < b * (a + 1)
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
hx : a < b * (a + 1)
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
exact this hx
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
simpa using open_leastNumber (P := fun u ↦ b * u ≤ a) ⟨“x | &b * x ≤ &a”, by simp, by intro x; 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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ “(&b * #0) ≤ &a”.Open
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ ∀ (x : M), (fun u => b * u ≤ a) x ↔ (Semiformula.Evalm M ![x] id) (“(&b * #0) ≤ &a”)
Tactic:
intro x
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
x : M
⊢ (fun u => b * u ≤ a) x ↔ (Semiformula.Evalm M ![x] id) (“(&b * #0) ≤ &a”)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
x : M
⊢ (fun u => b * u ≤ a) x ↔ (Semiformula.Evalm M ![x] id) (“(&b * #0) ≤ &a”)
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ a < b * (a + 1)
Tactic:
have : a + 0 < b * a + b :=
  add_lt_add_of_le_of_lt (le_mul_self_of_pos_left pos) pos
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this✝ : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
this : a + 0 < b * a + b
⊢ a < b * (a + 1)

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this✝ : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
this : a + 0 < b * a + b
⊢ a < b * (a + 1)
Tactic:
simpa [mul_add] using this
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
⊢ ∀ (y : M), b * y ≤ a ∧ a < b * (y + 1) → y = u
Tactic:
intro u' hu'
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
⊢ u' = u

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
⊢ u' = u
Tactic:
by_contra ne
State after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
⊢ False

State before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
⊢ False
Tactic:
wlog lt : u < u'
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] [inst_6 : M ⊧ₘ* 𝐈open] (a : M) {b : M},
    0 < b →
      ∀ (u : M), b * u ≤ a ∧ a < b * (u + 1) → ∀ (u' : M), b * u' ≤ a ∧ a < b * (u' + 1) → ¬u' = u → u < u' → False
lt : ¬u < u'
⊢ False

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
⊢ False

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
⊢ False
Tactic:
have : a < a := by calc
  a < b * (u + 1) := hu.2
  _ ≤ b * u'      := (_root_.mul_le_mul_left pos).mpr (lt_iff_succ_le.mp lt)
  _ ≤ a           := hu'.1
State after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
this : a < a
⊢ False

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
this : a < a
⊢ False
Tactic:
exact LT.lt.false this
State after:
no goals

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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] [inst_6 : M ⊧ₘ* 𝐈open] (a : M) {b : M},
    0 < b →
      ∀ (u : M), b * u ≤ a ∧ a < b * (u + 1) → ∀ (u' : M), b * u' ≤ a ∧ a < b * (u' + 1) → ¬u' = u → u < u' → False
lt : ¬u < u'
⊢ False
Tactic:
exact this a pos u' hu' u hu (Ne.symm ne) (Ne.lt_of_le ne $ by simpa using lt)
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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] [inst_6 : M ⊧ₘ* 𝐈open] (a : M) {b : M},
    0 < b →
      ∀ (u : M), b * u ≤ a ∧ a < b * (u + 1) → ∀ (u' : M), b * u' ≤ a ∧ a < b * (u' + 1) → ¬u' = u → u < u' → False
lt : ¬u < u'
⊢ u' ≤ u
Tactic:
simpa using lt
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✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
⊢ a < a
Tactic:
calc
a < b * (u + 1) := hu.2
_ ≤ b * u'      := (_root_.mul_le_mul_left pos).mpr (lt_iff_succ_le.mp lt)
_ ≤ a           := hu'.1
State after:
no goals