α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
let s : Set ℤ := { n : ℤ | n • a ≤ g }
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
obtain ⟨k, hk : -g ≤ k • a⟩ := Archimedean.arch (-g) ha
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
h_ne : Set.Nonempty s
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
have h_ne : s.Nonempty := ⟨-k, by simpa using neg_le_neg hk⟩
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
h_ne : Set.Nonempty s
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
obtain ⟨k, hk⟩ := Archimedean.arch g ha
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
  intro n hn
  apply (zsmul_le_zsmul_iff ha).mp
  rw [← coe_nat_zsmul] at hk
  exact le_trans hn hk
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
have hm'' : g < (m + 1) • a := by
  contrapose! hm'
  exact ⟨m + 1, hm', lt_add_one _⟩
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
n : ℤ
hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n
⊢ m < n + 1
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
refine' ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one _⟩
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
n : ℤ
hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n
⊢ m • a < (n + 1) • a
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
n : ℤ
hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n
⊢ m < n + 1
rw [← zsmul_lt_zsmul_iff ha]
no goals
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
n : ℤ
hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n
⊢ m • a < (n + 1) • a
exact lt_of_le_of_lt hm hn.2
no goals
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
⊢ -↑k ∈ s
simpa using neg_le_neg hk
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
n : ℤ
hn : n ∈ s
⊢ n ≤ ↑k
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
⊢ ∀ (n : ℤ), n ∈ s → n ≤ ↑k
intro n hn
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
n : ℤ
hn : n ∈ s
⊢ n • a ≤ ↑k • a
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
n : ℤ
hn : n ∈ s
⊢ n ≤ ↑k
apply (zsmul_le_zsmul_iff ha).mp
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ ↑k • a
n : ℤ
hn : n ∈ s
⊢ n • a ≤ ↑k • a
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
n : ℤ
hn : n ∈ s
⊢ n • a ≤ ↑k • a
rw [← coe_nat_zsmul] at hk
no goals
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ ↑k • a
n : ℤ
hn : n ∈ s
⊢ n • a ≤ ↑k • a
exact le_trans hn hk
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : (m + 1) • a ≤ g
⊢ ∃ z, z ∈ {n | n • a ≤ g} ∧ m < z
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
⊢ g < (m + 1) • a
contrapose! hm'
no goals
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : (m + 1) • a ≤ g
⊢ ∃ z, z ∈ {n | n • a ≤ g} ∧ m < z
exact ⟨m + 1, hm', lt_add_one _⟩